Upgrade encoding to latest smtml release

formalsec · Apr 25, 2024 · 4c2bad4 · 4c2bad4
1 parent 0fa8fc9
commit 4c2bad4
Show file tree

Hide file tree

Showing 13 changed files with 91 additions and 99 deletions.
diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml
@@ -151,15 +151,15 @@ let run ?(no_values = false) ?(test = false) input mode =
        Total Execution time: %f\n\
        Total Solver time: %f\n"
       execution_time
-      !Encoding.Solver.Z3_batch.solver_time;
+      !Smtml.Solver.Z3_batch.solver_time;
   write_report
     { execution_time
     ; mode
     ; num_paths
     ; num_problems
     ; problems
     ; filename = input
-    ; solver_time = !Encoding.Solver.Z3_batch.solver_time
+    ; solver_time = !Smtml.Solver.Z3_batch.solver_time
     }
 
 let main (opts : options) =

diff --git a/dune-project b/dune-project
@@ -33,7 +33,7 @@
    bos
    cmdliner
    ppx_deriving_yojson
-   (encoding (= "dev"))
+   (smtml (= "0.1.0"))
    (bisect_ppx (and :with-test (>= "2.5.0"))))
  (tags
   (topics "to describe" your project)))

diff --git a/lib/dune b/lib/dune
@@ -2,7 +2,7 @@
 
 (library
  (name whilloc)
- (libraries z3 ppx_deriving_yojson.runtime encoding)
+ (libraries ppx_deriving_yojson.runtime smtml)
  (preprocess
   (pps ppx_deriving_yojson))
  (instrumentation

diff --git a/lib/eval_concolic.ml b/lib/eval_concolic.ml
@@ -1,14 +1,14 @@
 module M = struct
-  type t = Value.t * Encoding.Expr.t
+  type t = Value.t * Smtml.Expr.t
   type st = t Store.t
 
   module Eval_concrete = Eval_concrete
   module Eval_symbolic = Eval_symbolic
-  module E = Encoding.Expr
-  module T = Encoding.Ty
-  module S = Encoding.Symbol
+  module E = Smtml.Expr
+  module T = Smtml.Ty
+  module S = Smtml.Symbol
 
-  let project_store (store : st) : Value.t Store.t * Encoding.Expr.t Store.t =
+  let project_store (store : st) : Value.t Store.t * Smtml.Expr.t Store.t =
     let key_values = Store.fold (fun k v z -> (k, fst v) :: z) store [] in
     let key_symbols = Store.fold (fun k v z -> (k, snd v) :: z) store [] in
     let concrete_store = Store.create_store key_values in
@@ -43,8 +43,8 @@ module M = struct
     let symbolic_name = Parameters.symbol_prefix ^ name in
     let symbolic_value =
       if String.equal "bool" tp then
-        E.mk_symbol (S.mk_symbol T.Ty_bool symbolic_name)
-      else E.mk_symbol (S.mk_symbol T.Ty_int symbolic_name)
+        E.mk_symbol (S.make T.Ty_bool symbolic_name)
+      else E.mk_symbol (S.make T.Ty_int symbolic_name)
     in
     let concrete_value =
       match Symb_map.map symbolic_name with
@@ -54,5 +54,5 @@ module M = struct
     Some (concrete_value, symbolic_value)
 end
 
-module M' : Eval_intf.M with type t = Value.t * Encoding.Expr.t = M
+module M' : Eval_intf.M with type t = Value.t * Smtml.Expr.t = M
 include M
diff --git a/lib/eval_symbolic.ml b/lib/eval_symbolic.ml
@@ -1,69 +1,59 @@
 module M = struct
   open Expr
-  module E = Encoding.Expr
-  module V = Encoding.Value
-  module T = Encoding.Ty
-  module Slv = Encoding.Solver
-  module S = Encoding.Symbol
+  module E = Smtml.Expr
+  module V = Smtml.Value
+  module Ty = Smtml.Ty
+  module Slv = Smtml.Solver
+  module S = Smtml.Symbol
 
   type t = E.t
   type st = t Store.t
 
   let solver = Slv.Z3_batch.create ()
 
-  let eval_unop (op : Expr.unop) =
-    match op with
-    | Expr.Neg -> (Some T.Neg, None)
-    | Expr.Not -> (Some T.Not, None)
-    | Expr.Abs -> (Some T.Abs, None)
-    | Expr.StringOfInt -> (None, Some T.String_from_int)
+  let eval_unop = function
+    | Expr.Not -> `Unary Ty.(Ty_bool, Not)
+    | Expr.Neg -> `Unary Ty.(Ty_int, Neg)
+    | Expr.Abs -> `Unary Ty.(Ty_int, Abs)
+    | Expr.StringOfInt -> `Cvtop Ty.(Ty_str, String_from_int)
 
-  let eval_binop (op : Expr.binop) =
-    match op with
-    | Expr.Plus -> (Some T.Add, None)
-    | Expr.Minus -> (Some T.Sub, None)
-    | Expr.Times -> (Some T.Mul, None)
-    | Expr.Div -> (Some T.Div, None)
-    | Expr.Modulo -> (Some T.Rem, None)
-    | Expr.Pow -> (Some T.Pow, None)
-    | Expr.Or -> (Some T.Or, None)
-    | Expr.And -> (Some T.And, None)
-    | Expr.Xor -> (Some T.Xor, None)
-    | Expr.ShiftL -> (Some T.Shl, None)
-    | Expr.ShiftR -> (Some T.ShrA, None)
-    | Expr.Gt -> (None, Some T.Gt)
-    | Expr.Lt -> (None, Some T.Lt)
-    | Expr.Gte -> (None, Some T.Ge)
-    | Expr.Lte -> (None, Some T.Le)
-    | Expr.Equals -> (None, Some T.Eq)
-    | Expr.NEquals -> (None, Some T.Ne)
+  let eval_binop = function
+    | Expr.Plus -> `Binary Ty.(Ty_int, Add)
+    | Expr.Minus -> `Binary Ty.(Ty_int, Sub)
+    | Expr.Times -> `Binary Ty.(Ty_int, Mul)
+    | Expr.Div -> `Binary Ty.(Ty_int, Div)
+    | Expr.Modulo -> `Binary Ty.(Ty_int, Rem)
+    | Expr.Pow -> `Binary Ty.(Ty_int, Pow)
+    | Expr.ShiftL -> `Binary Ty.(Ty_int, Shl)
+    | Expr.ShiftR -> `Binary Ty.(Ty_int, ShrA)
+    | Expr.Or -> `Binary Ty.(Ty_bool, Or)
+    | Expr.And -> `Binary Ty.(Ty_bool, And)
+    | Expr.Xor -> `Binary Ty.(Ty_bool, Xor)
+    | Expr.Gt -> `Relop Ty.(Ty_int, Gt)
+    | Expr.Lt -> `Relop Ty.(Ty_int, Lt)
+    | Expr.Gte -> `Relop Ty.(Ty_int, Ge)
+    | Expr.Lte -> `Relop Ty.(Ty_int, Le)
+    | Expr.Equals -> `Relop Ty.(Ty_bool, Eq)
+    | Expr.NEquals -> `Relop Ty.(Ty_bool, Ne)
 
   let rec eval (store : st) (e : Expr.t) : t =
     match e with
-    | Val (Integer n) -> E.(make @@ Val (V.Int n))
-    | Val (Boolean true) -> E.(make @@ Val V.True)
-    | Val (Boolean false) -> E.(make @@ Val V.False)
-    | Val (Loc n) -> E.(make @@ Val (V.Int n))
+    | Val (Integer n) -> E.value (V.Int n)
+    | Val (Boolean true) -> E.value V.True
+    | Val (Boolean false) -> E.value V.False
+    | Val (Loc n) -> E.value (V.Int n)
     | Var x -> Store.get store x
     | Unop (op, e) -> (
-      let op' = eval_unop op in
-      let e' = eval store e in
-      match op' with
-      | Some T.Not, None -> E.(unop T.Ty_bool T.Not e')
-      | Some u, None -> E.(unop T.Ty_int u e')
-      | None, Some c -> E.(cvtop T.Ty_int c e')
-      | _ -> assert false )
+      let e = eval store e in
+      match eval_unop op with
+      | `Unary (t, op) -> E.(unop t op e)
+      | `Cvtop (t, c) -> E.(cvtop t c e) )
     | Binop (op, e1, e2) -> (
-      let op' = eval_binop op in
-      let e1' = eval store e1 in
-      let e2' = eval store e2 in
-      match op' with
-      | Some T.Or, None -> E.(binop T.Ty_bool T.Or e1' e2')
-      | Some T.And, None -> E.(binop T.Ty_bool T.And e1' e2')
-      | Some T.Xor, None -> E.(binop T.Ty_bool T.Xor e1' e2')
-      | Some b, None -> E.(binop T.Ty_int b e1' e2')
-      | None, Some r -> E.(relop T.Ty_int r e1' e2')
-      | _ -> assert false )
+      let e1 = eval store e1 in
+      let e2 = eval store e2 in
+      match eval_binop op with
+      | `Binary (t, op) -> E.(binop t op e1 e2)
+      | `Relop (t, op) -> E.(relop t op e1 e2) )
     | B_symb _ ->
       failwith
         "InternalError: EvalSymbolic.eval, tried to evaluate a symbolic boolean"
@@ -73,7 +63,12 @@ module M = struct
     | Ite (_, _, _) -> failwith "InternalError: concrete Ite not implemented"
     | _ -> assert false
 
-  let is_true (exprs : t list) : bool = Slv.Z3_batch.check solver exprs
+  let is_true (exprs : t list) : bool =
+    match Slv.Z3_batch.check solver exprs with
+    | `Sat -> true
+    | `Unsat -> false
+    | `Unknown ->
+      failwith "InternalError: EvalSymbolic.is_true, Z3 returned unknown"
 
   let translate_value (v : V.t) : Value.t =
     match v with
@@ -96,20 +91,19 @@ module M = struct
     | Some m -> (true, Some (hashtbl_to_list m))
     | None -> (false, None)
 
-  let negate (e : t) : t = E.(unop T.Ty_bool T.Not e)
+  let negate (e : t) : t = E.(unop Ty.Ty_bool Ty.Not e)
   let pp (fmt : Fmt.t) (e : t) : unit = E.pp fmt e
   let to_string (e : t) : string = Fmt.asprintf "%a" pp e
   let print (e : t) : unit = to_string e |> print_endline
 
   let make_symbol (name : string) (tp : string) =
     let symb_name = Parameters.symbol_prefix ^ name in
     let symb_value =
-      if String.equal "bool" tp then
-        E.mk_symbol (S.mk_symbol T.Ty_bool symb_name)
-      else E.mk_symbol (S.mk_symbol T.Ty_int symb_name)
+      if String.equal "bool" tp then E.mk_symbol (S.make Ty.Ty_bool symb_name)
+      else E.mk_symbol (S.make Ty.Ty_int symb_name)
     in
     Some symb_value
 end
 
-module M' : Eval_intf.M with type t = Encoding.Expr.t = M
+module M' : Eval_intf.M with type t = Smtml.Expr.t = M
 include M
diff --git a/lib/heap/heap_array_fork.ml b/lib/heap/heap_array_fork.ml
@@ -1,7 +1,7 @@
-open Encoding
+open Smtml
 
 module M = struct
-  type value = Encoding.Expr.t
+  type value = Expr.t
   type block = value array
 
   type t =
@@ -84,7 +84,7 @@ module M = struct
         (fun index' _ ->
           (* can be optimized *)
           let e =
-            Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index')))
+            Expr.(relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int index')))
           in
           Eval_symbolic.is_true (e :: path) )
         temp
@@ -108,7 +108,7 @@ module M = struct
             let _ = Array.set newBlock index' v in
             let _ = Hashtbl.replace newHeap loc newBlock in
             let cond =
-              Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index')))
+              Expr.(relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int index')))
             in
             ({ heap with map = newHeap }, Pc.add_condition path cond) )
           blockList
@@ -117,7 +117,7 @@ module M = struct
         (fun index' _ ->
           (* can be optimized *)
           let e =
-            Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index')))
+            Expr.(relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int index')))
           in
           Eval_symbolic.is_true (e :: path) )
         temp
@@ -149,5 +149,5 @@ module M = struct
   let clone h = copy h
 end
 
-module M' : Heap_intf.M with type value = Encoding.Expr.t = M
+module M' : Heap_intf.M with type value = Expr.t = M
 include M
diff --git a/lib/heap/heap_arrayite.ml b/lib/heap/heap_arrayite.ml
@@ -1,7 +1,7 @@
-open Encoding
+open Smtml
 
 module M = struct
-  type value = Encoding.Expr.t
+  type value = Expr.t
   type block = value array
   type t = (int, block) Hashtbl.t * int
 
@@ -73,7 +73,7 @@ module M = struct
       let block' =
         Array.mapi
           (fun j old_expr ->
-            let e = Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int j))) in
+            let e = Expr.(relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int j))) in
             if Eval_symbolic.is_true (e :: path) then
               Expr.(Bool.ite e v old_expr)
             else old_expr )
