Skip to content

Commit 23dcbe8

Browse files
N1arkN1ark
authored
Automate wrappers around stubs (#325)
* Bump Charon and Obol * Separate externs/intrinsics handling + fix poly * Update intrinsics script for new Charon AST * Add automated stub generation * organise into folders * simplify * organise intrinsics into folders * reorganise externs * remove leading underscores in arguments * finish cleaning * Rename `intrinsincs.py` -> `stubs.py` * I guess soteria should be stubbed like the rest * support "with sig" in stubs + fixes * Update eval.ml * Migrate new stubs * Delete intrinsics.py * Add missing stub * support custom "with" in patterns * move comment * this comment disappeared? @claude come on * hehe * Saner JSON + schema * We never needed that Miri lib * Better stubs.json * match on impl elems too + tokio !! * Add soteria comment * Add pattern aliases * Add `include` to stubs json * Add alias of std::rt::begin_panic * Document `eval.ml`
1 parent 604111f commit 23dcbe8

48 files changed

Lines changed: 3700 additions & 1565 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/build.yml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,12 @@ env:
88
OCAML_VERSION: 5.4.0
99
# [versionsync: OBOL_REPO=soteria-tools/obol]
1010
OBOL_REPO: soteria-tools/obol
11-
# [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c]
12-
OBOL_COMMIT_HASH: 3d2266de79f1e2e601b7a82f6803b649cbe6953c
11+
# [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41]
12+
OBOL_COMMIT_HASH: ddea5ca5da4c07301584f47f05ea8615fc365b41
1313
# [versionsync: CHARON_REPO=soteria-tools/charon]
1414
CHARON_REPO: soteria-tools/charon
15-
# [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
16-
CHARON_COMMIT_HASH: fbd54169205bf97e3c42cbfef95ca5807d697bfb
15+
# [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
16+
CHARON_COMMIT_HASH: fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba
1717

1818
jobs:
1919
build:

‎.github/workflows/test-packages.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ on:
66
env:
77
# [versionsync: OBOL_REPO=soteria-tools/obol]
88
OBOL_REPO: soteria-tools/obol
9-
# [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c]
10-
OBOL_COMMIT_HASH: 3d2266de79f1e2e601b7a82f6803b649cbe6953c
9+
# [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41]
10+
OBOL_COMMIT_HASH: ddea5ca5da4c07301584f47f05ea8615fc365b41
1111

1212
jobs:
1313
test-soteria-c-package:

‎README.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -137,12 +137,12 @@ We support two frontends: [Obol](https://github.com/soteria-tools/obol) and [Cha
137137
138138
**Manual installation:**
139139
1. **Clone Obol at the correct commit:**
140-
<!-- [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c] -->
140+
<!-- [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41] -->
141141
```sh
142142
cd ..
143143
git clone https://github.com/soteria-tools/obol.git
144144
cd obol
145-
git checkout 3d2266de79f1e2e601b7a82f6803b649cbe6953c
145+
git checkout ddea5ca5da4c07301584f47f05ea8615fc365b41
146146
```
147147
> **Note:** The required commit hash can always be found in [`scripts/versions.json`](scripts/versions.json) under `OBOL_COMMIT_HASH`.
148148
@@ -168,12 +168,12 @@ We support two frontends: [Obol](https://github.com/soteria-tools/obol) and [Cha
168168

169169
**Manual installation:**
170170
1. **Clone Charon at the correct commit:**
171-
<!-- [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb] -->
171+
<!-- [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba] -->
172172
```sh
173173
cd ..
174174
git clone https://github.com/soteria-tools/charon.git
175175
cd charon
176-
git checkout fbd54169205bf97e3c42cbfef95ca5807d697bfb
176+
git checkout fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba
177177
```
178178
> **Note:** The required commit hash can always be found in [`scripts/versions.json`](scripts/versions.json) under `CHARON_COMMIT_HASH`.
179179

‎scripts/versions.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
{
22
"_comment": "Central version configuration for Soteria. Run `scripts/versionsync.py check` to verify versions are in sync, or `scripts/versionsync.py update` to update versions everywhere.",
33
"CHARON_REPO": "soteria-tools/charon",
4-
"CHARON_COMMIT_HASH": "fbd54169205bf97e3c42cbfef95ca5807d697bfb",
4+
"CHARON_COMMIT_HASH": "fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba",
55
"OBOL_REPO": "soteria-tools/obol",
6-
"OBOL_COMMIT_HASH": "3d2266de79f1e2e601b7a82f6803b649cbe6953c",
6+
"OBOL_COMMIT_HASH": "ddea5ca5da4c07301584f47f05ea8615fc365b41",
77
"OCAMLFORMAT_VERSION": "0.28.1",
88
"OCAML_VERSION": "5.4.0"
99
}

‎soteria-rust.opam‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,8 @@ build: [
5555
dev-repo: "git+https://github.com/soteria-tools/soteria.git"
5656
# Versions managed by scripts/versionsync.py - edit scripts/versions.json to change
5757
pin-depends: [
58-
# [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
59-
["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
60-
# [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
61-
["charon.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
58+
# [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
59+
["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
60+
# [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
61+
["charon.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
6262
]

‎soteria-rust.opam.template‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
# Versions managed by scripts/versionsync.py - edit scripts/versions.json to change
22
pin-depends: [
3-
# [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
4-
["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
5-
# [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
6-
["charon.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
3+
# [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
4+
["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
5+
# [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
6+
["charon.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
77
]

‎soteria-rust/lib/builtins/core.ml‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -208,4 +208,27 @@ module M (StateM : State.StateM.S) = struct
208208
State.load ptr ty
209209
in
210210
Soteria.Symex.Compo_res.is_ok res
211+
212+
let parse_string ptr =
213+
let str_ty : Charon.Types.ty =
214+
TAdt
215+
{ id = TBuiltin TStr; generics = Charon.TypesUtils.empty_generic_args }
216+
in
217+
let+ str_data = State.load ptr str_ty in
218+
let map_opt f l = Option.bind l (Monad.OptionM.all f) in
219+
match str_data with
220+
| Tuple bytes ->
221+
Some bytes
222+
|> map_opt (function Int b -> Typed.BitVec.to_z b | _ -> None)
223+
|> Option.map (fun cs ->
224+
let cs = List.map (fun z -> Char.chr (Z.to_int z)) cs in
225+
let str = String.of_seq @@ List.to_seq cs in
226+
if
227+
String.starts_with ~prefix:"\"" str
228+
&& String.ends_with ~suffix:"\"" str
229+
then
230+
let unquoted = String.sub str 1 (String.length str - 2) in
231+
try Scanf.unescaped unquoted with _ -> unquoted
232+
else str)
233+
| _ -> None
211234
end

0 commit comments

Comments
 (0)