Symbolic abstractions

soteria-c/lib/ctree_block.ml

@@ -11,24 +11,29 @@ module MemVal = struct
   module TB = Soteria.Sym_states.Tree_block
   module Symex = Csymex
 
-  module SBoundedInt = struct
-    include Typed
-    include Typed.Infix
+  module Bounded_int = struct
+    module Symex = Symex
 
-    type sint = T.sint
-    type sbool = T.sbool
+    type t = T.sint Typed.t
 
     let zero () = Usize.(0s)
-    let ( <@ ) = Typed.Infix.( <$@ )
-    let ( <=@ ) = Typed.Infix.( <=$@ )
+    let one () = Usize.(1s)
 
-    (* We assume addition/overflow within the range of an allocation may never overflow.
-       This allows extremely good reductions around inequalities, which Tree_block relies on.  *)
-    let ( +@ ) = Typed.Infix.( +!!@ )
-    let ( -@ ) = Typed.Infix.( -!!@ )
-
-    let in_bound (v : sint Typed.t) : sbool Typed.t =
+    let in_bound (v : t) : T.sbool Typed.t =
       v >=@ zero () &&@ (v <=@ Typed.BitVec.isize_max)
+
+    let pp = Value.ppa
+    let of_z z = Typed.BitVec.usize z
+    let subst = Typed.subst
+    let iter_vars v f = Typed.iter_vars v f
+    let equal = Typed.equal
+    let sem_eq = Typed.sem_eq
+    let distinct = Typed.distinct
+    let add = Infix.( +!@ )
+    let sub = Infix.( -!@ )
+    let to_z = Typed.BitVec.to_z
+    let lt = Infix.( <@ )
+    let leq = Infix.( <=@ )
   end
 
   let pp_init ft (v, ty) =

soteria-c/lib/driver.ml

@@ -338,7 +338,7 @@ let dump_summaries results =
       let pp_summary ~fid ft summary =
         Fmt.pf ft "@[<v 2>%a@]" Summary.pp (Summary.analyse ~fid summary)
       in
-      let@ oc = Channels.with_out_file file in
+      let@ oc = Out_channel.with_open_text file in
       let ft = Format.formatter_of_out_channel oc in
       List.iter
         (fun (fid, summaries) ->

soteria-c/lib/globs.ml

@@ -57,7 +57,7 @@ let get sym st =
                let open Typed.Infix in
                if Cerb_frontend.Symbol.equal_sym k sym then None
                else
-                 let neq = Typed.not (v ==@ loc) in
+                 let neq = Typed.S_bool.not (v ==@ loc) in
                  Some neq)
         |> List.of_seq
       in
@@ -75,7 +75,7 @@ let produce serialized st =
       |> Seq.self_cross_product
       |> Seq.map (fun ((_, loca), (_, locb)) ->
              let open Typed.Infix in
-             Typed.not (loca ==@ locb))
+             Typed.S_bool.not (loca ==@ locb))
       |> List.of_seq
     in
     assume to_assume

soteria-c/lib/interp.ml

@@ -1304,7 +1304,7 @@ module Make (State : State_intf.S) = struct
         let rec loop () =
           let* cond_v = eval_expr cond in
           let^ cond_v = cast_aggregate_to_bool cond_v in
-          let neg_cond = Typed.not cond_v in
+          let neg_cond = Typed.S_bool.not cond_v in
           if%sat neg_cond then ok Normal
           else
             let () = L.trace (fun m -> m "Condition is SAT!") in
@@ -1325,7 +1325,7 @@ module Make (State : State_intf.S) = struct
           | Normal | Continue ->
               let* cond_v = eval_expr cond in
               let^ cond_v = cast_aggregate_to_bool cond_v in
-              if%sat Typed.not cond_v then ok Normal else loop ()
+              if%sat Typed.S_bool.not cond_v then ok Normal else loop ()
           | Case _ -> failwith "SOTERIA BUG: Case in do body"
         in
         loop ()

soteria-c/test/cram/simple_bi.t/run.t

@@ -23,7 +23,7 @@
                info = None })];
            globs = [] }
           ];
