Prepare for smtml.0.25.0

Use the new bitvector API that requires passing bit offsets instead of
the previous non-standard byte offsets.

Author: filipeom

dune-project

@@ -75,7 +75,7 @@
   (sedlex
    (>= 3.3))
   (smtml
-   (>= 0.22.0))
+   (>= 0.25.0))
   (symex
    (>= 0.2))
   (synchronizer

owi.opam

@@ -39,7 +39,7 @@ depends: [
   "prelude" {>= "0.5"}
   "processor" {>= "0.2"}
   "sedlex" {>= "3.3"}
-  "smtml" {>= "0.22.0"}
+  "smtml" {>= "0.25.0"}
   "symex" {>= "0.2"}
   "synchronizer" {>= "0.3"}
   "uutf" {>= "1.0.3"}

shell.nix

@@ -22,6 +22,14 @@ let
       };
       meta.broken = false;
     });
+    smtml = super.smtml.overrideAttrs (old: {
+      src = pkgs.fetchFromGitHub {
+        owner = "formalsec";
+        repo = "smtml";
+        rev = "3d19685d6859df7695eb697571b2a8ec41638068";
+        hash = "sha256-dWZrN0hTxxqGC2queit91GDuw/x5fyRPwHbmKxkvc/w=";
+      };
+    });
   });
   tinygo = pkgs.tinygo.overrideAttrs (old: {
     doCheck = false;
@@ -45,6 +53,7 @@ pkgs.mkShell {
     merlin
     ocaml
     ocamlformat
+    ocaml-lsp
     ocp-browser
     ocp-index
     ocb

src/symbolic/symbolic_memory.ml

@@ -173,17 +173,17 @@ let store_8 m ~addr v =
   let open Symbolic_choice in
   let* a = must_be_valid_address m addr 1 in
   let data =
-    replace_byte a (Smtml.Typed.Bitv32.extract v ~high:1 ~low:0) m.data
+    replace_byte a (Smtml.Typed.Bitv32.extract v ~high:7 ~low:0) m.data
   in
   replace { m with data }
 
 let store_16 m ~addr v =
   let open Symbolic_choice in
   let* a = must_be_valid_address m addr 2 in
   let data =
-    replace_byte a (Smtml.Typed.Bitv32.extract v ~high:1 ~low:0) m.data
+    replace_byte a (Smtml.Typed.Bitv32.extract v ~high:7 ~low:0) m.data
     |> replace_byte (Int32.add a 1l)
-         (Smtml.Typed.Bitv32.extract v ~high:2 ~low:1)
+         (Smtml.Typed.Bitv32.extract v ~high:15 ~low:8)
   in
   replace { m with data }
 
@@ -213,7 +213,7 @@ let store_64 m ~(addr : Symbolic_i32.t) v =
 let store_8_no_replace m data ~(addr : Symbolic_i32.t) v =
   let open Symbolic_choice in
   let+ a = must_be_valid_address m addr 1 in
-  replace_byte a (Smtml.Typed.Bitv32.extract v ~high:1 ~low:0) data
+  replace_byte a (Smtml.Typed.Bitv32.extract v ~high:7 ~low:0) data
 
 let fill m ~(pos : Symbolic_i32.t) ~(len : Symbolic_i32.t) (c : char) =
   let open Symbolic_choice in