Automate wrappers around stubs

.github/workflows/build.yml

@@ -8,12 +8,12 @@ env:
   OCAML_VERSION: 5.4.0
   # [versionsync: OBOL_REPO=soteria-tools/obol]
   OBOL_REPO: soteria-tools/obol
-  # [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c]
-  OBOL_COMMIT_HASH: 3d2266de79f1e2e601b7a82f6803b649cbe6953c
+  # [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41]
+  OBOL_COMMIT_HASH: ddea5ca5da4c07301584f47f05ea8615fc365b41
   # [versionsync: CHARON_REPO=soteria-tools/charon]
   CHARON_REPO: soteria-tools/charon
-  # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
-  CHARON_COMMIT_HASH: fbd54169205bf97e3c42cbfef95ca5807d697bfb
+  # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
+  CHARON_COMMIT_HASH: fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba
 
 jobs:
   build:

.github/workflows/test-packages.yml

@@ -6,8 +6,8 @@ on:
 env:
   # [versionsync: OBOL_REPO=soteria-tools/obol]
   OBOL_REPO: soteria-tools/obol
-  # [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c]
-  OBOL_COMMIT_HASH: 3d2266de79f1e2e601b7a82f6803b649cbe6953c
+  # [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41]
+  OBOL_COMMIT_HASH: ddea5ca5da4c07301584f47f05ea8615fc365b41
 
 jobs:
   test-soteria-c-package:

README.md

@@ -137,12 +137,12 @@ We support two frontends: [Obol](https://github.com/soteria-tools/obol) and [Cha
 
 **Manual installation:**
 1. **Clone Obol at the correct commit:**
-   <!-- [versionsync: OBOL_COMMIT_HASH=3d2266de79f1e2e601b7a82f6803b649cbe6953c] -->
+   <!-- [versionsync: OBOL_COMMIT_HASH=ddea5ca5da4c07301584f47f05ea8615fc365b41] -->
    ```sh
    cd ..
    git clone https://github.com/soteria-tools/obol.git
    cd obol
-   git checkout 3d2266de79f1e2e601b7a82f6803b649cbe6953c
+   git checkout ddea5ca5da4c07301584f47f05ea8615fc365b41
    ```
    > **Note:** The required commit hash can always be found in [`scripts/versions.json`](scripts/versions.json) under `OBOL_COMMIT_HASH`.
 
@@ -168,12 +168,12 @@ We support two frontends: [Obol](https://github.com/soteria-tools/obol) and [Cha
 
 **Manual installation:**
 1. **Clone Charon at the correct commit:**
-   <!-- [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb] -->
+   <!-- [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba] -->
    ```sh
    cd ..
    git clone https://github.com/soteria-tools/charon.git
    cd charon
-   git checkout fbd54169205bf97e3c42cbfef95ca5807d697bfb
+   git checkout fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba
    ```
    > **Note:** The required commit hash can always be found in [`scripts/versions.json`](scripts/versions.json) under `CHARON_COMMIT_HASH`.
 

scripts/versions.json

@@ -1,9 +1,9 @@
 {
   "_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.",
   "CHARON_REPO": "soteria-tools/charon",
-  "CHARON_COMMIT_HASH": "fbd54169205bf97e3c42cbfef95ca5807d697bfb",
+  "CHARON_COMMIT_HASH": "fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba",
   "OBOL_REPO": "soteria-tools/obol",
-  "OBOL_COMMIT_HASH": "3d2266de79f1e2e601b7a82f6803b649cbe6953c",
+  "OBOL_COMMIT_HASH": "ddea5ca5da4c07301584f47f05ea8615fc365b41",
   "OCAMLFORMAT_VERSION": "0.28.1",
   "OCAML_VERSION": "5.4.0"
 }

soteria-rust.opam

@@ -55,8 +55,8 @@ build: [
 dev-repo: "git+https://github.com/soteria-tools/soteria.git"
 # Versions managed by scripts/versionsync.py - edit scripts/versions.json to change
 pin-depends: [
-  # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
-  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
-  # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
-  ["charon.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
+  # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
+  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
+  # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
+  ["charon.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
 ]

soteria-rust.opam.template

@@ -1,7 +1,7 @@
 # Versions managed by scripts/versionsync.py - edit scripts/versions.json to change
 pin-depends: [
-  # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
-  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
-  # [versionsync: CHARON_COMMIT_HASH=fbd54169205bf97e3c42cbfef95ca5807d697bfb]
-  ["charon.~dev" "git+https://github.com/soteria-tools/charon#fbd54169205bf97e3c42cbfef95ca5807d697bfb"]
+  # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
+  ["name_matcher_parser.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
+  # [versionsync: CHARON_COMMIT_HASH=fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba]
+  ["charon.~dev" "git+https://github.com/soteria-tools/charon#fa7ff7118fc9f695ecde2b4aa8401fe3ea195fba"]
 ]

soteria-rust/lib/builtins/core.ml

@@ -208,4 +208,27 @@ module M (StateM : State.StateM.S) = struct
       State.load ptr ty
     in
     Soteria.Symex.Compo_res.is_ok res
+
+  let parse_string ptr =
+    let str_ty : Charon.Types.ty =
+      TAdt
+        { id = TBuiltin TStr; generics = Charon.TypesUtils.empty_generic_args }
+    in
+    let+ str_data = State.load ptr str_ty in
+    let map_opt f l = Option.bind l (Monad.OptionM.all f) in
+    match str_data with
+    | Tuple bytes ->
+        Some bytes
+        |> map_opt (function Int b -> Typed.BitVec.to_z b | _ -> None)
+        |> Option.map (fun cs ->
+            let cs = List.map (fun z -> Char.chr (Z.to_int z)) cs in
+            let str = String.of_seq @@ List.to_seq cs in
+            if
+              String.starts_with ~prefix:"\"" str
+              && String.ends_with ~suffix:"\"" str
+            then
+              let unquoted = String.sub str 1 (String.length str - 2) in
+              try Scanf.unescaped unquoted with _ -> unquoted
+            else str)
+    | _ -> None
 end