@@ -111,14 +111,14 @@ module M = struct
                    (* can be optimized *)
                    let e =
                      Expr.(
-                       relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index')) )
+                       relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int index')) )
                    in
                    Eval_symbolic.is_true (e :: pc) )
                  (Array.to_list
                     (Array.mapi
                        (fun j e ->
                          ( Expr.(
-                             relop Ty.Ty_int Ty.Eq index (make @@ Val (Int j)) )
+                             relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int j)) )
                          , e ) )
                        arr ) ) )
           in
@@ -167,5 +167,5 @@ module M = struct
   let clone h = copy h
 end
 
-module M' : Heap_intf.M with type value = Encoding.Expr.t = M
+module M' : Heap_intf.M with type value = Expr.t = M
 include M
diff --git a/lib/heap/heap_concolic.ml b/lib/heap/heap_concolic.ml
@@ -1,6 +1,8 @@
+open Smtml
+
 module M = struct
   type value =
-    Value.t * Encoding.Expr.t (* indexes and sizes are always values *)
+    Value.t * Expr.t (* indexes and sizes are always values *)
 
   type block = value array
   type t = (int, block) Hashtbl.t
@@ -35,7 +37,7 @@ module M = struct
   let clone _ = assert false
 end
 
-module M' : Heap_intf.M with type value = Value.t * Encoding.Expr.t = M
+module M' : Heap_intf.M with type value = Value.t * Expr.t = M
 include M
 (*
 type t = (int, int arry) Hashtbl.t

diff --git a/lib/heap/heap_oplist.ml b/lib/heap/heap_oplist.ml
@@ -1,7 +1,7 @@
-open Encoding
+open Smtml
 
 module M = struct
-  type value = Encoding.Expr.t
+  type value = Expr.t
   type addr = int
   type size = value
   type op = value * value * value Pc.t
@@ -76,7 +76,7 @@ module M = struct
     let v =
       List.fold_left
         (fun ac (i, v, _) ->
-          Expr.(Bool.ite Expr.(relop Ty.Ty_int Ty.Eq index i) v ac) )
+          Expr.(Bool.ite Expr.(relop Ty.Ty_bool Ty.Eq index i) v ac) )
         Expr.(make @@ Val (Int 0))
         (List.rev ops)
     in
