From 4c2bad4ea7e2075f2c35c5f2550453c6ad4a8f68 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 24 Apr 2024 15:33:04 +0100 Subject: [PATCH] Upgrade `encoding` to latest `smtml` release --- bin/commands/cmd_execute.ml | 4 +- dune-project | 2 +- lib/dune | 2 +- lib/eval_concolic.ml | 16 +++--- lib/eval_symbolic.ml | 108 +++++++++++++++++------------------- lib/heap/heap_array_fork.ml | 12 ++-- lib/heap/heap_arrayite.ml | 12 ++-- lib/heap/heap_concolic.ml | 6 +- lib/heap/heap_oplist.ml | 8 +-- lib/heap/heap_symbolic.ml | 6 +- lib/heap/heap_tree.ml | 6 +- whilloc.opam | 5 +- whilloc.opam.template | 3 - 13 files changed, 91 insertions(+), 99 deletions(-) delete mode 100644 whilloc.opam.template diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml index 61a0008..e82c797 100644 --- a/bin/commands/cmd_execute.ml +++ b/bin/commands/cmd_execute.ml @@ -151,7 +151,7 @@ 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 @@ -159,7 +159,7 @@ let run ?(no_values = false) ?(test = false) input mode = ; 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 index 31e949e..94bcea0 100644 --- 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 index b14a274..5fe03d6 100644 --- 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 index b49c1e4..0ce3c68 100644 --- 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 index 6dcbf21..7c23cb6 100644 --- 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,7 +91,7 @@ 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 @@ -104,12 +99,11 @@ module M = struct 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 index 85474a4..bc9b958 100644 --- 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 index 766c8bd..e5f985f 100644 --- 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 index 36fa8d5..7d055c2 100644 --- 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 index ecfaadc..a8763ac 100644 --- 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 index 2e0432a..ea3e997 100644 --- 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 index 661753d..db7dcbc 100644 --- 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 diff --git a/whilloc.opam b/whilloc.opam index b8d9444..5d6ec53 100644 --- a/whilloc.opam +++ b/whilloc.opam @@ -17,7 +17,7 @@ depends: [ "bos" "cmdliner" "ppx_deriving_yojson" - "encoding" {= "dev"} + "smtml" {= "0.1.0"} "bisect_ppx" {with-test & >= "2.5.0"} "odoc" {with-doc} ] @@ -36,6 +36,3 @@ build: [ ] ] dev-repo: "git+https://github.com/formalsec/whilloc.git" -pin-depends: [ - [ "encoding.dev" "git+https://github.com/formalsec/encoding#25c6021256a995d84e62a358e51451bc710210f7"] -] \ No newline at end of file diff --git a/whilloc.opam.template b/whilloc.opam.template deleted file mode 100644 index e41c5d5..0000000 --- a/whilloc.opam.template +++ /dev/null @@ -1,3 +0,0 @@ -pin-depends: [ - [ "encoding.dev" "git+https://github.com/formalsec/encoding#25c6021256a995d84e62a358e51451bc710210f7"] -] \ No newline at end of file