-        pc = [(0x0000000000000000 != V|1|); (0xfffffffffffffffc <=u V|2|)];
+        pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
         post =
         { heap =
           [(V|1|,
@@ -122,7 +122,7 @@ NO_COLOR=true is necessary to avoid test output changing in CI. For some reason,
                info = None })];
            globs = [] }
           ];
-        pc = [(0x0000000000000000 != V|1|); (0xfffffffffffffffc <=u V|2|)];
+        pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
         post =
         { heap =
           [(V|1|,
@@ -255,7 +255,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|2|); (0x00000001 <=u V|1|);
-          (V|1| <=u 0x7fffffff); (0xfffffffffffffffc <=u V|3|)];
+          (V|1| <=u 0x7fffffff); (V|3| <=u 0x7ffffffffffffffb)];
         post =
         { heap =
           [(V|2|,
@@ -309,7 +309,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|1|); (V|3| == 0x00000001);
-          (0xfffffffffffffffc <=u V|2|); (V|3| == 0x00000001)];
+          (V|2| <=u 0x7ffffffffffffffb); (V|3| == 0x00000001)];
         post =
         { heap =
           [(V|1|,
@@ -341,17 +341,20 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|1|);
+          ((V|2| <s 0x0000000000000000) == ((V|2| + 0x0000000000000004) <s 0x0000000000000000));
+          ((V|2| + 0x0000000000000004) <u (V|2| + 0x0000000000000008));
+          ((V|2| + 0x0000000000000004) <=u (V|2| +ck 0x0000000000000004));
           ((V|4| <s 0x00000000) != ((V|4| + V|5|) <s 0x00000000));
           ((V|4| <s 0x00000000) == (V|5| <s 0x00000000));
-          (0xfffffffffffffffc <=u V|2|); (0x00000002 <=u V|3|);
+          (V|2| <=u 0x7ffffffffffffff7); (0x00000002 <=u V|3|);
           (V|3| <=u 0x7fffffff)];
         post =
         { heap =
           [(V|1|,
             { node =
               [MemVal {offset = V|2|; len = 0x0000000000000004;
                  v = V|4| : signed int};
-               MemVal {offset = (V|2| +ck 0x0000000000000004);
+               MemVal {offset = (V|2| + 0x0000000000000004);
                  len = 0x0000000000000004; v = V|5| : signed int}];
               info = None })];
           globs = [] };
@@ -381,16 +384,19 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
           ];
         pc =
         [(0x0000000000000000 != V|1|);
+          ((V|2| <s 0x0000000000000000) == ((V|2| + 0x0000000000000004) <s 0x0000000000000000));
+          ((V|2| + 0x0000000000000004) <u (V|2| + 0x0000000000000008));
+          ((V|2| + 0x0000000000000004) <=u (V|2| +ck 0x0000000000000004));
           (((V|4| <s 0x00000000) == ((V|4| + V|5|) <s 0x00000000)) || ((V|4| <s 0x00000000) != (V|5| <s 0x00000000)));
-          (V|3| == 0x00000002); (0xfffffffffffffffc <=u V|2|);
+          (V|3| == 0x00000002); (V|2| <=u 0x7ffffffffffffff7);
           (V|3| == 0x00000002)];
         post =
         { heap =
           [(V|1|,
             { node =
               [MemVal {offset = V|2|; len = 0x0000000000000004;
                  v = V|4| : signed int};
-               MemVal {offset = (V|2| +ck 0x0000000000000004);
+               MemVal {offset = (V|2| + 0x0000000000000004);
                  len = 0x0000000000000004; v = V|5| : signed int}];
               info = None })];
           globs = [] };

soteria-rust/lib/interp.ml

@@ -108,7 +108,7 @@ module Make (State : State_intf.S) = struct
   let rec resolve_constant (const : Expressions.constant_expr) =
     match const.kind with
     | CLiteral (VScalar scalar) -> ok (Base (BV.of_scalar scalar))
-    | CLiteral (VBool b) -> ok (Base (BV.of_bool (Typed.bool b)))
+    | CLiteral (VBool b) -> ok (Base (BV.of_bool (Typed.S_bool.of_bool b)))
     | CLiteral (VChar c) -> ok (Base (BV.u32i (Uchar.to_int c)))
     | CLiteral (VFloat { float_value; float_ty }) ->
         ok (Base (Typed.Float.mk float_ty float_value))

soteria-rust/lib/rtree_block.ml

@@ -19,26 +19,31 @@ module Make (Sptr : Sptr.S) = struct
     module TB = Soteria.Sym_states.Tree_block
     module Symex = DecayMapMonad
 
-    module SBoundedInt = struct
-      include Typed
-      include Typed.Infix
+    module Bounded_int = struct
+      module Symex = Symex
 
-      type sint = T.sint
-      type sbool = T.sbool
+      type t = T.sint Typed.t
 
       let zero () = Typed.BitVec.usize Z.zero
-      let ( <@ ) = Typed.Infix.( <$@ )
-      let ( <=@ ) = Typed.Infix.( <=$@ )
+      let one () = Typed.BitVec.usize Z.one
 
-      (* We assume addition/overflow within the range of an allocation may never overflow.
-         This allows extremely good reductions around inequalities, which Tree_block relies on.  *)
-      let ( +@ ) = Typed.Infix.( +!!@ )
-      let ( -@ ) = Typed.Infix.( -!!@ )
-
-      let in_bound (v : sint Typed.t) : sbool Typed.t =
+      let in_bound (v : t) : S_bool.t Typed.t =
         let max = Layout.max_value_z (TInt Isize) in
         let max = Typed.BitVec.usize max in
         v >=@ zero () &&@ (v <=@ max)
+
+      let pp = Value.ppa
+      let of_z z = Typed.BitVec.usize z
+      let subst = Typed.subst
+      let iter_vars v f = Typed.iter_vars v f
+      let equal = Typed.equal
+      let sem_eq = Typed.sem_eq
+      let distinct = Typed.distinct
+      let add = Infix.( +!@ )
+      let sub = Infix.( -!@ )
+      let to_z = Typed.BitVec.to_z
+      let lt = Infix.( <@ )
+      let leq = Infix.( <=@ )
     end
 
     let pp_init ft (v, ty) =

soteria-rust/lib/rustsymex.ml

@@ -12,7 +12,7 @@ include
 
 include Syntaxes.FunctionWrap
 
-let match_on (elements : 'a list) ~(constr : 'a -> Typed.sbool Typed.t) :
+let match_on (elements : 'a list) ~(constr : 'a -> Typed.S_bool.t Typed.t) :
     'a option t =
   let open Syntax in
   let rec aux = function

soteria-rust/lib/typed.ml

@@ -94,7 +94,7 @@ module BitVec = struct
   let of_literal : Values.literal -> [> T.sint ] t = function
     | VScalar s -> of_scalar s
     | VChar c -> u32i (Uchar.to_int c)
-    | VBool b -> of_bool (bool b)
+    | VBool b -> of_bool (S_bool.of_bool b)
     | l ->
         Fmt.failwith "Cannot convert non-scalar literal %s to bitvector"
           (PrintValues.literal_to_string l)

soteria/lib/bv_values/analyses.ml

@@ -18,7 +18,7 @@ module type S = sig
 
   (** Encode all the information relevant to the given variables and conjuncts
       them with the given accumulator. *)
-  val encode : ?vars:Var.Hashset.t -> t -> Typed.sbool Typed.t Iter.t
+  val encode : ?vars:Var.Hashset.t -> t -> Typed.S_bool.t Typed.t Iter.t
 end
 
 module Merge (A1 : S) (A2 : S) : S = struct
@@ -45,7 +45,7 @@ module Merge (A1 : S) (A2 : S) : S = struct
     let v'', vars2 = A2.add_constraint a2 v' in
     (v'', Var.Set.union vars1 vars2)
 
-  let encode ?vars (a1, a2) : Typed.sbool Typed.t Iter.t =
+  let encode ?vars (a1, a2) : Typed.S_bool.t Typed.t Iter.t =
     Iter.append (A1.encode ?vars a1) (A2.encode ?vars a2)
 end
 
@@ -266,7 +266,7 @@ module Interval : S = struct
           m "Useless range  %a: %a %a = %a" Var.pp var Data.pp range Range.pps
             new_range Data.pp range');
       let is_ok = not (Data.is_empty range) in
-      (Svalue.Bool.bool is_ok, Var.Set.empty, st))
+      (Svalue.S_bool.of_bool is_ok, Var.Set.empty, st))
     else
       let st = Var.Map.add var range' st in
       log (fun m ->
@@ -281,12 +281,12 @@ module Interval : S = struct
         (eq, Var.Set.empty, st)
       else if Data.is_empty range' then
         (* The range is empty, so this cannot be true *)
-        (Svalue.Bool.v_false, Var.Set.empty, st)
+        (Svalue.S_bool.v_false, Var.Set.empty, st)
       else
         (* We could cleanly absorb the range, so the PC doesn't need to store it -- however
            we must mark this variable as dirty, as maybe the modified range still renders
            the branch infeasible, e.g. because of some additional PC assertions. *)
-        (Svalue.Bool.v_true, Var.Set.singleton var, st)
+        (Svalue.S_bool.v_true, Var.Set.singleton var, st)
 
   let rec as_range (v : Svalue.t) =
     match v.node.kind with
@@ -430,8 +430,8 @@ module Interval : S = struct
         (v1' &&@ v2', learnt1 &&@ learnt2, Var.Set.union vars1 vars2, st'')
     | _, (lazy (Some (var, size, srange))) ->
         let learnt, vars, st' = update st var size srange in
-        (Svalue.Bool.v_true, learnt, vars, st')
-    | _, (lazy None) -> (v, Svalue.Bool.v_true, Var.Set.empty, st)
+        (Svalue.S_bool.v_true, learnt, vars, st')
+    | _, (lazy None) -> (v, Svalue.S_bool.v_true, Var.Set.empty, st)
 
   let simplify (v : Svalue.t) st =
     match (v.node.kind, lazy (as_range v)) with
@@ -447,10 +447,10 @@ module Interval : S = struct
         (* If the state is unchanged, then the conjunction covers all possible states and
            this is always true. (I think.) *)
         if
-          Svalue.equal v1' Svalue.Bool.v_true
-          && Svalue.equal v2' Svalue.Bool.v_true
+          Svalue.equal v1' Svalue.S_bool.v_true
+          && Svalue.equal v2' Svalue.S_bool.v_true
           && st_equal st st'
-        then Svalue.Bool.v_true
+        then Svalue.S_bool.v_true
         else v
     | _, (lazy (Some (var, size, srange))) ->
         let range = get size var st in
@@ -460,8 +460,8 @@ module Interval : S = struct
         let range', redundant = Data.add range srange in
         log (fun m ->
             m "Redundant? %b Empty? %b" redundant (Data.is_empty range'));
-        if redundant then Svalue.Bool.v_true
-        else if Data.is_empty range' then Svalue.Bool.v_false
+        if redundant then Svalue.S_bool.v_true
+        else if Data.is_empty range' then Svalue.S_bool.v_false
         else v
     | _, (lazy None) -> v
 
@@ -480,7 +480,7 @@ module Interval : S = struct
   let simplify st v = wrap_read (simplify v) st
   let add_constraint st v = wrap (add_constraint v) st
 
-  let encode ?vars st : Typed.sbool Typed.t Iter.t =
+  let encode ?vars st : Typed.S_bool.t Typed.t Iter.t =
     let to_check =
       Option.fold ~none:(fun _ -> true) ~some:Var.Hashset.mem vars
     in
@@ -566,8 +566,8 @@ module Equality : S = struct
         | None -> (
             match v.node.kind with
             | Binop ((Eq | Leq _), l, r) when known_eq l r st ->
-                Svalue.Bool.v_true
-            | Binop (Lt _, l, r) when known_eq l r st -> Svalue.Bool.v_false
+                Svalue.S_bool.v_true
+            | Binop (Lt _, l, r) when known_eq l r st -> Svalue.S_bool.v_false
             | Binop (op, l, r) ->
                 let l' = simplify l in
                 let r' = simplify r in