@@ -109,5 +109,5 @@ module M = struct
   let clone h = copy h
 end
 
-module M' : Heap_intf.M with type value = Encoding.Expr.t = M
+module M' : Heap_intf.M with type value = Expr.t = M
 include M
diff --git a/lib/heap/heap_symbolic.ml b/lib/heap/heap_symbolic.ml
@@ -1,5 +1,7 @@
+open Smtml
+
 module M = struct
-  type value = Encoding.Expr.t
+  type value = Expr.t
   type block = value array
   type t = (int, block) Hashtbl.t
 
@@ -34,7 +36,7 @@ module M = struct
   let clone _ = assert false
 end
 
-module M' : Heap_intf.M with type value = Encoding.Expr.t = M
+module M' : Heap_intf.M with type value = Expr.t = M
 include M
 (*
 type t = (int, int arry) Hashtbl.t

diff --git a/lib/heap/heap_tree.ml b/lib/heap/heap_tree.ml
@@ -1,7 +1,7 @@
-open Encoding
+open Smtml
 
 module M = struct
-  type value = Encoding.Expr.t
+  type value = Expr.t
   type range = value * value
 
   type tree_t =
@@ -239,5 +239,5 @@ module M = struct
   let clone h = copy h
 end
 
-module M' : Heap_intf.M with type value = Encoding.Expr.t = M
+module M' : Heap_intf.M with type value = Expr.t = M
 include M