From dfd4d64c16a5a338c9641b0b4dc55f6827ccd1bf Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 11 Mar 2024 14:15:51 +0000 Subject: [PATCH 1/4] add pp function --- lib/Heap/HeapTree.ml | 42 +++++++++++++++++++++++------------------- 1 file changed, 23 insertions(+), 19 deletions(-) diff --git a/lib/Heap/HeapTree.ml b/lib/Heap/HeapTree.ml index f06c841..c4ac067 100644 --- a/lib/Heap/HeapTree.ml +++ b/lib/Heap/HeapTree.ml @@ -1,33 +1,37 @@ module M : Heap_intf.M with type vt = Term.t = struct - type vt = Term.t [@@deriving yojson] - type range = vt * vt [@@deriving yojson] + type vt = Term.t + type range = vt * vt type tree_t = Leaf of range * vt | Node of range * tree_t list - [@@deriving yojson] type t = (int, tree_t) Hashtbl.t * int let init () : t = (Hashtbl.create Parameters.size, 0) - let pp (_fmt : Fmt.t) (_heap : t) : unit = - failwith "Not Implemented" + let rec pp_block (fmt : Fmt.t) (block : tree_t) : unit = + let open Fmt in + match block with + | Leaf ((l, r), v) -> + fprintf fmt "{ \"leaf\": { \"range\": \"[%a, %a]\", \"value\": \"%a\"} }" + Term.pp l + Term.pp r + Term.pp v + | Node ((l, r), ch) -> + fprintf fmt "{ \"node\": { \"range\": \"[%a, %a]\", \"children\": [ %a ]} }" + Term.pp l + Term.pp r + (pp_lst ~pp_sep:pp_comma pp_block) ch + + let pp (fmt : Fmt.t) ((heap, _) : t) : unit = + let open Fmt in + let pp_binding fmt (_, v) = fprintf fmt "%a" pp_block v in + fprintf fmt "%a" (pp_hashtbl ~pp_sep:pp_newline pp_binding) heap let tree_to_json (idx : int) (tree : tree_t) : unit = - let rec iter_tree (tree : tree_t) : string = - match tree with - | Leaf ((l, r), v) -> - "{ \"leaf\": { \"range\": \"[" ^ Term.to_string l ^ ", " - ^ Term.to_string r ^ "[\", \"value\": " ^ "\"" ^ Term.to_string v - ^ "\"" ^ " } }" - | Node ((l, r), ch) -> - "{ \"node\": { \"range\": \"[" ^ Term.to_string l ^ ", " - ^ Term.to_string r ^ "[\", \"children\": " ^ "[ " - ^ String.concat ", " (List.map iter_tree ch) - ^ " ]" ^ " } }" - in let f = open_out ("output/" ^ string_of_int idx ^ "_tree.json") in - let tree_json = iter_tree tree in - Printf.fprintf f "%s\n" tree_json + let tree_json = Format.asprintf "%a" pp_block tree in + Printf.fprintf f "%s\n" tree_json; + close_out f let to_string (h : t) : string = let h', _ = h in From 9a7d69249ebc93d92f336f7e3b3c7fdfbe47f773 Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 11 Mar 2024 14:35:42 +0000 Subject: [PATCH 2/4] rename files --- bin/commands/cmd_execute.ml | 26 +++---- lib/BinaryTree.ml | 67 ------------------- lib/Heap/heap_intf.ml | 14 ---- lib/{BFS.ml => bfs.ml} | 0 lib/{Callstack.ml => callstack.ml} | 0 lib/choice_intf.ml | 2 +- lib/{DFS.ml => dfs.ml} | 0 lib/{EvalConcolic.ml => eval_concolic.ml} | 16 ++--- lib/{EvalConcrete.ml => eval_concrete.ml} | 14 ++-- lib/{EvalExpression.ml => eval_expression.ml} | 0 lib/{EvalSymbolic.ml => eval_symbolic.ml} | 6 +- .../heap_array_fork.ml} | 20 +++--- .../HeapArrayITE.ml => heap/heap_arrayite.ml} | 16 ++--- .../HeapConcolic.ml => heap/heap_concolic.ml} | 12 ++-- .../HeapConcrete.ml => heap/heap_concrete.ml} | 14 ++-- lib/heap/heap_intf.ml | 14 ++++ .../HeapOpList.ml => heap/heap_oplist.ml} | 16 ++--- .../HeapSymbolic.ml => heap/heap_symbolic.ml} | 14 ++-- lib/{Heap/HeapTree.ml => heap/heap_tree.ml} | 24 +++---- lib/interpreter.ml | 20 +++--- lib/interpreter_intf.ml | 2 +- lib/{ListChoice.ml => list_choice.ml} | 12 ++-- lib/{Operations.ml => operations.ml} | 0 lib/{Outcome.ml => outcome.ml} | 0 lib/{Parameters.ml => parameters.ml} | 0 lib/{PC.ml => pc.ml} | 0 lib/{Program.ml => program.ml} | 0 lib/{Return.ml => return.ml} | 4 +- lib/{SState.ml => sstate.ml} | 4 +- lib/{State.ml => state.ml} | 6 +- lib/{Store.ml => store.ml} | 0 lib/{SymbMap.ml => symb_map.ml} | 0 lib/{Utils.ml => utils.ml} | 0 lib/{Value.ml => value.ml} | 0 34 files changed, 128 insertions(+), 195 deletions(-) delete mode 100644 lib/BinaryTree.ml delete mode 100644 lib/Heap/heap_intf.ml rename lib/{BFS.ml => bfs.ml} (100%) rename lib/{Callstack.ml => callstack.ml} (100%) rename lib/{DFS.ml => dfs.ml} (100%) rename lib/{EvalConcolic.ml => eval_concolic.ml} (78%) rename lib/{EvalConcrete.ml => eval_concrete.ml} (75%) rename lib/{EvalExpression.ml => eval_expression.ml} (100%) rename lib/{EvalSymbolic.ml => eval_symbolic.ml} (93%) rename lib/{Heap/HeapArrayFork.ml => heap/heap_array_fork.ml} (87%) rename lib/{Heap/HeapArrayITE.ml => heap/heap_arrayite.ml} (92%) rename lib/{Heap/HeapConcolic.ml => heap/heap_concolic.ml} (70%) rename lib/{Heap/HeapConcrete.ml => heap/heap_concrete.ml} (90%) create mode 100644 lib/heap/heap_intf.ml rename lib/{Heap/HeapOpList.ml => heap/heap_oplist.ml} (86%) rename lib/{Heap/HeapSymbolic.ml => heap/heap_symbolic.ml} (68%) rename lib/{Heap/HeapTree.ml => heap/heap_tree.ml} (90%) rename lib/{ListChoice.ml => list_choice.ml} (79%) rename lib/{Operations.ml => operations.ml} (100%) rename lib/{Outcome.ml => outcome.ml} (100%) rename lib/{Parameters.ml => parameters.ml} (100%) rename lib/{PC.ml => pc.ml} (100%) rename lib/{Program.ml => program.ml} (100%) rename lib/{Return.ml => return.ml} (89%) rename lib/{SState.ml => sstate.ml} (96%) rename lib/{State.ml => state.ml} (92%) rename lib/{Store.ml => store.ml} (100%) rename lib/{SymbMap.ml => symb_map.ml} (100%) rename lib/{Utils.ml => utils.ml} (100%) rename lib/{Value.ml => value.ml} (100%) diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml index 0f6e379..7834870 100644 --- a/bin/commands/cmd_execute.ml +++ b/bin/commands/cmd_execute.ml @@ -1,22 +1,22 @@ open Whilloc open Utils -module C_Choice = ListChoice.Make (EvalConcrete.M) (HeapConcrete.M) -module SAF_Choice = ListChoice.Make (EvalSymbolic.M) (HeapArrayFork.M) -module SAITE_Choice = ListChoice.Make (EvalSymbolic.M) (HeapArrayITE.M) -module ST_Choice = ListChoice.Make (EvalSymbolic.M) (HeapTree.M) -module SOPL_Choice = ListChoice.Make (EvalSymbolic.M) (HeapOpList.M) -module C = Interpreter.Make (EvalConcrete.M) (DFS.M) (HeapConcrete.M) (C_Choice) -module SAF = - Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapArrayFork.M) (SAF_Choice) +(* Choice *) +module C_Choice = List_choice.Make (Eval_concrete.M) (Heap_concrete.M) +module SAF_Choice = List_choice.Make (Eval_symbolic.M) (Heap_array_fork.M) +module SAITE_Choice = List_choice.Make (Eval_symbolic.M) (Heap_arrayite.M) +module ST_Choice = List_choice.Make (Eval_symbolic.M) (Heap_tree.M) +module SOPL_Choice = List_choice.Make (Eval_symbolic.M) (Heap_oplist.M) +(* Interpreter *) +module C = Interpreter.Make (Eval_concrete.M) (Dfs.M) (Heap_concrete.M) (C_Choice) +module SAF = + Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_array_fork.M) (SAF_Choice) module SAITE = - Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapArrayITE.M) (SAITE_Choice) - -module ST = Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapTree.M) (ST_Choice) - + Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_arrayite.M) (SAITE_Choice) +module ST = Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_tree.M) (ST_Choice) module SOPL = - Interpreter.Make (EvalSymbolic.M) (DFS.M) (HeapOpList.M) (SOPL_Choice) + Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_oplist.M) (SOPL_Choice) type mode = Concrete | Saf | Saite | St | Sopl [@@deriving yojson] diff --git a/lib/BinaryTree.ml b/lib/BinaryTree.ml deleted file mode 100644 index 574fdba..0000000 --- a/lib/BinaryTree.ml +++ /dev/null @@ -1,67 +0,0 @@ -type 'a t = Nil | Node of 'a * 'a t * 'a t - -let rec fold_tree (f : 'b -> 'a -> 'a -> 'a) (e : 'a) (tree : 'b t) : 'a = - match tree with - | Nil -> e - | Node (x, left, right) -> f x (fold_tree f e left) (fold_tree f e right) - -let size (tree : 'a t) = fold_tree (fun _ l r -> 1 + l + r) 0 tree -let depth (tree : 'a t) = fold_tree (fun _ l r -> 1 + max l r) 0 tree -let preorder (tree : 'a t) = fold_tree (fun x l r -> [ x ] @ l @ r) [] tree - -let string_of_tree_preorder (f : 'a -> string) (tree : 'a t) = - List.map f (preorder tree) - -let rec add_left (tree : 'a t) (x : 'a) : 'a t = - let subtree = Node (x, Nil, Nil) in - match tree with - | Nil -> subtree - | Node (v, left, right) when left == Nil -> Node (v, subtree, right) - | Node (v, left, right) when right == Nil -> Node (v, left, subtree) - | Node (v, left, right) -> Node (v, add_left left x, right) - -let rec add_right (tree : 'a t) (x : 'a) : 'a t = - let subtree = Node (x, Nil, Nil) in - match tree with - | Nil -> subtree - | Node (v, left, right) when right == Nil -> Node (v, left, subtree) - | Node (v, left, right) when left == Nil -> Node (v, subtree, right) - | Node (v, left, right) -> Node (v, left, add_right right x) - -let rec string_of_tree (prefix : string) (is_left : bool) (f : 'a -> string) - (tree : 'a t) : string = - match tree with - | Nil -> "" - | Node (x, l, r) -> - let helper, next_prefix = - if is_left then ("├──", "│ ") else ("└──", " ") - in - prefix ^ helper ^ f x ^ "\n" - ^ string_of_tree (prefix ^ next_prefix) true f l - ^ string_of_tree (prefix ^ next_prefix) false f r - -let print_tree (f : 'a -> string) (tree : 'a t) : unit = - print_endline (string_of_tree "" false f tree) - -(* use program lines to simultaneously identify each node of the graph and its statement *) -(* https://stackoverflow.com/questions/3455389/graphviz-tree-layout *) -(* https://graphviz.org/docs/attrs/fontsize/ *) -(* https://dreampuf.github.io/GraphvizOnline *) -let to_graphviz (f : 'a -> string) (tree : 'a t) : string = - let header = - "strict graph {\n\ - \ size=\"6,6\";\n\ - \ node [color=lightblue2, style=filled];\n\n\ - \ " - in - let rec aux = function - | Nil -> "" - | Node (x, (Node (xl, _, _) as left), (Node (xr, _, _) as right)) -> - (f x ^ " -- {" ^ f xl ^ " " ^ f xr ^ "}\n ") ^ aux left ^ aux right - | Node (x, (Node (xl, _, _) as left), Nil) -> - (f x ^ " -- {" ^ f xl ^ "}\n ") ^ aux left - | Node (x, Nil, (Node (xr, _, _) as right)) -> - (f x ^ " -- {" ^ f xr ^ "}\n ") ^ aux right - | Node (x, Nil, Nil) -> f x ^ "\n " - in - header ^ aux tree ^ "}" diff --git a/lib/Heap/heap_intf.ml b/lib/Heap/heap_intf.ml deleted file mode 100644 index b2e176c..0000000 --- a/lib/Heap/heap_intf.ml +++ /dev/null @@ -1,14 +0,0 @@ -module type M = sig - type t (* the representation of the heap itself *) - type vt (* the type of the index and size of the arrays *) - - val init : unit -> t - val pp : Fmt.t -> t -> unit - val to_string : t -> string - val malloc : t -> vt -> vt PC.t -> (t * vt * vt PC.t) list - val lookup : t -> vt -> vt -> vt PC.t -> (t * vt * vt PC.t) list - val update : t -> vt -> vt -> vt -> vt PC.t -> (t * vt PC.t) list - val free : t -> vt -> vt PC.t -> (t * vt PC.t) list - val in_bounds : t -> vt -> vt -> vt PC.t -> bool - val clone : t -> t -end diff --git a/lib/BFS.ml b/lib/bfs.ml similarity index 100% rename from lib/BFS.ml rename to lib/bfs.ml diff --git a/lib/Callstack.ml b/lib/callstack.ml similarity index 100% rename from lib/Callstack.ml rename to lib/callstack.ml diff --git a/lib/choice_intf.ml b/lib/choice_intf.ml index afd3549..6f66c84 100644 --- a/lib/choice_intf.ml +++ b/lib/choice_intf.ml @@ -2,7 +2,7 @@ module type Choice = sig type 'a t type v type h - type state = (v, h) SState.t + type state = (v, h) Sstate.t val return : 'a -> 'a t val bind : 'a t -> ('a -> 'b t) -> 'b t diff --git a/lib/DFS.ml b/lib/dfs.ml similarity index 100% rename from lib/DFS.ml rename to lib/dfs.ml diff --git a/lib/EvalConcolic.ml b/lib/eval_concolic.ml similarity index 78% rename from lib/EvalConcolic.ml rename to lib/eval_concolic.ml index ee46bd8..1f28d98 100644 --- a/lib/EvalConcolic.ml +++ b/lib/eval_concolic.ml @@ -2,8 +2,8 @@ module M : Eval_intf.M with type t = Value.t * Term.t = struct type t = Value.t * Term.t type st = t Store.t - module EvalConcrete = EvalConcrete.M - module EvalSymbolic = EvalSymbolic.M + module Eval_concrete = Eval_concrete.M + module Eval_symbolic = Eval_symbolic.M let project_store (store : st) : Value.t Store.t * Term.t Store.t = let key_values = Store.fold (fun k v z -> (k, fst v) :: z) store [] in @@ -14,23 +14,23 @@ module M : Eval_intf.M with type t = Value.t * Term.t = struct let eval (store : st) (e : Term.t) : t = let cstore, sstore = project_store store in - (EvalConcrete.eval cstore e, EvalSymbolic.eval sstore e) + (Eval_concrete.eval cstore e, Eval_symbolic.eval sstore e) let is_true (exprs : t list) : bool = let v, _ = List.split exprs in - EvalConcrete.is_true v + Eval_concrete.is_true v let test_assert (exprs : t list) : bool * Model.t = let _, e = List.split exprs in - EvalSymbolic.test_assert e + Eval_symbolic.test_assert e let negate (e : t) : t = let value, expression = e in - (EvalConcrete.negate value, EvalSymbolic.negate expression) + (Eval_concrete.negate value, Eval_symbolic.negate expression) let pp (fmt : Fmt.t) (e : t) : unit = let value, expression = e in - Format.fprintf fmt "(%a, %a)" EvalConcrete.pp value EvalSymbolic.pp + Format.fprintf fmt "(%a, %a)" Eval_concrete.pp value Eval_symbolic.pp expression let to_string (e : t) : string = Format.asprintf "%a" pp e @@ -43,7 +43,7 @@ module M : Eval_intf.M with type t = Value.t * Term.t = struct else Term.make_symb_int symbolic_name in let concrete_value = - match SymbMap.map symbolic_name with + match Symb_map.map symbolic_name with | None -> Value.Integer (Utils.random_int ()) | Some v -> v in diff --git a/lib/EvalConcrete.ml b/lib/eval_concrete.ml similarity index 75% rename from lib/EvalConcrete.ml rename to lib/eval_concrete.ml index d29381e..22cced8 100644 --- a/lib/EvalConcrete.ml +++ b/lib/eval_concrete.ml @@ -1,5 +1,5 @@ module M : Eval_intf.M with type t = Value.t = struct - open EvalExpression + open Eval_expression type t = Value.t type st = t Store.t @@ -12,11 +12,11 @@ module M : Eval_intf.M with type t = Value.t = struct | Binop (op, e1, e2) -> eval_binop_expr op (eval store e1) (eval store e2) | B_symb s -> failwith - ("InternalError: EvalConcrete.eval, tried to evaluate a symbolic \ + ("InternalError: Eval_concrete.eval, tried to evaluate a symbolic \ expression" ^ s ^ "in a concrete execution context") | I_symb s -> failwith - ("InternalError: EvalConcrete.eval, tried to evaluate a symbolic \ + ("InternalError: Eval_concrete.eval, tried to evaluate a symbolic \ expression" ^ s ^ "in a concrete execution context") | Ite (e1, e2, e3) -> eval_ite e1 e2 e3 @@ -25,18 +25,18 @@ module M : Eval_intf.M with type t = Value.t = struct try List.hd v with _ -> failwith - "InternalError: EvalConcrete.is_true, tried to evaluate an empty \ + "InternalError: Eval_concrete.is_true, tried to evaluate an empty \ list of values" in match v' with | Boolean b -> b | Integer _ -> failwith - "InternalError: EvalConcrete.is_true, guard expressions must be of \ + "InternalError: Eval_concrete.is_true, guard expressions must be of \ type boolean" | Loc l -> failwith - ("InternalError: EvalConcrete.is_true, location value " + ("InternalError: Eval_concrete.is_true, location value " ^ string_of_int l ^ " cannot be evaluated to true or false in concrete evaluation \ contexts") @@ -50,7 +50,7 @@ module M : Eval_intf.M with type t = Value.t = struct | Boolean false -> Boolean true | _ -> failwith - "InternalError: EvalConcrete.negate, tried to negate a non boolean \ + "InternalError: Eval_concrete.negate, tried to negate a non boolean \ value" let pp (fmt : Fmt.t) (v : t) : unit = Value.pp fmt v diff --git a/lib/EvalExpression.ml b/lib/eval_expression.ml similarity index 100% rename from lib/EvalExpression.ml rename to lib/eval_expression.ml diff --git a/lib/EvalSymbolic.ml b/lib/eval_symbolic.ml similarity index 93% rename from lib/EvalSymbolic.ml rename to lib/eval_symbolic.ml index c4d1471..42c71d9 100644 --- a/lib/EvalSymbolic.ml +++ b/lib/eval_symbolic.ml @@ -1,5 +1,5 @@ module M : Eval_intf.M with type t = Term.t = struct - open EvalExpression + open Eval_expression open Term type t = Term.t @@ -45,11 +45,11 @@ module M : Eval_intf.M with type t = Term.t = struct (eval store e2 |> get_val)) | B_symb _ -> failwith - "InternalError: EvalSymbolic.eval, tried to evaluate a symbolic \ + "InternalError: Eval_symbolic.eval, tried to evaluate a symbolic \ boolean" | I_symb _ -> failwith - "InternalError: EvalSymbolic.eval, tried to evaluate a symbolic \ + "InternalError: Eval_symbolic.eval, tried to evaluate a symbolic \ integer" | Ite (_, _, _) -> failwith "InternalError: concrete Ite not implemented" diff --git a/lib/Heap/HeapArrayFork.ml b/lib/heap/heap_array_fork.ml similarity index 87% rename from lib/Heap/HeapArrayFork.ml rename to lib/heap/heap_array_fork.ml index 4a92b62..a0a333b 100644 --- a/lib/Heap/HeapArrayFork.ml +++ b/lib/heap/heap_array_fork.ml @@ -18,14 +18,14 @@ module M : Heap_intf.M with type vt = Term.t = struct let to_string (heap : t) : string = Format.asprintf "%a" pp heap - let is_within (sz : int) (index : vt) (pc : vt PC.t) : bool = + let is_within (sz : int) (index : vt) (pc : vt Pc.t) : bool = let e1 = Term.Binop (Lt, index, Val (Value.Integer 0)) in let e2 = Term.Binop (Gte, index, Val (Value.Integer sz)) in let e3 = Term.Binop (Or, e1, e2) in not (Translator.is_sat ([ e3 ] @ pc)) - let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt PC.t) : bool = + let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = match arr with | Val (Loc l) -> ( match Hashtbl.find_opt heap.map l with @@ -48,7 +48,7 @@ module M : Heap_intf.M with type vt = Term.t = struct | None -> failwith "Block does not exist") | _ -> failwith "Location needs to be a concrete value" - let malloc (heap : t) (size : vt) (path : vt PC.t) : (t * vt * vt PC.t) list = + let malloc (heap : t) (size : vt) (path : vt Pc.t) : (t * vt * vt Pc.t) list = match size with | Val (Integer size') -> let block = Array.make size' (Val (Integer 0)) in @@ -56,8 +56,8 @@ module M : Heap_intf.M with type vt = Term.t = struct [ ({ heap with i = heap.i + 1 }, Val (Loc heap.i), path) ] | _ -> failwith "Size needs to be a concrete integer" - let lookup (heap : t) (loc : vt) (index : vt) (path : vt PC.t) : - (t * vt * vt PC.t) list = + let lookup (heap : t) (loc : vt) (index : vt) (path : vt Pc.t) : + (t * vt * vt Pc.t) list = let _, block = find_block heap loc in match index with | Val (Integer index') -> @@ -69,7 +69,7 @@ module M : Heap_intf.M with type vt = Term.t = struct List.mapi (fun index' expr -> let cond = Binop (Equals, I_symb sym, Val (Integer index')) in - (copy heap, expr, PC.add_condition path cond)) + (copy heap, expr, Pc.add_condition path cond)) blockList in List.filteri @@ -80,8 +80,8 @@ module M : Heap_intf.M with type vt = Term.t = struct temp | _ -> failwith "Invalid index" - let update (heap : t) (loc : vt) (index : vt) (v : vt) (path : vt PC.t) : - (t * vt PC.t) list = + let update (heap : t) (loc : vt) (index : vt) (v : vt) (path : vt Pc.t) : + (t * vt Pc.t) list = let loc, block = find_block heap loc in match index with | Val (Integer index') -> @@ -98,7 +98,7 @@ module M : Heap_intf.M with type vt = Term.t = struct let _ = Array.set newBlock index' v in let _ = Hashtbl.replace newHeap loc newBlock in let cond = Binop (Equals, I_symb sym, Val (Integer index')) in - ({ heap with map = newHeap }, PC.add_condition path cond)) + ({ heap with map = newHeap }, Pc.add_condition path cond)) blockList in List.filteri @@ -109,7 +109,7 @@ module M : Heap_intf.M with type vt = Term.t = struct temp | _ -> failwith "Invalid index" - let free (heap : t) (loc : vt) (path : vt PC.t) : (t * vt PC.t) list = + let free (heap : t) (loc : vt) (path : vt Pc.t) : (t * vt Pc.t) list = let loc', _ = find_block heap loc in let _ = Hashtbl.remove heap.map loc' in [ (heap, path) ] diff --git a/lib/Heap/HeapArrayITE.ml b/lib/heap/heap_arrayite.ml similarity index 92% rename from lib/Heap/HeapArrayITE.ml rename to lib/heap/heap_arrayite.ml index 357f97d..9c62fe6 100644 --- a/lib/Heap/HeapArrayITE.ml +++ b/lib/heap/heap_arrayite.ml @@ -17,14 +17,14 @@ module M : Heap_intf.M with type vt = Term.t = struct let to_string (heap : t) : string = Format.asprintf "%a" pp heap - let is_within (sz : int) (index : vt) (pc : vt PC.t) : bool = + let is_within (sz : int) (index : vt) (pc : vt Pc.t) : bool = let e1 = Term.Binop (Lt, index, Val (Value.Integer 0)) in let e2 = Term.Binop (Gte, index, Val (Value.Integer sz)) in let e3 = Term.Binop (Or, e1, e2) in not (Translator.is_sat (e3 :: pc)) - let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt PC.t) : bool = + let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = let h, _ = heap in match arr with | Val (Loc l) -> ( @@ -49,7 +49,7 @@ module M : Heap_intf.M with type vt = Term.t = struct | None -> failwith "Block does not exist") | _ -> failwith "Location needs to be a concrete value" - let malloc (h : t) (sz : vt) (pc : vt PC.t) : (t * vt * vt PC.t) list = + let malloc (h : t) (sz : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let tbl, next = h in match sz with | Val (Integer i) -> @@ -58,8 +58,8 @@ module M : Heap_intf.M with type vt = Term.t = struct | _ -> failwith "InternalError: HeapArrayIte.malloc, size must be an integer" - let update (heap : t) (loc : vt) (index : vt) (v : vt) (path : vt PC.t) : - (t * vt PC.t) list = + let update (heap : t) (loc : vt) (index : vt) (v : vt) (path : vt Pc.t) : + (t * vt Pc.t) list = let heap', curr = heap in let loc, block = find_block heap loc in match index with @@ -80,8 +80,8 @@ module M : Heap_intf.M with type vt = Term.t = struct [ ((heap', curr), path) ] | _ -> failwith "Invalid index" - let lookup (h : t) (arr : vt) (index : vt) (pc : vt PC.t) : - (t * vt * vt PC.t) list = + let lookup (h : t) (arr : vt) (index : vt) (pc : vt Pc.t) : + (t * vt * vt Pc.t) list = let tbl, _ = h in match index with | Val (Integer i) -> ( @@ -131,7 +131,7 @@ module M : Heap_intf.M with type vt = Term.t = struct failwith "InternalError: HeapArrayIte.update, arr must be a location") - let free (h : t) (arr : vt) (pc : vt PC.t) : (t * vt PC.t) list = + let free (h : t) (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = let tbl, _ = h in match arr with | Val (Loc l) -> ( diff --git a/lib/Heap/HeapConcolic.ml b/lib/heap/heap_concolic.ml similarity index 70% rename from lib/Heap/HeapConcolic.ml rename to lib/heap/heap_concolic.ml index a5bf10a..da8d5db 100644 --- a/lib/Heap/HeapConcolic.ml +++ b/lib/heap/heap_concolic.ml @@ -10,21 +10,21 @@ module M = struct let to_string (_h : t) : string = failwith "Not Implemented" - let malloc _h (_sz : vt) (_pc : vt PC.t) : (t * vt * vt PC.t) list = + let malloc _h (_sz : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = [] - let update _h (_arr : vt) (_index : vt) (_v : vt) (_pc : vt PC.t) : - (t * vt PC.t) list = + let update _h (_arr : vt) (_index : vt) (_v : vt) (_pc : vt Pc.t) : + (t * vt Pc.t) list = [] - let lookup _h (_arr : vt) (_index : vt) (_pc : vt PC.t) : (t * vt * vt PC.t) list + let lookup _h (_arr : vt) (_index : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = [] - let free _h (_arr : vt) (_pc : vt PC.t) : (t * vt PC.t) list = + let free _h (_arr : vt) (_pc : vt Pc.t) : (t * vt Pc.t) list = [] - let in_bounds (_heap : t) (_v : vt) (_i : vt) (_pc : vt PC.t) : bool = + let in_bounds (_heap : t) (_v : vt) (_i : vt) (_pc : vt Pc.t) : bool = failwith "not implemented" let clone _ = assert false diff --git a/lib/Heap/HeapConcrete.ml b/lib/heap/heap_concrete.ml similarity index 90% rename from lib/Heap/HeapConcrete.ml rename to lib/heap/heap_concrete.ml index 7cfaaf5..81f207d 100644 --- a/lib/Heap/HeapConcrete.ml +++ b/lib/heap/heap_concrete.ml @@ -17,7 +17,7 @@ module M : Heap_intf.M with type vt = Value.t = struct let to_string (heap : t) : string = Format.asprintf "%a" pp heap - let malloc (h : t) (sz : vt) (pc : vt PC.t) : (t * vt * vt PC.t) list = + let malloc (h : t) (sz : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let tbl, next = h in match sz with | Integer i -> @@ -26,8 +26,8 @@ module M : Heap_intf.M with type vt = Value.t = struct | _ -> failwith "InternalError: HeapConcrete.malloc, size must be an integer" - let update (h : t) (arr : vt) (index : vt) (v : vt) (pc : vt PC.t) : - (t * vt PC.t) list = + let update (h : t) (arr : vt) (index : vt) (v : vt) (pc : vt Pc.t) : + (t * vt Pc.t) list = let tbl, _ = h in match (arr, index) with | Loc l, Integer i -> ( @@ -41,8 +41,8 @@ module M : Heap_intf.M with type vt = Value.t = struct "InternalError: HeapConcrete.update, arr must be location and index \ must be an integer" - let lookup (h : t) (arr : vt) (index : vt) (pc : vt PC.t) : - (t * vt * vt PC.t) list = + let lookup (h : t) (arr : vt) (index : vt) (pc : vt Pc.t) : + (t * vt * vt Pc.t) list = let tbl, _ = h in match (arr, index) with | Loc l, Integer i -> ( @@ -57,7 +57,7 @@ module M : Heap_intf.M with type vt = Value.t = struct "InternalError: HeapConcrete.update, arr must be location and index \ must be an integer" - let free (h : t) (arr : vt) (pc : vt PC.t) : (t * vt PC.t) list = + let free (h : t) (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = let tbl, _ = h in match arr with | Loc l -> ( @@ -68,7 +68,7 @@ module M : Heap_intf.M with type vt = Value.t = struct | _ -> failwith "InternalError: illegal free") | _ -> failwith "InternalError: HeapConcrete.update, arr must be location" - let in_bounds (heap : t) (addr : vt) (i : vt) (_pc : vt PC.t) : bool = + let in_bounds (heap : t) (addr : vt) (i : vt) (_pc : vt Pc.t) : bool = match addr with | Loc l -> ( let tbl, _ = heap in diff --git a/lib/heap/heap_intf.ml b/lib/heap/heap_intf.ml new file mode 100644 index 0000000..62cf1bf --- /dev/null +++ b/lib/heap/heap_intf.ml @@ -0,0 +1,14 @@ +module type M = sig + type t (* the representation of the heap itself *) + type vt (* the type of the index and size of the arrays *) + + val init : unit -> t + val pp : Fmt.t -> t -> unit + val to_string : t -> string + val malloc : t -> vt -> vt Pc.t -> (t * vt * vt Pc.t) list + val lookup : t -> vt -> vt -> vt Pc.t -> (t * vt * vt Pc.t) list + val update : t -> vt -> vt -> vt -> vt Pc.t -> (t * vt Pc.t) list + val free : t -> vt -> vt Pc.t -> (t * vt Pc.t) list + val in_bounds : t -> vt -> vt -> vt Pc.t -> bool + val clone : t -> t +end diff --git a/lib/Heap/HeapOpList.ml b/lib/heap/heap_oplist.ml similarity index 86% rename from lib/Heap/HeapOpList.ml rename to lib/heap/heap_oplist.ml index aa07ff9..3ae63cb 100644 --- a/lib/Heap/HeapOpList.ml +++ b/lib/heap/heap_oplist.ml @@ -1,7 +1,7 @@ module M : Heap_intf.M with type vt = Term.t = struct type addr = int type size = Term.t - type op = Term.t * Term.t * Term.t PC.t + type op = Term.t * Term.t * Term.t Pc.t type t = { map : (addr, size * op list) Hashtbl.t; mutable next : int } type vt = Term.t @@ -20,14 +20,14 @@ module M : Heap_intf.M with type vt = Term.t = struct let to_string (heap : t) : string = Fmt.asprintf "%a" pp heap - let is_within (sz : vt) (index : vt) (pc : vt PC.t) : bool = + let is_within (sz : vt) (index : vt) (pc : vt Pc.t) : bool = let e1 = Term.Binop (Lt, index, Val (Value.Integer 0)) in let e2 = Term.Binop (Gte, index, sz) in let e3 = Term.Binop (Or, e1, e2) in not (Translator.is_sat ([ e3 ] @ pc)) - let in_bounds (heap : t) (v : vt) (i : vt) (pc : vt PC.t) : bool = + let in_bounds (heap : t) (v : vt) (i : vt) (pc : vt Pc.t) : bool = match v with | Val (Loc l) -> ( match Hashtbl.find_opt heap.map l with @@ -43,14 +43,14 @@ module M : Heap_intf.M with type vt = Term.t = struct the heap") | _ -> failwith "InternalError: HeapOpList.in_bounds, v must be location" - let malloc (h : t) (sz : vt) (pc : vt PC.t) : (t * vt * vt PC.t) list = + let malloc (h : t) (sz : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let next = h.next in Hashtbl.add h.map next (sz, []); h.next <- h.next + 1; [ (h, Val (Loc next), pc) ] - let update (h : t) (arr : vt) (index : vt) (v : vt) (pc : vt PC.t) : - (t * vt PC.t) list = + let update (h : t) (arr : vt) (index : vt) (v : vt) (pc : vt Pc.t) : + (t * vt Pc.t) list = let lbl = match arr with Val (Loc i) -> i | _ -> assert false in let arr' = Hashtbl.find_opt h.map lbl in let f ((sz, oplist) : size * op list) : unit = @@ -59,7 +59,7 @@ module M : Heap_intf.M with type vt = Term.t = struct Option.fold ~none:() ~some:f arr'; [ (h, pc) ] - let lookup h (arr : vt) (index : vt) (pc : vt PC.t) : (t * vt * vt PC.t) list + let lookup h (arr : vt) (index : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let lbl = match arr with Val (Loc i) -> i | _ -> assert false in let arr' = Hashtbl.find h.map lbl in @@ -72,7 +72,7 @@ module M : Heap_intf.M with type vt = Term.t = struct in [ (h, v, pc) ] - let free h (arr : vt) (pc : vt PC.t) : (t * vt PC.t) list = + let free h (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = let lbl = match arr with Val (Loc i) -> i | _ -> assert false in Hashtbl.remove h.map lbl; [ (h, pc) ] diff --git a/lib/Heap/HeapSymbolic.ml b/lib/heap/heap_symbolic.ml similarity index 68% rename from lib/Heap/HeapSymbolic.ml rename to lib/heap/heap_symbolic.ml index 7116705..64faaf5 100644 --- a/lib/Heap/HeapSymbolic.ml +++ b/lib/heap/heap_symbolic.ml @@ -10,20 +10,20 @@ module M : Heap_intf.M with type vt = Term.t = struct let to_string (_h : t) : string = failwith "Not Implemented" - let malloc _h (_sz : vt) (_pc : vt PC.t) : (t * vt * vt PC.t) list = + let malloc _h (_sz : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = assert false - let update _h (_arr : vt) (_index : vt) (_v : vt) (_pc : vt PC.t) : - (t * vt PC.t) list = + let update _h (_arr : vt) (_index : vt) (_v : vt) (_pc : vt Pc.t) : + (t * vt Pc.t) list = assert false - let lookup _h (_arr : vt) (_index : vt) (_pc : vt PC.t) : - (t * vt * vt PC.t) list = + let lookup _h (_arr : vt) (_index : vt) (_pc : vt Pc.t) : + (t * vt * vt Pc.t) list = assert false - let free _h (_arr : vt) (_pc : vt PC.t) : (t * vt PC.t) list = assert false + let free _h (_arr : vt) (_pc : vt Pc.t) : (t * vt Pc.t) list = assert false - let in_bounds (_heap : t) (_v : vt) (_i : vt) (_pc : vt PC.t) : bool = + let in_bounds (_heap : t) (_v : vt) (_i : vt) (_pc : vt Pc.t) : bool = assert false let clone _ = assert false diff --git a/lib/Heap/HeapTree.ml b/lib/heap/heap_tree.ml similarity index 90% rename from lib/Heap/HeapTree.ml rename to lib/heap/heap_tree.ml index c4ac067..5ef5d64 100644 --- a/lib/Heap/HeapTree.ml +++ b/lib/heap/heap_tree.ml @@ -38,17 +38,17 @@ module M : Heap_intf.M with type vt = Term.t = struct Hashtbl.iter tree_to_json h'; "Json files created in output directory." - let malloc (h : t) (sz : vt) (pc : vt PC.t) : (t * vt * vt PC.t) list = + let malloc (h : t) (sz : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let h', curr = h in let tree = Leaf ((Term.Val (Integer 0), sz), Term.Val (Integer 0)) in Hashtbl.replace h' curr tree; [ ((h', curr + 1), Term.Val (Loc curr), pc) ] - let update h (arr : vt) (index : vt) (v : vt) (pc : vt PC.t) : - (t * vt PC.t) list = + let update h (arr : vt) (index : vt) (v : vt) (pc : vt Pc.t) : + (t * vt Pc.t) list = let h', next = h in - let rec update_tree (tree : tree_t) (index : vt) (v : vt) (pc : vt PC.t) : - (tree_t * vt PC.t) list option = + let rec update_tree (tree : tree_t) (index : vt) (v : vt) (pc : vt Pc.t) : + (tree_t * vt Pc.t) list option = match tree with | Leaf ((left, right), old_v) -> let ge_left = Term.Binop (Gte, index, left) in @@ -128,7 +128,7 @@ module M : Heap_intf.M with type vt = Term.t = struct new_trees | None -> failwith "Out of bounds access" - let must_within_range (r : range) (index : vt) (pc : vt PC.t) : bool = + let must_within_range (r : range) (index : vt) (pc : vt Pc.t) : bool = let lower, upper = r in let e1 = Term.Binop (Lt, index, lower) in @@ -137,7 +137,7 @@ module M : Heap_intf.M with type vt = Term.t = struct not (Translator.is_sat (e3 :: pc)) - let may_within_range (r : range) (index : vt) (pc : vt PC.t) : bool = + let may_within_range (r : range) (index : vt) (pc : vt Pc.t) : bool = let lower, upper = r in let e1 = Term.Binop (Gte, index, lower) in @@ -145,7 +145,7 @@ module M : Heap_intf.M with type vt = Term.t = struct Translator.is_sat ([ e1; e2 ] @ pc) - let rec search_tree (index : vt) (pc : vt PC.t) (tree : tree_t) : + let rec search_tree (index : vt) (pc : vt Pc.t) (tree : tree_t) : (vt * vt) list = match tree with | Leaf (r, v) -> @@ -165,7 +165,7 @@ module M : Heap_intf.M with type vt = Term.t = struct if in_range then List.concat (List.map (search_tree index pc) tree_list) else [] - let lookup h (arr : vt) (index : vt) (pc : vt PC.t) : (t * vt * vt PC.t) list + let lookup h (arr : vt) (index : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let tbl, _ = h in @@ -186,7 +186,7 @@ module M : Heap_intf.M with type vt = Term.t = struct ) | _ -> failwith "InternalError: HeapTree.lookup, arr must be location" - let free h (arr : vt) (pc : vt PC.t) : (t * vt PC.t) list = + let free h (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = let h', _ = h in (* let ign = to_string h in ignore ign; *) @@ -195,8 +195,8 @@ module M : Heap_intf.M with type vt = Term.t = struct | _ -> failwith "Invalid allocation index"); [ (h, pc) ] - let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt PC.t) : bool = - (* Printf.printf "In_bounds .array: %s, i: %s\n PC: %s\n" (Term.to_string arr) (Term.string_of_expression i) (PC.to_string Term.string_of_expression pc); *) + let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = + (* Printf.printf "In_bounds .array: %s, i: %s\n PC: %s\n" (Term.to_string arr) (Term.string_of_expression i) (Pc.to_string Term.string_of_expression pc); *) let h', _ = heap in match arr with | Val (Loc l) -> ( diff --git a/lib/interpreter.ml b/lib/interpreter.ml index ee17001..1d1ad4f 100644 --- a/lib/interpreter.ml +++ b/lib/interpreter.ml @@ -9,7 +9,7 @@ module Make type t = Eval.t type h = Heap.t - type state = (Eval.t, Heap.t) SState.t + type state = (Eval.t, Heap.t) Sstate.t (* Evaluates an expressions *) let eval = Eval.eval @@ -21,7 +21,7 @@ module Make let make_symbol = Eval.make_symbol (* Adds an expression to a path condition *) - let add_condition = PC.add_condition + let add_condition = Pc.add_condition (* Integer constant that bounds the number of steps performed by the interpreter *) let tank = Parameters.tank @@ -31,11 +31,11 @@ module Make let initial_state (program : Program.program) : state * Program.stmt list = let main = Program.get_function Parameters.main_id program in let state = - SState. + Sstate. { heap = Heap.init (); store = Store.create_empty_store Parameters.size; - pc = PC.create_pathcondition; + pc = Pc.create_pathcondition; cs = Callstack.create_callstack; } in @@ -54,7 +54,7 @@ module Make if !Utils.verbose then (* Printf.printf "\n"; let/ state = Choice.get in Printf.printf "Heap: %s\n" (Heap.to_string state.heap); - Printf.printf "State: %s\n" (SState.to_string Eval.pp Heap.pp state); *) + Printf.printf "State: %s\n" (Sstate.to_string Eval.pp Heap.pp state); *) Fmt.printf "Stmt: %a@." Program.pp_stmt s; match s with | Skip | Clear -> return cont @@ -98,7 +98,7 @@ module Make Store.set s.store x symb_val; let v = eval s.store c in let pc' = add_condition s.pc v in - if is_true pc' then [ ((), SState.{ s with pc = pc' }) ] else [] + if is_true pc' then [ ((), Sstate.{ s with pc = pc' }) ] else [] in let/ () = Choice.lift f_symb_int in return cont) @@ -170,7 +170,7 @@ module Make List.map (fun (hp, loc, pc') -> ( loc, - SState. + Sstate. { heap = hp; pc = pc'; @@ -200,7 +200,7 @@ module Make else (s.store, s.cs) in ( (), - SState.{ heap = hp; pc = pc'; store = store'; cs = cs' } + Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' } )) lst else failwith "Index out of bounds" @@ -224,7 +224,7 @@ module Make if dup then (Store.dup s.store, Callstack.dup s.cs) else (s.store, s.cs) in - (v, SState.{ heap = hp; pc = pc'; store = store'; cs = cs' })) + (v, Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' })) lst else failwith "Index out of bounds" | None -> failwith "InternalError: array is not defined" @@ -246,7 +246,7 @@ module Make if dup then (Store.dup s.store, Callstack.dup s.cs) else (s.store, s.cs) in - ((), SState.{ heap = hp; pc = pc'; store = store'; cs = cs' })) + ((), Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' })) lst | None -> failwith "InternalError: array is not defined" in diff --git a/lib/interpreter_intf.ml b/lib/interpreter_intf.ml index 6bb1008..f814c22 100644 --- a/lib/interpreter_intf.ml +++ b/lib/interpreter_intf.ml @@ -1,7 +1,7 @@ module type S = sig type t type h - type state = (t, h) SState.t + type state = (t, h) Sstate.t val interpret : Program.program -> (Outcome.t * state) list end diff --git a/lib/ListChoice.ml b/lib/list_choice.ml similarity index 79% rename from lib/ListChoice.ml rename to lib/list_choice.ml index 19401e3..95b07ac 100644 --- a/lib/ListChoice.ml +++ b/lib/list_choice.ml @@ -1,8 +1,8 @@ -open SState +open Sstate module Make (Eval : Eval_intf.M) (Heap : Heap_intf.M with type vt = Eval.t) : Choice_intf.Choice with type v = Eval.t and type h = Heap.t = struct - type state = (Eval.t, Heap.t) SState.t + type state = (Eval.t, Heap.t) Sstate.t type v = Eval.t type h = Heap.t type 'a t = state -> ('a * state) list @@ -26,16 +26,16 @@ module Make (Eval : Eval_intf.M) (Heap : Heap_intf.M with type vt = Eval.t) : let select v (s : state) = let pc = s.pc in let not_v = Eval.negate v in - let pc_v = PC.add_condition pc v in - let pc_not_v = PC.add_condition pc not_v in + let pc_v = Pc.add_condition pc v in + let pc_not_v = Pc.add_condition pc not_v in match (Eval.is_true pc_v, Eval.is_true pc_not_v) with | false, false -> assert false | true, false -> [ (true, { s with pc = pc_v }) ] | false, true -> [ (false, { s with pc = pc_not_v }) ] | true, true -> [ - (true, { (SState.dup s Heap.clone) with pc = pc_v }); - (false, { (SState.dup s Heap.clone) with pc = pc_not_v }); + (true, { (Sstate.dup s Heap.clone) with pc = pc_v }); + (false, { (Sstate.dup s Heap.clone) with pc = pc_not_v }); ] let lift (f : state -> ('a * state) list) : 'a t = f diff --git a/lib/Operations.ml b/lib/operations.ml similarity index 100% rename from lib/Operations.ml rename to lib/operations.ml diff --git a/lib/Outcome.ml b/lib/outcome.ml similarity index 100% rename from lib/Outcome.ml rename to lib/outcome.ml diff --git a/lib/Parameters.ml b/lib/parameters.ml similarity index 100% rename from lib/Parameters.ml rename to lib/parameters.ml diff --git a/lib/PC.ml b/lib/pc.ml similarity index 100% rename from lib/PC.ml rename to lib/pc.ml diff --git a/lib/Program.ml b/lib/program.ml similarity index 100% rename from lib/Program.ml rename to lib/program.ml diff --git a/lib/Return.ml b/lib/return.ml similarity index 89% rename from lib/Return.ml rename to lib/return.ml index 8da8229..f88ef9c 100644 --- a/lib/Return.ml +++ b/lib/return.ml @@ -8,7 +8,7 @@ let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) "#RETURN:@\n -Outcome : %a@\n -Store : %a@\n -Path cond.: %a@\n \ -Heap : %a@\n" (Outcome.pp ~no_values:false) - out (Store.pp pp_val) st (PC.pp pp_val) pc pp_heap h + out (Store.pp pp_val) st (Pc.pp pp_val) pc pp_heap h let string_of_return (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) (ret : ('v, 'h) t) : string = @@ -18,7 +18,7 @@ let get_outcome (ret : ('v, 'h) t) : Outcome.t = let _, out = ret in out -let get_pc (ret : ('v, 'h) t) : 'v PC.t = +let get_pc (ret : ('v, 'h) t) : 'v Pc.t = let state, _ = ret in State.get_pathcondition state diff --git a/lib/SState.ml b/lib/sstate.ml similarity index 96% rename from lib/SState.ml rename to lib/sstate.ml index 6fcc1fd..d47bd7b 100644 --- a/lib/SState.ml +++ b/lib/sstate.ml @@ -1,7 +1,7 @@ type ('v, 'h) t = { store : 'v Store.t; cs : 'v Callstack.t; - pc : 'v PC.t; + pc : 'v Pc.t; heap : 'h; } @@ -10,7 +10,7 @@ let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) Format.fprintf fmt "{@\n-Store : %a@\n-Callstack : %a@\n-Path cond. : \ %a@\n-Heap : %a@\n}" - (Store.pp pp_val) state.store (Callstack.pp pp_val) state.cs (PC.pp pp_val) + (Store.pp pp_val) state.store (Callstack.pp pp_val) state.cs (Pc.pp pp_val) state.pc pp_heap state.heap let to_string (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) diff --git a/lib/State.ml b/lib/state.ml similarity index 92% rename from lib/State.ml rename to lib/state.ml index 8f27f5f..8f39dcb 100644 --- a/lib/State.ml +++ b/lib/state.ml @@ -1,5 +1,5 @@ type ('v, 'h) t = - Program.stmt * Program.stmt list * 'v Store.t * 'v Callstack.t * 'v PC.t * 'h + Program.stmt * Program.stmt list * 'v Store.t * 'v Callstack.t * 'v Pc.t * 'h let get_statement (state : ('v, 'h) t) : Program.stmt = let stmt, _, _, _, _, _ = state in @@ -17,7 +17,7 @@ let get_callstack (state : ('v, 'h) t) : 'v Callstack.t = let _, _, _, cs, _, _ = state in cs -let get_pathcondition (state : ('v, 'h) t) : 'v PC.t = +let get_pathcondition (state : ('v, 'h) t) : 'v Pc.t = let _, _, _, _, pc, _ = state in pc @@ -34,7 +34,7 @@ let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) ">STATE:@\n -Cur Statement : %a@\n -Continuation : %a@\n -Store : \ %a@\n -Callstack : %a@\n -Path cond. : %a@\n -Heap : %a@\n" Program.pp_stmt s (pp_lst ~pp_sep:(fun fmt () -> fprintf fmt "; ") Program.pp_stmt) cont (Store.pp pp_val) store - (Callstack.pp pp_val) cs (PC.pp pp_val) pc pp_heap heap + (Callstack.pp pp_val) cs (Pc.pp pp_val) pc pp_heap heap let to_string (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) (state : ('v, 'h) t) : string = diff --git a/lib/Store.ml b/lib/store.ml similarity index 100% rename from lib/Store.ml rename to lib/store.ml diff --git a/lib/SymbMap.ml b/lib/symb_map.ml similarity index 100% rename from lib/SymbMap.ml rename to lib/symb_map.ml diff --git a/lib/Utils.ml b/lib/utils.ml similarity index 100% rename from lib/Utils.ml rename to lib/utils.ml diff --git a/lib/Value.ml b/lib/value.ml similarity index 100% rename from lib/Value.ml rename to lib/value.ml From 41ec0f5a96aa55640d4dd9c00deebb3647164f5c Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 11 Mar 2024 14:43:57 +0000 Subject: [PATCH 3/4] using Fmt instead of Format --- lib/callstack.ml | 2 +- lib/eval_concolic.ml | 4 ++-- lib/eval_concrete.ml | 2 +- lib/heap/heap_array_fork.ml | 4 ++-- lib/heap/heap_arrayite.ml | 2 +- lib/heap/heap_concrete.ml | 2 +- lib/heap/heap_tree.ml | 2 +- lib/log.ml | 2 +- lib/model.ml | 4 ++-- lib/model.mli | 2 +- lib/outcome.ml | 12 ++++++------ lib/program.ml | 4 ++-- lib/return.ml | 2 +- lib/sstate.ml | 6 +++--- lib/state.ml | 2 +- lib/term.ml | 6 +++--- lib/translator.ml | 4 ++-- lib/value.ml | 4 ++-- 18 files changed, 33 insertions(+), 33 deletions(-) diff --git a/lib/callstack.ml b/lib/callstack.ml index ba6ddb0..2a67f94 100644 --- a/lib/callstack.ml +++ b/lib/callstack.ml @@ -44,7 +44,7 @@ let pp (pp_val : Fmt.t -> 'v -> unit) (fmt : Fmt.t) (cs : 'store t) : unit = (pp_lst ~pp_sep:pp_newline pp_frame fmt) cs let to_string (pp_val : Fmt.t -> 'v -> unit) (cs : 'v t) : string = - Format.asprintf "%a" (pp pp_val) cs + Fmt.asprintf "%a" (pp pp_val) cs let print (pp_val : Fmt.t -> 'v -> unit) (cs : 'v t) : unit = to_string pp_val cs |> print_endline diff --git a/lib/eval_concolic.ml b/lib/eval_concolic.ml index 1f28d98..3a6c428 100644 --- a/lib/eval_concolic.ml +++ b/lib/eval_concolic.ml @@ -30,10 +30,10 @@ module M : Eval_intf.M with type t = Value.t * Term.t = struct let pp (fmt : Fmt.t) (e : t) : unit = let value, expression = e in - Format.fprintf fmt "(%a, %a)" Eval_concrete.pp value Eval_symbolic.pp + Fmt.fprintf fmt "(%a, %a)" Eval_concrete.pp value Eval_symbolic.pp expression - let to_string (e : t) : string = Format.asprintf "%a" pp 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) = diff --git a/lib/eval_concrete.ml b/lib/eval_concrete.ml index 22cced8..42c6454 100644 --- a/lib/eval_concrete.ml +++ b/lib/eval_concrete.ml @@ -54,7 +54,7 @@ module M : Eval_intf.M with type t = Value.t = struct value" let pp (fmt : Fmt.t) (v : t) : unit = Value.pp fmt v - let to_string (v : t) : string = Format.asprintf "%a" pp v + let to_string (v : t) : string = Fmt.asprintf "%a" pp v let print (v : t) : unit = to_string v |> print_endline let make_symbol (name : string) (tp : string) = diff --git a/lib/heap/heap_array_fork.ml b/lib/heap/heap_array_fork.ml index a0a333b..03f032a 100644 --- a/lib/heap/heap_array_fork.ml +++ b/lib/heap/heap_array_fork.ml @@ -8,7 +8,7 @@ module M : Heap_intf.M with type vt = Term.t = struct let init () : t = { map = Hashtbl.create Parameters.size; i = 0 } - let pp_block fmt (block : bt) = + let pp_block (fmt : Fmt.t) (block : bt) = Fmt.fprintf fmt "%a" (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Term.pp) (Array.to_list block) let pp (fmt : Fmt.t) (heap : t) : unit = @@ -16,7 +16,7 @@ module M : Heap_intf.M with type vt = Term.t = struct let pp_binding fmt (_, v) = fprintf fmt "%a" pp_block v in fprintf fmt "%a" (pp_hashtbl ~pp_sep:pp_newline pp_binding) heap.map - let to_string (heap : t) : string = Format.asprintf "%a" pp heap + let to_string (heap : t) : string = Fmt.asprintf "%a" pp heap let is_within (sz : int) (index : vt) (pc : vt Pc.t) : bool = let e1 = Term.Binop (Lt, index, Val (Value.Integer 0)) in diff --git a/lib/heap/heap_arrayite.ml b/lib/heap/heap_arrayite.ml index 9c62fe6..8936e39 100644 --- a/lib/heap/heap_arrayite.ml +++ b/lib/heap/heap_arrayite.ml @@ -15,7 +15,7 @@ module M : Heap_intf.M with type vt = Term.t = struct let pp_binding fmt (_, v) = fprintf fmt "%a" pp_block v in fprintf fmt "%a" (pp_hashtbl ~pp_sep:pp_newline pp_binding) heap - let to_string (heap : t) : string = Format.asprintf "%a" pp heap + let to_string (heap : t) : string = Fmt.asprintf "%a" pp heap let is_within (sz : int) (index : vt) (pc : vt Pc.t) : bool = let e1 = Term.Binop (Lt, index, Val (Value.Integer 0)) in diff --git a/lib/heap/heap_concrete.ml b/lib/heap/heap_concrete.ml index 81f207d..25ff7c0 100644 --- a/lib/heap/heap_concrete.ml +++ b/lib/heap/heap_concrete.ml @@ -15,7 +15,7 @@ module M : Heap_intf.M with type vt = Value.t = struct let pp_binding fmt (_, v) = fprintf fmt "%a" pp_block v in fprintf fmt "%a" (pp_hashtbl ~pp_sep:pp_newline pp_binding) heap - let to_string (heap : t) : string = Format.asprintf "%a" pp heap + let to_string (heap : t) : string = Fmt.asprintf "%a" pp heap let malloc (h : t) (sz : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let tbl, next = h in diff --git a/lib/heap/heap_tree.ml b/lib/heap/heap_tree.ml index 5ef5d64..686356d 100644 --- a/lib/heap/heap_tree.ml +++ b/lib/heap/heap_tree.ml @@ -29,7 +29,7 @@ module M : Heap_intf.M with type vt = Term.t = struct let tree_to_json (idx : int) (tree : tree_t) : unit = let f = open_out ("output/" ^ string_of_int idx ^ "_tree.json") in - let tree_json = Format.asprintf "%a" pp_block tree in + let tree_json = Fmt.asprintf "%a" pp_block tree in Printf.fprintf f "%s\n" tree_json; close_out f diff --git a/lib/log.ml b/lib/log.ml index ea227da..678322b 100644 --- a/lib/log.ml +++ b/lib/log.ml @@ -1 +1 @@ -let error fmt = Format.kasprintf failwith fmt +let error fmt = Fmt.kasprintf failwith fmt diff --git a/lib/model.ml b/lib/model.ml index 87abf30..8f390c3 100644 --- a/lib/model.ml +++ b/lib/model.ml @@ -18,7 +18,7 @@ let get_value (model : t) (var : string) : Value.t = var | v -> v) -let pp ?(no_values = false) (fmt : Format.formatter) (model : t) : unit = +let pp ?(no_values = false) (fmt : Fmt.formatter) (model : t) : unit = let open Fmt in let pp_binding fmt (x, v) = fprintf fmt "%s : %a" x (Value.pp ~no_values) v @@ -31,4 +31,4 @@ let pp ?(no_values = false) (fmt : Format.formatter) (model : t) : unit = pp_lst ~pp_sep:pp_newline pp_binding fmt m let to_string (model : t) : string = - Format.asprintf "%a" (pp ~no_values:false) model + Fmt.asprintf "%a" (pp ~no_values:false) model diff --git a/lib/model.mli b/lib/model.mli index f4d8aac..5315528 100644 --- a/lib/model.mli +++ b/lib/model.mli @@ -2,5 +2,5 @@ type t = (string * Value.t) list option [@@deriving yojson] val empty : t val get_value : t -> string -> Value.t -val pp : ?no_values:bool -> Format.formatter -> t -> unit +val pp : ?no_values:bool -> Fmt.formatter -> t -> unit val to_string : t -> string diff --git a/lib/outcome.ml b/lib/outcome.ml index 33322a4..9a8b6ba 100644 --- a/lib/outcome.ml +++ b/lib/outcome.ml @@ -7,16 +7,16 @@ type t = [@@deriving yojson] let pp ?(no_values = false) fmt = function - | Cont _ -> Format.pp_print_string fmt "Continue" + | Cont _ -> Fmt.pp_print_string fmt "Continue" | Error e -> - Format.fprintf fmt + Fmt.fprintf fmt "Assertion violated, counter example:@\n@[ %a@]" (Model.pp ~no_values) e - | AssumeF -> Format.pp_print_string fmt "Assumption evaluated to false" - | Return e -> Format.fprintf fmt "Returned %s" e - | EndGas -> Format.pp_print_string fmt "EndGas" + | AssumeF -> Fmt.pp_print_string fmt "Assumption evaluated to false" + | Return e -> Fmt.fprintf fmt "Returned %s" e + | EndGas -> Fmt.pp_print_string fmt "EndGas" -let to_string (o : t) : string = Format.asprintf "%a" (pp ~no_values:false) o +let to_string (o : t) : string = Fmt.asprintf "%a" (pp ~no_values:false) o let should_halt (o : t) : bool = match o with Error _ | AssumeF | EndGas -> true | _ -> false diff --git a/lib/program.ml b/lib/program.ml index c07b6cb..4115524 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -61,13 +61,13 @@ let rec pp_stmt (fmt : Fmt.t) (s : stmt) : unit = Term.pp e arr | Delete arr -> fprintf fmt "Delete: %s" arr -let string_of_stmt (s : stmt) : string = Format.asprintf "%a" pp_stmt s +let string_of_stmt (s : stmt) : string = Fmt.asprintf "%a" pp_stmt s let pp_func (fmt : Fmt.t) (f : func) : unit = let open Fmt in fprintf fmt " Function id: %s@\nArguments : (%a)@\nBody : %a@\n" f.id (pp_lst ~pp_sep:pp_comma pp_str) f.args pp_stmt f.body -let string_of_function (f : func) : string = Format.asprintf "%a" pp_func f +let string_of_function (f : func) : string = Fmt.asprintf "%a" pp_func f let print_statement (s : stmt) : unit = s |> string_of_stmt |> print_endline let print_function (f : func) : unit = f |> string_of_function |> print_endline diff --git a/lib/return.ml b/lib/return.ml index f88ef9c..9c20710 100644 --- a/lib/return.ml +++ b/lib/return.ml @@ -12,7 +12,7 @@ let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) let string_of_return (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) (ret : ('v, 'h) t) : string = - Format.asprintf "%a" (pp pp_val pp_heap) ret + Fmt.asprintf "%a" (pp pp_val pp_heap) ret let get_outcome (ret : ('v, 'h) t) : Outcome.t = let _, out = ret in diff --git a/lib/sstate.ml b/lib/sstate.ml index d47bd7b..0e77d57 100644 --- a/lib/sstate.ml +++ b/lib/sstate.ml @@ -6,8 +6,8 @@ type ('v, 'h) t = { } let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (fmt : Format.formatter) (state : ('v, 'h) t) : unit = - Format.fprintf fmt + (fmt : Fmt.formatter) (state : ('v, 'h) t) : unit = + Fmt.fprintf fmt "{@\n-Store : %a@\n-Callstack : %a@\n-Path cond. : \ %a@\n-Heap : %a@\n}" (Store.pp pp_val) state.store (Callstack.pp pp_val) state.cs (Pc.pp pp_val) @@ -15,7 +15,7 @@ let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) let to_string (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) (state : ('v, 'h) t) : string = - Format.asprintf "%a" (pp pp_val pp_heap) state + Fmt.asprintf "%a" (pp pp_val pp_heap) state let print (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) (state : ('v, 'h) t) : unit = diff --git a/lib/state.ml b/lib/state.ml index 8f39dcb..84b8330 100644 --- a/lib/state.ml +++ b/lib/state.ml @@ -38,7 +38,7 @@ let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) let to_string (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) (state : ('v, 'h) t) : string = - Format.asprintf "%a" (pp pp_val pp_heap) state + Fmt.asprintf "%a" (pp pp_val pp_heap) state let print (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) (state : ('v, 'h) t) : unit = diff --git a/lib/term.ml b/lib/term.ml index b4bc584..f5ddc40 100644 --- a/lib/term.ml +++ b/lib/term.ml @@ -64,8 +64,8 @@ let rec get_symbols (e : t) : string list = | Binop (_, e1, e2) -> get_symbols e1 @ get_symbols e2 | Ite (e1, e2, e3) -> get_symbols e1 @ get_symbols e2 @ get_symbols e3 -let pp_string = Format.pp_print_string -let fprintf = Format.fprintf +let pp_string = Fmt.pp_print_string +let fprintf = Fmt.fprintf let pp_unop fmt (op : unop) = match op with @@ -104,4 +104,4 @@ let rec pp fmt (e : t) = | Binop (op, v1, v2) -> fprintf fmt "(%a %a %a)" pp_binop op pp v1 pp v2 | Ite (e1, e2, e3) -> fprintf fmt "(%a %a %a)" pp e1 pp e2 pp e3 -let to_string (e : t) : string = Format.asprintf "%a" pp e +let to_string (e : t) : string = Fmt.asprintf "%a" pp e diff --git a/lib/translator.ml b/lib/translator.ml index 4734391..448520e 100644 --- a/lib/translator.ml +++ b/lib/translator.ml @@ -45,7 +45,7 @@ let translate_binop (op : binop) (v1 : Z3.Expr.expr) (v2 : Z3.Expr.expr) : | And -> Z3.Boolean.mk_and ctx [ v1; v2 ] | Xor -> Z3.Boolean.mk_xor ctx v1 v2 | _ -> - Format.kasprintf failwith + Fmt.kasprintf failwith "TODO: Encoding.encode_binop, missing implementation of %a" Term.pp_binop op @@ -102,5 +102,5 @@ let find_model ?(print_model = false) (es : Term.t list) : (string * Value.t) list option = assert (is_sat es); let* model = Z3.Solver.get_model solver in - if print_model then Format.printf "%s@." (Z3.Model.to_string model); + if print_model then Fmt.printf "%s@." (Z3.Model.to_string model); list_map (get_interp model) (Z3.Model.get_const_decls model) diff --git a/lib/value.ml b/lib/value.ml index 97fb088..af8307c 100644 --- a/lib/value.ml +++ b/lib/value.ml @@ -2,7 +2,7 @@ type t = Integer of int | Boolean of bool | Loc of int | Error [@@deriving yojson] let pp ?(no_values = false) fmt (v : t) = - let open Format in + let open Fmt in match v with | Integer n -> if no_values then fprintf fmt "Int _" else fprintf fmt "Int %d" n @@ -11,4 +11,4 @@ let pp ?(no_values = false) fmt (v : t) = | Loc l -> if no_values then fprintf fmt "Loc _ " else fprintf fmt "Loc %d" l | Error -> pp_print_string fmt "Error" -let to_string = Format.asprintf "%a" (pp ~no_values:false) +let to_string = Fmt.asprintf "%a" (pp ~no_values:false) From ce48badc863ebc439fb2459570604815f99c3175 Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 11 Mar 2024 14:49:01 +0000 Subject: [PATCH 4/4] configure and apply ocamlformat --- .ocamlformat | 43 ++++ bin/commands/cmd_execute.ml | 140 +++++++------ bin/commands/cmd_test.ml | 28 +-- bin/docs/doc_execute.ml | 22 +-- bin/docs/doc_test.ml | 18 +- bin/main.ml | 22 +-- bin/utils/dir.ml | 2 +- bin/utils/options.ml | 11 +- lib/callstack.ml | 18 +- lib/eval_concrete.ml | 34 ++-- lib/eval_expression.ml | 123 ++++++------ lib/eval_symbolic.ml | 22 +-- lib/fmt.ml | 12 +- lib/heap/heap_array_fork.ml | 115 ++++++----- lib/heap/heap_arrayite.ml | 151 +++++++------- lib/heap/heap_concolic.ml | 21 +- lib/heap/heap_concrete.ml | 74 +++---- lib/heap/heap_oplist.ml | 30 +-- lib/heap/heap_symbolic.ml | 12 +- lib/heap/heap_tree.ml | 225 +++++++++++---------- lib/interpreter.ml | 382 ++++++++++++++++++------------------ lib/list_choice.ml | 15 +- lib/model.ml | 28 ++- lib/operations.ml | 12 +- lib/outcome.ml | 5 +- lib/program.ml | 40 ++-- lib/return.ml | 13 +- lib/sstate.ml | 35 ++-- lib/state.ml | 23 ++- lib/term.ml | 13 +- lib/translator.ml | 48 +++-- lib/value.ml | 10 +- 32 files changed, 907 insertions(+), 840 deletions(-) diff --git a/.ocamlformat b/.ocamlformat index e69de29..ca185b1 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -0,0 +1,43 @@ +version=0.26.1 +assignment-operator=end-line +break-cases=fit +break-fun-decl=wrap +break-fun-sig=wrap +break-infix=wrap +break-infix-before-func=false +break-separators=before +break-sequences=true +cases-exp-indent=2 +cases-matching-exp-indent=normal +doc-comments=before +doc-comments-padding=2 +doc-comments-tag-only=default +dock-collection-brackets=false +exp-grouping=preserve +field-space=loose +if-then-else=compact +indicate-multiline-delimiters=space +indicate-nested-or-patterns=unsafe-no +infix-precedence=indent +leading-nested-match-parens=false +let-and=sparse +let-binding-spacing=compact +let-module=compact +margin=80 +max-indent=2 +module-item-spacing=compact +ocaml-version=4.14.0 +ocp-indent-compat=false +parens-ite=false +parens-tuple=always +parse-docstrings=true +sequence-blank-line=preserve-one +sequence-style=terminator +single-case=compact +space-around-arrays=true +space-around-lists=true +space-around-records=true +space-around-variants=true +type-decl=sparse +wrap-comments=false +wrap-fun-args=true \ No newline at end of file diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml index 7834870..3cc3812 100644 --- a/bin/commands/cmd_execute.ml +++ b/bin/commands/cmd_execute.ml @@ -9,34 +9,45 @@ module ST_Choice = List_choice.Make (Eval_symbolic.M) (Heap_tree.M) module SOPL_Choice = List_choice.Make (Eval_symbolic.M) (Heap_oplist.M) (* Interpreter *) -module C = Interpreter.Make (Eval_concrete.M) (Dfs.M) (Heap_concrete.M) (C_Choice) +module C = + Interpreter.Make (Eval_concrete.M) (Dfs.M) (Heap_concrete.M) (C_Choice) + module SAF = Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_array_fork.M) (SAF_Choice) + module SAITE = Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_arrayite.M) (SAITE_Choice) + module ST = Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_tree.M) (ST_Choice) + module SOPL = Interpreter.Make (Eval_symbolic.M) (Dfs.M) (Heap_oplist.M) (SOPL_Choice) -type mode = Concrete | Saf | Saite | St | Sopl [@@deriving yojson] +type mode = + | Concrete + | Saf + | Saite + | St + | Sopl +[@@deriving yojson] -type report = { - filename : string; - mode : mode; - execution_time : float; - solver_time : float; - num_paths : int; - num_problems : int; - problems : Outcome.t list; -} +type report = + { filename : string + ; mode : mode + ; execution_time : float + ; solver_time : float + ; num_paths : int + ; num_problems : int + ; problems : Outcome.t list + } [@@deriving yojson] -type options = { - input : Fpath.t; - mode : mode; - output : Fpath.t option; - verbose : bool; -} +type options = + { input : Fpath.t + ; mode : mode + ; output : Fpath.t option + ; verbose : bool + } let mode_to_string = function | Concrete -> "c" @@ -61,50 +72,50 @@ let run input mode = let problems, num_paths = match mode with | Concrete -> - let rets = C.interpret program in - ( List.filter_map - (fun (out, _) -> - match out with - | Outcome.Error _ | Outcome.EndGas -> Some out - | _ -> None) - rets, - List.length rets ) + let rets = C.interpret program in + ( List.filter_map + (fun (out, _) -> + match out with + | Outcome.Error _ | Outcome.EndGas -> Some out + | _ -> None ) + rets + , List.length rets ) | Saf -> - let rets = SAF.interpret program in - ( List.filter_map - (fun (out, _) -> - match out with - | Outcome.Error _ | Outcome.EndGas -> Some out - | _ -> None) - rets, - List.length rets ) + let rets = SAF.interpret program in + ( List.filter_map + (fun (out, _) -> + match out with + | Outcome.Error _ | Outcome.EndGas -> Some out + | _ -> None ) + rets + , List.length rets ) | Saite -> - let rets = SAITE.interpret program in - ( List.filter_map - (fun (out, _) -> - match out with - | Outcome.Error _ | Outcome.EndGas -> Some out - | _ -> None) - rets, - List.length rets ) + let rets = SAITE.interpret program in + ( List.filter_map + (fun (out, _) -> + match out with + | Outcome.Error _ | Outcome.EndGas -> Some out + | _ -> None ) + rets + , List.length rets ) | St -> - let rets = ST.interpret program in - ( List.filter_map - (fun (out, _) -> - match out with - | Outcome.Error _ | Outcome.EndGas -> Some out - | _ -> None) - rets, - List.length rets ) + let rets = ST.interpret program in + ( List.filter_map + (fun (out, _) -> + match out with + | Outcome.Error _ | Outcome.EndGas -> Some out + | _ -> None ) + rets + , List.length rets ) | Sopl -> - let rets = SOPL.interpret program in - ( List.filter_map - (fun (out, _) -> - match out with - | Outcome.Error _ | Outcome.EndGas -> Some out - | _ -> None) - rets, - List.length rets ) + let rets = SOPL.interpret program in + ( List.filter_map + (fun (out, _) -> + match out with + | Outcome.Error _ | Outcome.EndGas -> Some out + | _ -> None ) + rets + , List.length rets ) in let execution_time = Sys.time () -. start in let num_problems = List.length problems in @@ -118,14 +129,13 @@ let run input mode = Total Solver time: %f\n" execution_time !Translator.solver_time; write_report - { - execution_time; - mode; - num_paths; - num_problems; - problems; - filename = input; - solver_time = !Translator.solver_time; + { execution_time + ; mode + ; num_paths + ; num_problems + ; problems + ; filename = input + ; solver_time = !Translator.solver_time } let main (opts : options) = diff --git a/bin/commands/cmd_test.ml b/bin/commands/cmd_test.ml index c4e5751..afd91c8 100644 --- a/bin/commands/cmd_test.ml +++ b/bin/commands/cmd_test.ml @@ -2,12 +2,12 @@ open Whilloc exception Timeout -type options = { - inputs : Fpath.t; - mode : Cmd_execute.mode; - timeout : float option; - verbose : bool; -} +type options = + { inputs : Fpath.t + ; mode : Cmd_execute.mode + ; timeout : float option + ; verbose : bool + } let _max_timeout = ref 0.0 let unset () = Sys.set_signal Sys.sigalrm Sys.Signal_ignore @@ -17,9 +17,9 @@ let set = fun () -> Sys.set_signal Sys.sigalrm (Sys.Signal_handle raise); ignore - @@ (Unix.setitimer Unix.ITIMER_REAL - { Unix.it_interval = 0.; Unix.it_value = !_max_timeout } - : Unix.interval_timer_status) + @@ ( Unix.setitimer Unix.ITIMER_REAL + { Unix.it_interval = 0.; Unix.it_value = !_max_timeout } + : Unix.interval_timer_status ) let run_single mode file = try @@ -27,13 +27,13 @@ let run_single mode file = set (); try Cmd_execute.run file mode with | Timeout -> - Printf.printf - "Timeout occurred while processing file: %s (Max Timeout: %f \ - seconds)\n" - file !_max_timeout + Printf.printf + "Timeout occurred while processing file: %s (Max Timeout: %f \ + seconds)\n" + file !_max_timeout (* maybe is not the best way to treat exceptions *) | ex -> - Printf.printf "Fatal error: exception %s\n" (Printexc.to_string ex)) + Printf.printf "Fatal error: exception %s\n" (Printexc.to_string ex) ) with Timeout -> Printf.printf "General timeout\n" let run (opts : options) : unit = diff --git a/bin/docs/doc_execute.ml b/bin/docs/doc_execute.ml index 1119f38..e9d3e93 100644 --- a/bin/docs/doc_execute.ml +++ b/bin/docs/doc_execute.ml @@ -4,23 +4,21 @@ let doc = "Executes a program concretely or symbolically depending on the mode" let sdocs = Manpage.s_common_options let description = - [ - "Given a program in the simple \"While\" language, executes the program \ + [ "Given a program in the simple \"While\" language, executes the program \ concretely or symbolically depending on the mode. At the end, it \ generates a report named 'report.json' that includes some execution \ - metrics and counter models that were found."; - "To run the program concretely, use the mode 'c'."; - "To run the program symbolically, there are several modes to choose from. \ + metrics and counter models that were found." + ; "To run the program concretely, use the mode 'c'." + ; "To run the program symbolically, there are several modes to choose from. \ These modes differs on the memory model that it uses to execute the \ - program."; + program." ] let man = - [ - `S Manpage.s_description; - `P (List.nth description 0); - `P (List.nth description 1); - `P (List.nth description 2); + [ `S Manpage.s_description + ; `P (List.nth description 0) + ; `P (List.nth description 1) + ; `P (List.nth description 2) ] let man_xrefs = [] @@ -31,6 +29,6 @@ let cmd_options input mode output verbose : Cmd_execute.options = let options = Term.( const cmd_options $ Options.File.input $ Options.mode $ Options.File.output - $ Options.verbose) + $ Options.verbose ) let term = Term.(const Cmd_execute.main $ options) diff --git a/bin/docs/doc_test.ml b/bin/docs/doc_test.ml index 0c7d8dc..a849231 100644 --- a/bin/docs/doc_test.ml +++ b/bin/docs/doc_test.ml @@ -7,21 +7,19 @@ let doc = let sdocs = Manpage.s_common_options let description = - [ - "Executes all programs with the extension .wl in the given directory and \ - mode."; - "The difference of running programs using this command and command 'wl \ + [ "Executes all programs with the extension .wl in the given directory and \ + mode." + ; "The difference of running programs using this command and command 'wl \ execute' is that this command will run all programs in the given \ directory. In addition, this command have the option to set a time limit \ for each program's execution. When the time limit is exceeded, the \ - execution is killed."; + execution is killed." ] let man = - [ - `S Manpage.s_description; - `P (List.nth description 0); - `P (List.nth description 1); + [ `S Manpage.s_description + ; `P (List.nth description 0) + ; `P (List.nth description 1) ] let man_xrefs = [ `Page ("wl execute", 2) ] @@ -32,6 +30,6 @@ let cmd_options inputs mode timeout verbose : Cmd_test.options = let options = Term.( const cmd_options $ Options.File.inputs $ Options.mode $ Options.timeout - $ Options.verbose) + $ Options.verbose ) let term = Term.(const Cmd_test.main $ options) diff --git a/bin/main.ml b/bin/main.ml index 74509e2..e40b357 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -8,24 +8,22 @@ module AppInfo = struct allocation support." let description = - [ - "Whilloc is a parametric interpreter that supports concrete, symbolic, \ + [ "Whilloc is a parametric interpreter that supports concrete, symbolic, \ and concolic execution of programs written in a simple \"while\"-like \ - programming language with memory allocation support."; - "Use wl --help for more information on a specific command."; + programming language with memory allocation support." + ; "Use wl --help for more information on a specific command." ] let sdocs = Manpage.s_common_options let man = - [ - `S Manpage.s_description; - `P (List.nth description 0); - `P (List.nth description 1); - `S Manpage.s_common_options; - `P "These options are common to all commands."; - `S Manpage.s_bugs; - `P "Check bug reports at https://github.com/formalsec/whilloc/issues"; + [ `S Manpage.s_description + ; `P (List.nth description 0) + ; `P (List.nth description 1) + ; `S Manpage.s_common_options + ; `P "These options are common to all commands." + ; `S Manpage.s_bugs + ; `P "Check bug reports at https://github.com/formalsec/whilloc/issues" ] let man_xrefs = [] diff --git a/bin/utils/dir.ml b/bin/utils/dir.ml index 402e8f2..8a49a87 100644 --- a/bin/utils/dir.ml +++ b/bin/utils/dir.ml @@ -3,7 +3,7 @@ let get_files dir = let result = Bos.OS.Path.fold ~elements:`Files ~traverse:`Any (fun file files -> - if Fpath.has_ext ".wl" file then file :: files else files) + if Fpath.has_ext ".wl" file then file :: files else files ) files [ dir ] in match result with Ok files -> files | Error (`Msg err) -> failwith err diff --git a/bin/utils/options.ml b/bin/utils/options.ml index 7885f78..f4c8500 100644 --- a/bin/utils/options.ml +++ b/bin/utils/options.ml @@ -31,12 +31,11 @@ end let mode_conv = Arg.enum - [ - ("c", Cmd_execute.Concrete); - ("saf", Cmd_execute.Saf); - ("saite", Cmd_execute.Saite); - ("st", Cmd_execute.St); - ("sopl", Cmd_execute.Sopl); + [ ("c", Cmd_execute.Concrete) + ; ("saf", Cmd_execute.Saf) + ; ("saite", Cmd_execute.Saite) + ; ("st", Cmd_execute.St) + ; ("sopl", Cmd_execute.Sopl) ] let mode = diff --git a/lib/callstack.ml b/lib/callstack.ml index 2a67f94..615a4bb 100644 --- a/lib/callstack.ml +++ b/lib/callstack.ml @@ -24,22 +24,22 @@ let rec dup (cs : 'v t) : 'v t = match cs with | [] -> failwith "InternalError: Callstack.dup, empty callstack" | [ h ] -> - assert (h = Toplevel); - [ h ] + assert (h = Toplevel); + [ h ] | h :: t -> ( - match h with - | Toplevel -> [ h ] - | Intermediate (store, cont, var) -> - Intermediate (Store.dup store, cont, var) :: dup t) + match h with + | Toplevel -> [ h ] + | Intermediate (store, cont, var) -> + Intermediate (Store.dup store, cont, var) :: dup t ) let pp (pp_val : Fmt.t -> 'v -> unit) (fmt : Fmt.t) (cs : 'store t) : unit = let open Fmt in let pp_frame fmt = function | Toplevel -> pp_str fmt "Toplevel" | Intermediate (store, cont, var) -> - fprintf fmt "Intermediate: %a@\n%a@\n%s" (Store.pp pp_val) store - (pp_lst ~pp_sep:(fun fmt () -> fprintf fmt "@\n ") Program.pp_stmt) - cont var + fprintf fmt "Intermediate: %a@\n%a@\n%s" (Store.pp pp_val) store + (pp_lst ~pp_sep:(fun fmt () -> fprintf fmt "@\n ") Program.pp_stmt) + cont var in (pp_lst ~pp_sep:pp_newline pp_frame fmt) cs diff --git a/lib/eval_concrete.ml b/lib/eval_concrete.ml index 42c6454..605667e 100644 --- a/lib/eval_concrete.ml +++ b/lib/eval_concrete.ml @@ -11,13 +11,13 @@ module M : Eval_intf.M with type t = Value.t = struct | Unop (op, e) -> eval_unop_expr op (eval store e) | Binop (op, e1, e2) -> eval_binop_expr op (eval store e1) (eval store e2) | B_symb s -> - failwith - ("InternalError: Eval_concrete.eval, tried to evaluate a symbolic \ - expression" ^ s ^ "in a concrete execution context") + failwith + ( "InternalError: Eval_concrete.eval, tried to evaluate a symbolic \ + expression" ^ s ^ "in a concrete execution context" ) | I_symb s -> - failwith - ("InternalError: Eval_concrete.eval, tried to evaluate a symbolic \ - expression" ^ s ^ "in a concrete execution context") + failwith + ( "InternalError: Eval_concrete.eval, tried to evaluate a symbolic \ + expression" ^ s ^ "in a concrete execution context" ) | Ite (e1, e2, e3) -> eval_ite e1 e2 e3 let is_true (v : t list) : bool = @@ -31,15 +31,15 @@ module M : Eval_intf.M with type t = Value.t = struct match v' with | Boolean b -> b | Integer _ -> - failwith - "InternalError: Eval_concrete.is_true, guard expressions must be of \ - type boolean" + failwith + "InternalError: Eval_concrete.is_true, guard expressions must be of \ + type boolean" | Loc l -> - failwith - ("InternalError: Eval_concrete.is_true, location value " - ^ string_of_int l - ^ " cannot be evaluated to true or false in concrete evaluation \ - contexts") + failwith + ( "InternalError: Eval_concrete.is_true, location value " + ^ string_of_int l + ^ " cannot be evaluated to true or false in concrete evaluation \ + contexts" ) | Error -> failwith "ERROR ERROR" let test_assert (exprs : t list) : bool * Model.t = (is_true exprs, None) @@ -49,9 +49,9 @@ module M : Eval_intf.M with type t = Value.t = struct | Boolean true -> Boolean false | Boolean false -> Boolean true | _ -> - failwith - "InternalError: Eval_concrete.negate, tried to negate a non boolean \ - value" + failwith + "InternalError: Eval_concrete.negate, tried to negate a non boolean \ + value" let pp (fmt : Fmt.t) (v : t) : unit = Value.pp fmt v let to_string (v : t) : string = Fmt.asprintf "%a" pp v diff --git a/lib/eval_expression.ml b/lib/eval_expression.ml index c1f55dc..3528ba5 100644 --- a/lib/eval_expression.ml +++ b/lib/eval_expression.ml @@ -4,169 +4,168 @@ let neg (v : t) : t = match v with | Integer n -> Integer (-1 * n) | _ -> - invalid_arg - "Exception in Oper.neg: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.neg: this operation is only applicable to Integer \ + arguments" let not_ (v : t) : t = match v with | Boolean b -> Boolean (not b) | _ -> - invalid_arg - "Exception in Oper.neg: this operation is only applicable to Boolean \ - arguments" + invalid_arg + "Exception in Oper.neg: this operation is only applicable to Boolean \ + arguments" let abs (v : t) : t = match v with | Integer n -> Integer (abs n) | _ -> - invalid_arg - "Exception in Oper.neg: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.neg: this operation is only applicable to Integer \ + arguments" let stoi (v : t) : t = match v with | _ -> - invalid_arg - "Exception in Oper.stoi: language does not support strings yet" + invalid_arg "Exception in Oper.stoi: language does not support strings yet" let plus ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 + n2) | _ -> - invalid_arg - "Exception in Oper.plus: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.plus: this operation is only applicable to Integer \ + arguments" let minus ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 - n2) | _ -> - invalid_arg - "Exception in Oper.minus: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.minus: this operation is only applicable to Integer \ + arguments" let times ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 * n2) | _ -> - invalid_arg - "Exception in Oper.times: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.times: this operation is only applicable to Integer \ + arguments" let div ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 / n2) | _ -> - invalid_arg - "Exception in Oper.div: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.div: this operation is only applicable to Integer \ + arguments" let modulo ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 mod n2) | _ -> - invalid_arg - "Exception in Oper.modulo: this operation is only applicable to \ - Integer arguments" + invalid_arg + "Exception in Oper.modulo: this operation is only applicable to Integer \ + arguments" let pow ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 * n2) (*TODO*) | _ -> - invalid_arg - "Exception in Oper.modulo: this operation is only applicable to \ - Integer arguments" + invalid_arg + "Exception in Oper.modulo: this operation is only applicable to Integer \ + arguments" let equal ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Boolean (n1 = n2) | Boolean b1, Boolean b2 -> Boolean (b1 = b2) | _ -> - invalid_arg - "Exception in Oper.equal: this operation is only applicable to Integer \ - or Boolean arguments" + invalid_arg + "Exception in Oper.equal: this operation is only applicable to Integer \ + or Boolean arguments" let nequal ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Boolean (n1 != n2) | Boolean b1, Boolean b2 -> Boolean (b1 != b2) | _ -> - invalid_arg - "Exception in Oper.equal: this operation is only applicable to Integer \ - or Boolean arguments" + invalid_arg + "Exception in Oper.equal: this operation is only applicable to Integer \ + or Boolean arguments" let gt ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Boolean (n1 > n2) | _ -> - invalid_arg - "Exception in Oper.gt: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.gt: this operation is only applicable to Integer \ + arguments" let lt ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Boolean (n1 < n2) | _ -> - invalid_arg - "Exception in Oper.lt: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.lt: this operation is only applicable to Integer \ + arguments" let gte ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Boolean (n1 >= n2) | _ -> - invalid_arg - "Exception in Oper.gte: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.gte: this operation is only applicable to Integer \ + arguments" let lte ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Boolean (n1 <= n2) | _ -> - invalid_arg - "Exception in Oper.lte: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.lte: this operation is only applicable to Integer \ + arguments" let or_ ((v1, v2) : t * t) : t = match (v1, v2) with | Boolean b1, Boolean b2 -> Boolean (b1 || b2) | _ -> - invalid_arg - "Exception in Oper.or: this operation is only applicable to Boolean \ - arguments" + invalid_arg + "Exception in Oper.or: this operation is only applicable to Boolean \ + arguments" let and_ ((v1, v2) : t * t) : t = match (v1, v2) with | Boolean b1, Boolean b2 -> Boolean (b1 && b2) | _ -> - invalid_arg - "Exception in Oper.and: this operation is only applicable to Boolean \ - arguments" + invalid_arg + "Exception in Oper.and: this operation is only applicable to Boolean \ + arguments" let xor ((v1, v2) : t * t) : t = match (v1, v2) with | Boolean b1, Boolean b2 -> Boolean ((b1 || b2) && ((not b1) || not b2)) | _ -> - invalid_arg - "Exception in Oper.xor: this operation is only applicable to Boolean \ - arguments" + invalid_arg + "Exception in Oper.xor: this operation is only applicable to Boolean \ + arguments" let shl ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 + n2) (*TODO*) | _ -> - invalid_arg - "Exception in Oper.shl: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.shl: this operation is only applicable to Integer \ + arguments" let shr ((v1, v2) : t * t) : t = match (v1, v2) with | Integer n1, Integer n2 -> Integer (n1 + n2) (*TODO*) | _ -> - invalid_arg - "Exception in Oper.shr: this operation is only applicable to Integer \ - arguments" + invalid_arg + "Exception in Oper.shr: this operation is only applicable to Integer \ + arguments" let eval_unop_expr (op : Term.unop) (v : t) : t = match op with diff --git a/lib/eval_symbolic.ml b/lib/eval_symbolic.ml index 42c71d9..78c375a 100644 --- a/lib/eval_symbolic.ml +++ b/lib/eval_symbolic.ml @@ -26,7 +26,7 @@ module M : Eval_intf.M with type t = Term.t = struct | Unop (op, e) -> Unop (op, simplify_expr e) | Binop (op, e1, e2) -> Binop (op, simplify_expr e1, simplify_expr e2) | Ite (e1, e2, e3) -> - Ite (simplify_expr e1, simplify_expr e2, simplify_expr e3) + Ite (simplify_expr e1, simplify_expr e2, simplify_expr e3) let rec eval (store : st) (e : t) : t = (* We can't reduce the expression 'e' to a value if it contains symbolic variables, so we just replace each symbolic variable with its symbolic value *) @@ -39,18 +39,18 @@ module M : Eval_intf.M with type t = Term.t = struct | Var x -> Store.get store x | Unop (op, e) -> Val (eval store e |> get_val |> eval_unop_expr op) | Binop (op, e1, e2) -> - Val - (eval_binop_expr op - (eval store e1 |> get_val) - (eval store e2 |> get_val)) + Val + (eval_binop_expr op + (eval store e1 |> get_val) + (eval store e2 |> get_val) ) | B_symb _ -> - failwith - "InternalError: Eval_symbolic.eval, tried to evaluate a symbolic \ - boolean" + failwith + "InternalError: Eval_symbolic.eval, tried to evaluate a symbolic \ + boolean" | I_symb _ -> - failwith - "InternalError: Eval_symbolic.eval, tried to evaluate a symbolic \ - integer" + failwith + "InternalError: Eval_symbolic.eval, tried to evaluate a symbolic \ + integer" | Ite (_, _, _) -> failwith "InternalError: concrete Ite not implemented" let is_true (exprs : t list) : bool = Translator.is_sat exprs diff --git a/lib/fmt.ml b/lib/fmt.ml index 6fb6752..9e4909a 100644 --- a/lib/fmt.ml +++ b/lib/fmt.ml @@ -9,7 +9,7 @@ let pp_str (fmt : t) (s : string) : unit = pp_print_string fmt s let pp_bool (fmt : t) (b : bool) : unit = pp_print_bool fmt b let pp_iter ?(pp_sep = pp_print_cut) (iter : ('a -> unit) -> 'b -> unit) - (pp_el : t -> 'a -> unit) (fmt : t) (el : 'b) : unit = + (pp_el : t -> 'a -> unit) (fmt : t) (el : 'b) : unit = let is_first = ref true in let pp_el' el = if !is_first then is_first := false else pp_sep fmt (); @@ -18,13 +18,13 @@ let pp_iter ?(pp_sep = pp_print_cut) (iter : ('a -> unit) -> 'b -> unit) iter pp_el' el let pp_hashtbl ?(pp_sep = pp_print_cut) (pp_v : t -> 'a * 'b -> unit) (fmt : t) - (tbl : ('a, 'b) Hashtbl.t) = + (tbl : ('a, 'b) Hashtbl.t) = let hashtbl_iter f tbl = Hashtbl.iter (fun a b -> f (a, b)) tbl in pp_iter ~pp_sep hashtbl_iter pp_v fmt tbl -let pp_lst ?(pp_sep = pp_print_cut) (pp_v : t -> 'a -> unit) (fmt : t) (lst : 'a list) = +let pp_lst ?(pp_sep = pp_print_cut) (pp_v : t -> 'a -> unit) (fmt : t) + (lst : 'a list) = pp_print_list ~pp_sep pp_v fmt lst - - let pp_newline fmt () = fprintf fmt "@\n" - let pp_comma fmt () = pp_print_string fmt ", " \ No newline at end of file +let pp_newline fmt () = fprintf fmt "@\n" +let pp_comma fmt () = pp_print_string fmt ", " diff --git a/lib/heap/heap_array_fork.ml b/lib/heap/heap_array_fork.ml index 03f032a..d2c55fe 100644 --- a/lib/heap/heap_array_fork.ml +++ b/lib/heap/heap_array_fork.ml @@ -3,13 +3,20 @@ open Value module M : Heap_intf.M with type vt = Term.t = struct type bt = Term.t array - type t = { map : (int, bt) Hashtbl.t; i : int } + + type t = + { map : (int, bt) Hashtbl.t + ; i : int + } + type vt = Term.t let init () : t = { map = Hashtbl.create Parameters.size; i = 0 } let pp_block (fmt : Fmt.t) (block : bt) = - Fmt.fprintf fmt "%a" (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Term.pp) (Array.to_list block) + Fmt.fprintf fmt "%a" + (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Term.pp) + (Array.to_list block) let pp (fmt : Fmt.t) (heap : t) : unit = let open Fmt in @@ -28,85 +35,85 @@ module M : Heap_intf.M with type vt = Term.t = struct let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = match arr with | Val (Loc l) -> ( - match Hashtbl.find_opt heap.map l with - | Some a -> is_within (Array.length a) i pc - | _ -> - failwith - "InternalError: HeapArrayFork.in_bounds, accessed array is not \ - in the heap") + match Hashtbl.find_opt heap.map l with + | Some a -> is_within (Array.length a) i pc + | _ -> + failwith + "InternalError: HeapArrayFork.in_bounds, accessed array is not in \ + the heap" ) | _ -> - failwith "InternalError: HeapArrayFork.in_bounds, arr must be location" + failwith "InternalError: HeapArrayFork.in_bounds, arr must be location" let copy (heap : t) : t = { heap with map = Hashtbl.copy heap.map } let find_block (heap : t) (loc : vt) : int * bt = match loc with | Val (Loc loc') -> ( - let block = Hashtbl.find_opt heap.map loc' in - match block with - | Some block' -> (loc', block') - | None -> failwith "Block does not exist") + let block = Hashtbl.find_opt heap.map loc' in + match block with + | Some block' -> (loc', block') + | None -> failwith "Block does not exist" ) | _ -> failwith "Location needs to be a concrete value" let malloc (heap : t) (size : vt) (path : vt Pc.t) : (t * vt * vt Pc.t) list = match size with | Val (Integer size') -> - let block = Array.make size' (Val (Integer 0)) in - let _ = Hashtbl.add heap.map heap.i block in - [ ({ heap with i = heap.i + 1 }, Val (Loc heap.i), path) ] + let block = Array.make size' (Val (Integer 0)) in + let _ = Hashtbl.add heap.map heap.i block in + [ ({ heap with i = heap.i + 1 }, Val (Loc heap.i), path) ] | _ -> failwith "Size needs to be a concrete integer" let lookup (heap : t) (loc : vt) (index : vt) (path : vt Pc.t) : - (t * vt * vt Pc.t) list = + (t * vt * vt Pc.t) list = let _, block = find_block heap loc in match index with | Val (Integer index') -> - let ret = Array.get block index' in - [ (heap, ret, path) ] + let ret = Array.get block index' in + [ (heap, ret, path) ] | I_symb sym -> - let blockList = Array.to_list block in - let temp = - List.mapi - (fun index' expr -> - let cond = Binop (Equals, I_symb sym, Val (Integer index')) in - (copy heap, expr, Pc.add_condition path cond)) - blockList - in - List.filteri - (fun index' _ -> - (* can be optimized *) - let e = Binop (Equals, index, Val (Integer index')) in - Translator.is_sat ([ e ] @ path)) - temp + let blockList = Array.to_list block in + let temp = + List.mapi + (fun index' expr -> + let cond = Binop (Equals, I_symb sym, Val (Integer index')) in + (copy heap, expr, Pc.add_condition path cond) ) + blockList + in + List.filteri + (fun index' _ -> + (* can be optimized *) + let e = Binop (Equals, index, Val (Integer index')) in + Translator.is_sat ([ e ] @ path) ) + temp | _ -> failwith "Invalid index" let update (heap : t) (loc : vt) (index : vt) (v : vt) (path : vt Pc.t) : - (t * vt Pc.t) list = + (t * vt Pc.t) list = let loc, block = find_block heap loc in match index with | Val (Integer index') -> - let _ = Array.set block index' v in - let _ = Hashtbl.replace heap.map loc block in - [ (heap, path) ] + let _ = Array.set block index' v in + let _ = Hashtbl.replace heap.map loc block in + [ (heap, path) ] | I_symb sym -> - let blockList = Array.to_list block in - let temp = - List.mapi - (fun index' _ -> - let newBlock = Array.copy block in - let newHeap = Hashtbl.copy heap.map in - let _ = Array.set newBlock index' v in - let _ = Hashtbl.replace newHeap loc newBlock in - let cond = Binop (Equals, I_symb sym, Val (Integer index')) in - ({ heap with map = newHeap }, Pc.add_condition path cond)) - blockList - in - List.filteri + let blockList = Array.to_list block in + let temp = + List.mapi (fun index' _ -> - (* can be optimized *) - let e = Binop (Equals, index, Val (Integer index')) in - Translator.is_sat (e :: path)) - temp + let newBlock = Array.copy block in + let newHeap = Hashtbl.copy heap.map in + let _ = Array.set newBlock index' v in + let _ = Hashtbl.replace newHeap loc newBlock in + let cond = Binop (Equals, I_symb sym, Val (Integer index')) in + ({ heap with map = newHeap }, Pc.add_condition path cond) ) + blockList + in + List.filteri + (fun index' _ -> + (* can be optimized *) + let e = Binop (Equals, index, Val (Integer index')) in + Translator.is_sat (e :: path) ) + temp | _ -> failwith "Invalid index" let free (heap : t) (loc : vt) (path : vt Pc.t) : (t * vt Pc.t) list = diff --git a/lib/heap/heap_arrayite.ml b/lib/heap/heap_arrayite.ml index 8936e39..fafe650 100644 --- a/lib/heap/heap_arrayite.ml +++ b/lib/heap/heap_arrayite.ml @@ -8,7 +8,9 @@ module M : Heap_intf.M with type vt = Term.t = struct let init () : t = (Hashtbl.create Parameters.size, 0) let pp_block fmt (block : bt) = - Fmt.fprintf fmt "%a" (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Term.pp) (Array.to_list block) + Fmt.fprintf fmt "%a" + (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Term.pp) + (Array.to_list block) let pp (fmt : Fmt.t) ((heap, _) : t) : unit = let open Fmt in @@ -28,14 +30,14 @@ module M : Heap_intf.M with type vt = Term.t = struct let h, _ = heap in match arr with | Val (Loc l) -> ( - match Hashtbl.find_opt h l with - | Some a -> is_within (Array.length a) i pc - | _ -> - failwith - "InternalError: HeapArrayIte.in_bounds, accessed array is not in \ - the heap") + match Hashtbl.find_opt h l with + | Some a -> is_within (Array.length a) i pc + | _ -> + failwith + "InternalError: HeapArrayIte.in_bounds, accessed array is not in the \ + heap" ) | _ -> - failwith "InternalError: HeapArrayIte.in_bounds, arr must be location" + failwith "InternalError: HeapArrayIte.in_bounds, arr must be location" let copy ((heap, i) : t) : t = (Hashtbl.copy heap, i) @@ -43,103 +45,98 @@ module M : Heap_intf.M with type vt = Term.t = struct let heap', _ = heap in match loc with | Val (Loc loc') -> ( - let block = Hashtbl.find_opt heap' loc' in - match block with - | Some block' -> (loc', block') - | None -> failwith "Block does not exist") + let block = Hashtbl.find_opt heap' loc' in + match block with + | Some block' -> (loc', block') + | None -> failwith "Block does not exist" ) | _ -> failwith "Location needs to be a concrete value" let malloc (h : t) (sz : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = let tbl, next = h in match sz with | Val (Integer i) -> - Hashtbl.replace tbl next (Array.make i (Val (Integer 0))); - [ ((tbl, next + 1), Val (Loc next), pc) ] + Hashtbl.replace tbl next (Array.make i (Val (Integer 0))); + [ ((tbl, next + 1), Val (Loc next), pc) ] | _ -> - failwith "InternalError: HeapArrayIte.malloc, size must be an integer" + failwith "InternalError: HeapArrayIte.malloc, size must be an integer" let update (heap : t) (loc : vt) (index : vt) (v : vt) (path : vt Pc.t) : - (t * vt Pc.t) list = + (t * vt Pc.t) list = let heap', curr = heap in let loc, block = find_block heap loc in match index with | Val (Integer index') -> - let _ = Array.set block index' v in - let _ = Hashtbl.replace heap' loc block in - [ ((heap', curr), path) ] + let _ = Array.set block index' v in + let _ = Hashtbl.replace heap' loc block in + [ ((heap', curr), path) ] | I_symb _ -> - let block' = - Array.mapi - (fun j old_expr -> - let e = Binop (Equals, index, Val (Integer j)) in - if Translator.is_sat (e :: path) then Term.Ite (e, v, old_expr) - else old_expr) - block - in - let _ = Hashtbl.replace heap' loc block' in - [ ((heap', curr), path) ] + let block' = + Array.mapi + (fun j old_expr -> + let e = Binop (Equals, index, Val (Integer j)) in + if Translator.is_sat (e :: path) then Term.Ite (e, v, old_expr) + else old_expr ) + block + in + let _ = Hashtbl.replace heap' loc block' in + [ ((heap', curr), path) ] | _ -> failwith "Invalid index" let lookup (h : t) (arr : vt) (index : vt) (pc : vt Pc.t) : - (t * vt * vt Pc.t) list = + (t * vt * vt Pc.t) list = let tbl, _ = h in match index with | Val (Integer i) -> ( - (* quando o 'index' tem tipo "value", por exemplo: 5,2,... *) - match arr with - | Val (Loc l) -> ( - match Hashtbl.find_opt tbl l with - | Some arr -> [ (h, arr.(i), pc) ] - | _ -> - failwith - "InternalError: HeapArrayIte, accessed array is not in the \ - heap") + (* quando o 'index' tem tipo "value", por exemplo: 5,2,... *) + match arr with + | Val (Loc l) -> ( + match Hashtbl.find_opt tbl l with + | Some arr -> [ (h, arr.(i), pc) ] | _ -> - failwith - "InternalError: HeapArrayIte.update, arr must be a location") + failwith + "InternalError: HeapArrayIte, accessed array is not in the heap" ) + | _ -> + failwith "InternalError: HeapArrayIte.update, arr must be a location" ) | _ -> ( - (* quando o 'index' tem tipo "expression", por exemplo: Binop(+,x_hat,2), Symb y_hat,... *) - match arr with - | Val (Loc l) -> ( - match Hashtbl.find_opt tbl l with - | Some arr -> - let aux = - Array.of_list - (List.filteri - (fun index' _ -> - (* can be optimized *) - let e = Binop (Equals, index, Val (Integer index')) in - Translator.is_sat (e :: pc)) - (Array.to_list - (Array.mapi - (fun j e -> - (Binop (Equals, index, Val (Integer j)), e)) - arr))) - in - let f (bop, e) l = - match e with - | Ite (a, b, _) -> Ite (Binop (And, bop, a), b, l) - | _ -> Ite (bop, e, l) - in - let expr = Array.fold_right f aux (Val (Integer 0)) in - [ (h, expr, pc) ] - | _ -> - failwith - "InternalError: HeapArrayIte, accessed array is not in the \ - heap") + (* quando o 'index' tem tipo "expression", por exemplo: Binop(+,x_hat,2), Symb y_hat,... *) + match arr with + | Val (Loc l) -> ( + match Hashtbl.find_opt tbl l with + | Some arr -> + let aux = + Array.of_list + (List.filteri + (fun index' _ -> + (* can be optimized *) + let e = Binop (Equals, index, Val (Integer index')) in + Translator.is_sat (e :: pc) ) + (Array.to_list + (Array.mapi + (fun j e -> (Binop (Equals, index, Val (Integer j)), e)) + arr ) ) ) + in + let f (bop, e) l = + match e with + | Ite (a, b, _) -> Ite (Binop (And, bop, a), b, l) + | _ -> Ite (bop, e, l) + in + let expr = Array.fold_right f aux (Val (Integer 0)) in + [ (h, expr, pc) ] | _ -> - failwith - "InternalError: HeapArrayIte.update, arr must be a location") + failwith + "InternalError: HeapArrayIte, accessed array is not in the heap" ) + | _ -> + failwith "InternalError: HeapArrayIte.update, arr must be a location" ) let free (h : t) (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = let tbl, _ = h in match arr with | Val (Loc l) -> ( - match Hashtbl.find_opt tbl l with - | Some _ -> - Hashtbl.remove tbl l; - [ (h, pc) ] - | _ -> failwith "InternalError: HeapArrayIte.free, illegal free") + match Hashtbl.find_opt tbl l with + | Some _ -> + Hashtbl.remove tbl l; + [ (h, pc) ] + | _ -> failwith "InternalError: HeapArrayIte.free, illegal free" ) | _ -> failwith "InternalError: HeapArrayIte.free, arr must be location" let clone h = copy h diff --git a/lib/heap/heap_concolic.ml b/lib/heap/heap_concolic.ml index da8d5db..d87efb2 100644 --- a/lib/heap/heap_concolic.ml +++ b/lib/heap/heap_concolic.ml @@ -3,26 +3,19 @@ module M = struct type vt = Value.t * Term.t (* indexes and sizes are always values *) let init () : t = Hashtbl.create Parameters.size - - let pp (_fmt : Fmt.t) (_heap : t) : unit = - failwith "Not Implemented" - - let to_string (_h : t) : string = - failwith "Not Implemented" - - let malloc _h (_sz : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = - [] + let pp (_fmt : Fmt.t) (_heap : t) : unit = failwith "Not Implemented" + let to_string (_h : t) : string = failwith "Not Implemented" + let malloc _h (_sz : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = [] let update _h (_arr : vt) (_index : vt) (_v : vt) (_pc : vt Pc.t) : - (t * vt Pc.t) list = + (t * vt Pc.t) list = [] - let lookup _h (_arr : vt) (_index : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list - = + let lookup _h (_arr : vt) (_index : vt) (_pc : vt Pc.t) : + (t * vt * vt Pc.t) list = [] - let free _h (_arr : vt) (_pc : vt Pc.t) : (t * vt Pc.t) list = - [] + let free _h (_arr : vt) (_pc : vt Pc.t) : (t * vt Pc.t) list = [] let in_bounds (_heap : t) (_v : vt) (_i : vt) (_pc : vt Pc.t) : bool = failwith "not implemented" diff --git a/lib/heap/heap_concrete.ml b/lib/heap/heap_concrete.ml index 25ff7c0..dadaeec 100644 --- a/lib/heap/heap_concrete.ml +++ b/lib/heap/heap_concrete.ml @@ -8,7 +8,9 @@ module M : Heap_intf.M with type vt = Value.t = struct let init () : t = (Hashtbl.create Parameters.size, 0) let pp_block fmt (block : bt) = - Fmt.fprintf fmt "%a" (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Value.pp) (Array.to_list block) + Fmt.fprintf fmt "%a" + (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Value.pp) + (Array.to_list block) let pp (fmt : Fmt.t) ((heap, _) : t) : unit = let open Fmt in @@ -21,65 +23,65 @@ module M : Heap_intf.M with type vt = Value.t = struct let tbl, next = h in match sz with | Integer i -> - Hashtbl.replace tbl next (Array.make i (Integer 0)); - [ ((tbl, next + 1), Loc next, pc) ] + Hashtbl.replace tbl next (Array.make i (Integer 0)); + [ ((tbl, next + 1), Loc next, pc) ] | _ -> - failwith "InternalError: HeapConcrete.malloc, size must be an integer" + failwith "InternalError: HeapConcrete.malloc, size must be an integer" let update (h : t) (arr : vt) (index : vt) (v : vt) (pc : vt Pc.t) : - (t * vt Pc.t) list = + (t * vt Pc.t) list = let tbl, _ = h in match (arr, index) with | Loc l, Integer i -> ( - match Hashtbl.find_opt tbl l with - | Some arr -> - arr.(i) <- v; - [ (h, pc) ] - | _ -> failwith "InternalError: accessed array is not in the heap") + match Hashtbl.find_opt tbl l with + | Some arr -> + arr.(i) <- v; + [ (h, pc) ] + | _ -> failwith "InternalError: accessed array is not in the heap" ) | _ -> - failwith - "InternalError: HeapConcrete.update, arr must be location and index \ - must be an integer" + failwith + "InternalError: HeapConcrete.update, arr must be location and index \ + must be an integer" let lookup (h : t) (arr : vt) (index : vt) (pc : vt Pc.t) : - (t * vt * vt Pc.t) list = + (t * vt * vt Pc.t) list = let tbl, _ = h in match (arr, index) with | Loc l, Integer i -> ( - match Hashtbl.find_opt tbl l with - | Some arr -> - if Array.length arr <= i then - failwith "InternalError: accessing out-of-bounds index" - else [ (h, arr.(i), pc) ] - | _ -> failwith "InternalError: accessed array is not in the heap") + match Hashtbl.find_opt tbl l with + | Some arr -> + if Array.length arr <= i then + failwith "InternalError: accessing out-of-bounds index" + else [ (h, arr.(i), pc) ] + | _ -> failwith "InternalError: accessed array is not in the heap" ) | _ -> - failwith - "InternalError: HeapConcrete.update, arr must be location and index \ - must be an integer" + failwith + "InternalError: HeapConcrete.update, arr must be location and index \ + must be an integer" let free (h : t) (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = let tbl, _ = h in match arr with | Loc l -> ( - match Hashtbl.find_opt tbl l with - | Some _ -> - Hashtbl.remove tbl l; - [ (h, pc) ] - | _ -> failwith "InternalError: illegal free") + match Hashtbl.find_opt tbl l with + | Some _ -> + Hashtbl.remove tbl l; + [ (h, pc) ] + | _ -> failwith "InternalError: illegal free" ) | _ -> failwith "InternalError: HeapConcrete.update, arr must be location" let in_bounds (heap : t) (addr : vt) (i : vt) (_pc : vt Pc.t) : bool = match addr with | Loc l -> ( - let tbl, _ = heap in - match Hashtbl.find_opt tbl l with - | Some arr -> Integer 0 < i && i < Integer (Array.length arr) - | _ -> - failwith - "InternalError: HeapConcrete.in_bounds, accessed array is not in \ - the heap") + let tbl, _ = heap in + match Hashtbl.find_opt tbl l with + | Some arr -> Integer 0 < i && i < Integer (Array.length arr) + | _ -> + failwith + "InternalError: HeapConcrete.in_bounds, accessed array is not in the \ + heap" ) | _ -> - failwith "InternalError: HeapConcrete.in_bounds, arr must be location" + failwith "InternalError: HeapConcrete.in_bounds, arr must be location" let clone _ = assert false end diff --git a/lib/heap/heap_oplist.ml b/lib/heap/heap_oplist.ml index 3ae63cb..4313cfa 100644 --- a/lib/heap/heap_oplist.ml +++ b/lib/heap/heap_oplist.ml @@ -2,7 +2,12 @@ module M : Heap_intf.M with type vt = Term.t = struct type addr = int type size = Term.t type op = Term.t * Term.t * Term.t Pc.t - type t = { map : (addr, size * op list) Hashtbl.t; mutable next : int } + + type t = + { map : (addr, size * op list) Hashtbl.t + ; mutable next : int + } + type vt = Term.t let init () : t = { map = Hashtbl.create Parameters.size; next = 0 } @@ -30,17 +35,16 @@ module M : Heap_intf.M with type vt = Term.t = struct let in_bounds (heap : t) (v : vt) (i : vt) (pc : vt Pc.t) : bool = match v with | Val (Loc l) -> ( - match Hashtbl.find_opt heap.map l with - | Some (sz, _) -> ( - match sz with - | Val (Integer _) | I_symb _ -> is_within sz i pc - | _ -> - failwith - "InternalError: HeapOpList.in_bounds, size not an integer") + match Hashtbl.find_opt heap.map l with + | Some (sz, _) -> ( + match sz with + | Val (Integer _) | I_symb _ -> is_within sz i pc | _ -> - failwith - "InternalError: HeapOpList.in_bounds, accessed OpList is not in \ - the heap") + failwith "InternalError: HeapOpList.in_bounds, size not an integer" ) + | _ -> + failwith + "InternalError: HeapOpList.in_bounds, accessed OpList is not in the \ + heap" ) | _ -> failwith "InternalError: HeapOpList.in_bounds, v must be location" let malloc (h : t) (sz : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = @@ -50,7 +54,7 @@ module M : Heap_intf.M with type vt = Term.t = struct [ (h, Val (Loc next), pc) ] let update (h : t) (arr : vt) (index : vt) (v : vt) (pc : vt Pc.t) : - (t * vt Pc.t) list = + (t * vt Pc.t) list = let lbl = match arr with Val (Loc i) -> i | _ -> assert false in let arr' = Hashtbl.find_opt h.map lbl in let f ((sz, oplist) : size * op list) : unit = @@ -67,7 +71,7 @@ module M : Heap_intf.M with type vt = Term.t = struct let v = List.fold_left (fun ac (i, v, _) -> - Term.Ite (Term.Binop (Term.Equals, index, i), v, ac)) + Term.Ite (Term.Binop (Term.Equals, index, i), v, ac) ) (Term.Val (Value.Integer 0)) (List.rev ops) in [ (h, v, pc) ] diff --git a/lib/heap/heap_symbolic.ml b/lib/heap/heap_symbolic.ml index 64faaf5..95c95ab 100644 --- a/lib/heap/heap_symbolic.ml +++ b/lib/heap/heap_symbolic.ml @@ -3,22 +3,18 @@ module M : Heap_intf.M with type vt = Term.t = struct type vt = Term.t let init () : t = Hashtbl.create Parameters.size - - let pp (_fmt : Fmt.t) (_heap : t) : unit = - failwith "Not Implemented" - - let to_string (_h : t) : string = - failwith "Not Implemented" + let pp (_fmt : Fmt.t) (_heap : t) : unit = failwith "Not Implemented" + let to_string (_h : t) : string = failwith "Not Implemented" let malloc _h (_sz : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = assert false let update _h (_arr : vt) (_index : vt) (_v : vt) (_pc : vt Pc.t) : - (t * vt Pc.t) list = + (t * vt Pc.t) list = assert false let lookup _h (_arr : vt) (_index : vt) (_pc : vt Pc.t) : - (t * vt * vt Pc.t) list = + (t * vt * vt Pc.t) list = assert false let free _h (_arr : vt) (_pc : vt Pc.t) : (t * vt Pc.t) list = assert false diff --git a/lib/heap/heap_tree.ml b/lib/heap/heap_tree.ml index 686356d..09e177f 100644 --- a/lib/heap/heap_tree.ml +++ b/lib/heap/heap_tree.ml @@ -2,25 +2,26 @@ module M : Heap_intf.M with type vt = Term.t = struct type vt = Term.t type range = vt * vt - type tree_t = Leaf of range * vt | Node of range * tree_t list + type tree_t = + | Leaf of range * vt + | Node of range * tree_t list type t = (int, tree_t) Hashtbl.t * int let init () : t = (Hashtbl.create Parameters.size, 0) let rec pp_block (fmt : Fmt.t) (block : tree_t) : unit = - let open Fmt in + let open Fmt in match block with - | Leaf ((l, r), v) -> + | Leaf ((l, r), v) -> fprintf fmt "{ \"leaf\": { \"range\": \"[%a, %a]\", \"value\": \"%a\"} }" - Term.pp l - Term.pp r - Term.pp v - | Node ((l, r), ch) -> - fprintf fmt "{ \"node\": { \"range\": \"[%a, %a]\", \"children\": [ %a ]} }" - Term.pp l - Term.pp r - (pp_lst ~pp_sep:pp_comma pp_block) ch + Term.pp l Term.pp r Term.pp v + | Node ((l, r), ch) -> + fprintf fmt + "{ \"node\": { \"range\": \"[%a, %a]\", \"children\": [ %a ]} }" Term.pp + l Term.pp r + (pp_lst ~pp_sep:pp_comma pp_block) + ch let pp (fmt : Fmt.t) ((heap, _) : t) : unit = let open Fmt in @@ -45,71 +46,70 @@ module M : Heap_intf.M with type vt = Term.t = struct [ ((h', curr + 1), Term.Val (Loc curr), pc) ] let update h (arr : vt) (index : vt) (v : vt) (pc : vt Pc.t) : - (t * vt Pc.t) list = + (t * vt Pc.t) list = let h', next = h in let rec update_tree (tree : tree_t) (index : vt) (v : vt) (pc : vt Pc.t) : - (tree_t * vt Pc.t) list option = + (tree_t * vt Pc.t) list option = match tree with | Leaf ((left, right), old_v) -> - let ge_left = Term.Binop (Gte, index, left) in - let l_right = Term.Binop (Lt, index, right) in - let cond = Term.Binop (And, ge_left, l_right) in - let pc' = cond :: pc in - if Translator.is_sat pc' then - let index_plus_1 = Term.Binop (Plus, index, Val (Integer 1)) in - let leaves = - [ - Leaf ((left, index), old_v); - Leaf ((index, index_plus_1), v); - Leaf ((index_plus_1, right), old_v); - ] - in - Some [ (Node ((left, right), leaves), pc') ] - else None + let ge_left = Term.Binop (Gte, index, left) in + let l_right = Term.Binop (Lt, index, right) in + let cond = Term.Binop (And, ge_left, l_right) in + let pc' = cond :: pc in + if Translator.is_sat pc' then + let index_plus_1 = Term.Binop (Plus, index, Val (Integer 1)) in + let leaves = + [ Leaf ((left, index), old_v) + ; Leaf ((index, index_plus_1), v) + ; Leaf ((index_plus_1, right), old_v) + ] + in + Some [ (Node ((left, right), leaves), pc') ] + else None | Node ((left, right), trees) -> - let ge_left = Term.Binop (Gte, index, left) in - let l_right = Term.Binop (Lt, index, right) in - let cond = Term.Binop (And, ge_left, l_right) in - let pc' = cond :: pc in - if Translator.is_sat pc' then - let l = List.map (fun t -> update_tree t index v pc') trees in - let t1, t2, t3 = - match trees with - | t1 :: t2 :: [ t3 ] -> (t1, t2, t3) - | _ -> failwith "unreachable" - in - match l with - | nt1 :: nt2 :: [ nt3 ] -> - let l1 = - match nt1 with - | Some l1 -> - List.map - (fun (nt1, pc1) -> - (Node ((left, right), [ nt1; t2; t3 ]), pc1)) - l1 - | None -> [] - in - let l2 = - match nt2 with - | Some l2 -> - List.map - (fun (nt2, pc2) -> - (Node ((left, right), [ t1; nt2; t3 ]), pc2)) - l2 - | None -> [] - in - let l3 = - match nt3 with - | Some l3 -> - List.map - (fun (nt3, pc3) -> - (Node ((left, right), [ t1; t2; nt3 ]), pc3)) - l3 - | None -> [] - in - Some (l1 @ l2 @ l3) + let ge_left = Term.Binop (Gte, index, left) in + let l_right = Term.Binop (Lt, index, right) in + let cond = Term.Binop (And, ge_left, l_right) in + let pc' = cond :: pc in + if Translator.is_sat pc' then + let l = List.map (fun t -> update_tree t index v pc') trees in + let t1, t2, t3 = + match trees with + | t1 :: t2 :: [ t3 ] -> (t1, t2, t3) | _ -> failwith "unreachable" - else None + in + match l with + | nt1 :: nt2 :: [ nt3 ] -> + let l1 = + match nt1 with + | Some l1 -> + List.map + (fun (nt1, pc1) -> + (Node ((left, right), [ nt1; t2; t3 ]), pc1) ) + l1 + | None -> [] + in + let l2 = + match nt2 with + | Some l2 -> + List.map + (fun (nt2, pc2) -> + (Node ((left, right), [ t1; nt2; t3 ]), pc2) ) + l2 + | None -> [] + in + let l3 = + match nt3 with + | Some l3 -> + List.map + (fun (nt3, pc3) -> + (Node ((left, right), [ t1; t2; nt3 ]), pc3) ) + l3 + | None -> [] + in + Some (l1 @ l2 @ l3) + | _ -> failwith "unreachable" + else None in let i = match arr with @@ -120,12 +120,12 @@ module M : Heap_intf.M with type vt = Term.t = struct let new_trees = update_tree tree index v pc in match new_trees with | Some new_trees -> - List.map - (fun (new_tree, pc') -> - let new_h = Hashtbl.copy h' in - Hashtbl.replace new_h i new_tree; - ((new_h, next), pc')) - new_trees + List.map + (fun (new_tree, pc') -> + let new_h = Hashtbl.copy h' in + Hashtbl.replace new_h i new_tree; + ((new_h, next), pc') ) + new_trees | None -> failwith "Out of bounds access" let must_within_range (r : range) (index : vt) (pc : vt Pc.t) : bool = @@ -146,24 +146,23 @@ module M : Heap_intf.M with type vt = Term.t = struct Translator.is_sat ([ e1; e2 ] @ pc) let rec search_tree (index : vt) (pc : vt Pc.t) (tree : tree_t) : - (vt * vt) list = + (vt * vt) list = match tree with | Leaf (r, v) -> - let lower, upper = r in - let in_range = may_within_range r index pc in - if in_range then - [ - ( v, - Term.Binop - ( And, - Term.Binop (Lt, index, upper), - Term.Binop (Gte, index, lower) ) ); - ] - else [] + let lower, upper = r in + let in_range = may_within_range r index pc in + if in_range then + [ ( v + , Term.Binop + ( And + , Term.Binop (Lt, index, upper) + , Term.Binop (Gte, index, lower) ) ) + ] + else [] | Node (r, tree_list) -> - let in_range = may_within_range r index pc in - if in_range then List.concat (List.map (search_tree index pc) tree_list) - else [] + let in_range = may_within_range r index pc in + if in_range then List.concat (List.map (search_tree index pc) tree_list) + else [] let lookup h (arr : vt) (index : vt) (pc : vt Pc.t) : (t * vt * vt Pc.t) list = @@ -171,28 +170,27 @@ module M : Heap_intf.M with type vt = Term.t = struct match arr with | Val (Loc l) -> ( - match Hashtbl.find_opt tbl l with - | Some tree -> - let v = - List.fold_left - (fun ac (v, c) -> Term.Ite (c, v, ac)) - (Term.Val (Value.Integer 0)) - (search_tree index pc tree) - in - [ (h, v, pc) ] - | _ -> - failwith - "InternalError: HeapTree.lookup, accessed tree is not in the heap" - ) + match Hashtbl.find_opt tbl l with + | Some tree -> + let v = + List.fold_left + (fun ac (v, c) -> Term.Ite (c, v, ac)) + (Term.Val (Value.Integer 0)) + (search_tree index pc tree) + in + [ (h, v, pc) ] + | _ -> + failwith + "InternalError: HeapTree.lookup, accessed tree is not in the heap" ) | _ -> failwith "InternalError: HeapTree.lookup, arr must be location" let free h (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = let h', _ = h in (* let ign = to_string h in ignore ign; *) - (match arr with + ( match arr with | Val (Loc i) -> Hashtbl.remove h' i - | _ -> failwith "Invalid allocation index"); + | _ -> failwith "Invalid allocation index" ); [ (h, pc) ] let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = @@ -200,14 +198,13 @@ module M : Heap_intf.M with type vt = Term.t = struct let h', _ = heap in match arr with | Val (Loc l) -> ( - match Hashtbl.find_opt h' l with - | Some tree -> ( - match tree with - | Leaf (r, _) | Node (r, _) -> must_within_range r i pc) - | _ -> - failwith - "InternalError: HeapTree.in_bounds, accessed tree is not in the \ - heap") + match Hashtbl.find_opt h' l with + | Some tree -> ( + match tree with Leaf (r, _) | Node (r, _) -> must_within_range r i pc ) + | _ -> + failwith + "InternalError: HeapTree.in_bounds, accessed tree is not in the heap" + ) | _ -> failwith "InternalError: HeapTree.in_bounds, arr must be location" let copy ((heap, i) : t) : t = (Hashtbl.copy heap, i) diff --git a/lib/interpreter.ml b/lib/interpreter.ml index 1d1ad4f..caedac5 100644 --- a/lib/interpreter.ml +++ b/lib/interpreter.ml @@ -32,11 +32,10 @@ module Make let main = Program.get_function Parameters.main_id program in let state = Sstate. - { - heap = Heap.init (); - store = Store.create_empty_store Parameters.size; - pc = Pc.create_pathcondition; - cs = Callstack.create_callstack; + { heap = Heap.init () + ; store = Store.create_empty_store Parameters.size + ; pc = Pc.create_pathcondition + ; cs = Callstack.create_callstack } in (state, [ main.body ]) @@ -49,224 +48,223 @@ module Make (* The 'step' function is a small-step semantics evaluator and uses the "continuations" trick, and thus it is tail recursive. Note: the evaluation of expressions is big-step *) let rec step (prog : program) (s : Program.stmt) (cont : Program.stmt list) : - Outcome.t Choice.t = + Outcome.t Choice.t = let return stmts = Choice.return (Outcome.Cont stmts) in - if !Utils.verbose then (* Printf.printf "\n"; - let/ state = Choice.get in - Printf.printf "Heap: %s\n" (Heap.to_string state.heap); - Printf.printf "State: %s\n" (Sstate.to_string Eval.pp Heap.pp state); *) - Fmt.printf "Stmt: %a@." Program.pp_stmt s; + if !Utils.verbose then + (* Printf.printf "\n"; + let/ state = Choice.get in + Printf.printf "Heap: %s\n" (Heap.to_string state.heap); + Printf.printf "State: %s\n" (Sstate.to_string Eval.pp Heap.pp state); *) + Fmt.printf "Stmt: %a@." Program.pp_stmt s; match s with | Skip | Clear -> return cont | Sequence (s1 :: s2) -> step prog s1 (s2 @ cont) | Assign (x, e) -> - let/ state = Choice.get in - let e' = eval state.store e in - Store.set state.store x e'; - return cont + let/ state = Choice.get in + let e' = eval state.store e in + Store.set state.store x e'; + return cont | Symbol_bool (x, s) -> ( - let symb_opt = make_symbol s "bool" in - match symb_opt with - | None -> - failwith - "ApplicationError: tried to create a symbolic value in a \ - concrete execution context" - | Some symb_val -> - let/ state = Choice.get in - Store.set state.store x symb_val; - return cont) + let symb_opt = make_symbol s "bool" in + match symb_opt with + | None -> + failwith + "ApplicationError: tried to create a symbolic value in a concrete \ + execution context" + | Some symb_val -> + let/ state = Choice.get in + Store.set state.store x symb_val; + return cont ) | Symbol_int (x, s) -> ( - let symb_opt = make_symbol s "int" in - match symb_opt with - | None -> - failwith - "ApplicationError: tried to create a symbolic value in a \ - concrete execution context" - | Some symb_val -> - let/ state = Choice.get in - Store.set state.store x symb_val; - return cont) + let symb_opt = make_symbol s "int" in + match symb_opt with + | None -> + failwith + "ApplicationError: tried to create a symbolic value in a concrete \ + execution context" + | Some symb_val -> + let/ state = Choice.get in + Store.set state.store x symb_val; + return cont ) | Symbol_int_c (x, s, c) -> ( - let symb_opt = make_symbol s "int" in - match symb_opt with - | None -> - failwith - "ApplicationError: tried to create a symbolic value in a \ - concrete execution context" - | Some symb_val -> - let f_symb_int (s : state) = - Store.set s.store x symb_val; - let v = eval s.store c in - let pc' = add_condition s.pc v in - if is_true pc' then [ ((), Sstate.{ s with pc = pc' }) ] else [] - in - let/ () = Choice.lift f_symb_int in - return cont) + let symb_opt = make_symbol s "int" in + match symb_opt with + | None -> + failwith + "ApplicationError: tried to create a symbolic value in a concrete \ + execution context" + | Some symb_val -> + let f_symb_int (s : state) = + Store.set s.store x symb_val; + let v = eval s.store c in + let pc' = add_condition s.pc v in + if is_true pc' then [ ((), Sstate.{ s with pc = pc' }) ] else [] + in + let/ () = Choice.lift f_symb_int in + return cont ) | Print es -> - let/ state = Choice.get in - let vs = List.map (eval state.store) es in - print_endline ">Program Print"; - List.iter Eval.print vs; - print_endline ""; - return cont + let/ state = Choice.get in + let vs = List.map (eval state.store) es in + print_endline ">Program Print"; + List.iter Eval.print vs; + print_endline ""; + return cont | FunCall (x, f, es) -> - let/ state = Choice.get in - let vs = List.map (eval state.store) es in - let f' = Program.get_function f prog in - let xs = f'.args in - let xvs = - try List.combine xs vs - with _ -> - failwith ("TypeError: Argument arity mismatch when calling " ^ f) - in - let sto' = Store.create_store xvs in - let frame = Callstack.Intermediate (state.store, cont, x) in - let cs' = Callstack.push state.cs frame in - let/ _ = Choice.set { state with cs = cs'; store = sto' } in - return [ f'.body ] + let/ state = Choice.get in + let vs = List.map (eval state.store) es in + let f' = Program.get_function f prog in + let xs = f'.args in + let xvs = + try List.combine xs vs + with _ -> + failwith ("TypeError: Argument arity mismatch when calling " ^ f) + in + let sto' = Store.create_store xvs in + let frame = Callstack.Intermediate (state.store, cont, x) in + let cs' = Callstack.push state.cs frame in + let/ _ = Choice.set { state with cs = cs'; store = sto' } in + return [ f'.body ] | Return e -> ( - let/ state = Choice.get in - let v = eval state.store e in - let frame = Callstack.top state.cs in - let cs' = Callstack.pop state.cs in - match frame with - | Callstack.Intermediate (sto', cont', x) -> - let sto'' = Store.dup sto' in - Store.set sto'' x v; - let/ _ = Choice.set { state with cs = cs'; store = sto'' } in - return cont' - | Callstack.Toplevel -> - let/ _ = Choice.set { state with cs = cs' } in - Choice.return @@ Outcome.Return (Eval.to_string v)) + let/ state = Choice.get in + let v = eval state.store e in + let frame = Callstack.top state.cs in + let cs' = Callstack.pop state.cs in + match frame with + | Callstack.Intermediate (sto', cont', x) -> + let sto'' = Store.dup sto' in + Store.set sto'' x v; + let/ _ = Choice.set { state with cs = cs'; store = sto'' } in + return cont' + | Callstack.Toplevel -> + let/ _ = Choice.set { state with cs = cs' } in + Choice.return @@ Outcome.Return (Eval.to_string v) ) | IfElse (e, s1, s2) -> - let/ state = Choice.get in - let v = eval state.store e in - let/ b = Choice.select v in - if b then return (s1 :: cont) else return (s2 :: cont) + let/ state = Choice.get in + let v = eval state.store e in + let/ b = Choice.select v in + if b then return (s1 :: cont) else return (s2 :: cont) | While (e, body) as while_stmt -> - let/ state = Choice.get in - let v = eval state.store e in - let/ b = Choice.select v in - if b then return (body :: while_stmt :: cont) else return cont + let/ state = Choice.get in + let v = eval state.store e in + let/ b = Choice.select v in + if b then return (body :: while_stmt :: cont) else return cont | Assume e -> - let/ state = Choice.get in - let v = eval state.store e in - let/ b = Choice.select v in - (* Printf.printf "b = %b\n" (b); *) - if b then return cont else Choice.return Outcome.AssumeF + let/ state = Choice.get in + let v = eval state.store e in + let/ b = Choice.select v in + (* Printf.printf "b = %b\n" (b); *) + if b then return cont else Choice.return Outcome.AssumeF | Assert e -> - let/ state = Choice.get in - let v = eval state.store e in - let/ b = Choice.select v in - if b then return cont - else - let/ state' = Choice.get in - let _, model = Eval.test_assert state'.pc in - Choice.return @@ Outcome.Error model + let/ state = Choice.get in + let v = eval state.store e in + let/ b = Choice.select v in + if b then return cont + else + let/ state' = Choice.get in + let _, model = Eval.test_assert state'.pc in + Choice.return @@ Outcome.Error model | New (x, e) -> - let f_new (s : state) = - let size = eval s.store e in - let lst = Heap.malloc s.heap size s.pc in - List.map - (fun (hp, loc, pc') -> - ( loc, - Sstate. - { - heap = hp; - pc = pc'; - store = Store.dup s.store; - cs = Callstack.dup s.cs; - } )) - lst - in - let/ l = Choice.lift f_new in - let/ state = Choice.get in - Store.set state.store x l; - return cont + let f_new (s : state) = + let size = eval s.store e in + let lst = Heap.malloc s.heap size s.pc in + List.map + (fun (hp, loc, pc') -> + ( loc + , Sstate. + { heap = hp + ; pc = pc' + ; store = Store.dup s.store + ; cs = Callstack.dup s.cs + } ) ) + lst + in + let/ l = Choice.lift f_new in + let/ state = Choice.get in + Store.set state.store x l; + return cont | Update (a, index, e) -> - let f_update (s : state) = - match Store.get_opt s.store a with - | Some loc -> - let index_v = eval s.store index in - let v = eval s.store e in - let b = Heap.in_bounds s.heap loc index_v s.pc in - if b then - let lst = Heap.update s.heap loc index_v v s.pc in - let dup = List.length lst > 1 in - List.map - (fun (hp, pc') -> - let store', cs' = - if dup then (Store.dup s.store, Callstack.dup s.cs) - else (s.store, s.cs) - in - ( (), - Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' } - )) - lst - else failwith "Index out of bounds" - | None -> failwith "InternalError: array is not defined" - in - let/ _ = Choice.lift f_update in - return cont + let f_update (s : state) = + match Store.get_opt s.store a with + | Some loc -> + let index_v = eval s.store index in + let v = eval s.store e in + let b = Heap.in_bounds s.heap loc index_v s.pc in + if b then + let lst = Heap.update s.heap loc index_v v s.pc in + let dup = List.length lst > 1 in + List.map + (fun (hp, pc') -> + let store', cs' = + if dup then (Store.dup s.store, Callstack.dup s.cs) + else (s.store, s.cs) + in + ((), Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' }) + ) + lst + else failwith "Index out of bounds" + | None -> failwith "InternalError: array is not defined" + in + let/ _ = Choice.lift f_update in + return cont | LookUp (x, a, index) -> - let f_lookup (s : state) = - match Store.get_opt s.store a with - | Some loc -> - let index_v = eval s.store index in - let b = Heap.in_bounds s.heap loc index_v s.pc in - if b then - let lst = Heap.lookup s.heap loc index_v s.pc in - let dup = List.length lst > 1 in + let f_lookup (s : state) = + match Store.get_opt s.store a with + | Some loc -> + let index_v = eval s.store index in + let b = Heap.in_bounds s.heap loc index_v s.pc in + if b then + let lst = Heap.lookup s.heap loc index_v s.pc in + let dup = List.length lst > 1 in - List.map - (fun (hp, v, pc') -> - let store', cs' = - if dup then (Store.dup s.store, Callstack.dup s.cs) - else (s.store, s.cs) - in - (v, Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' })) - lst - else failwith "Index out of bounds" - | None -> failwith "InternalError: array is not defined" - in - let/ v = Choice.lift f_lookup in - let/ state = Choice.get in - Store.set state.store x v; - return cont + List.map + (fun (hp, v, pc') -> + let store', cs' = + if dup then (Store.dup s.store, Callstack.dup s.cs) + else (s.store, s.cs) + in + (v, Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' }) ) + lst + else failwith "Index out of bounds" + | None -> failwith "InternalError: array is not defined" + in + let/ v = Choice.lift f_lookup in + let/ state = Choice.get in + Store.set state.store x v; + return cont | Delete a -> - let f_delete (s : state) = - match Store.get_opt s.store a with - | Some loc -> - let lst = Heap.free s.heap loc s.pc in - let dup = List.length lst > 1 in + let f_delete (s : state) = + match Store.get_opt s.store a with + | Some loc -> + let lst = Heap.free s.heap loc s.pc in + let dup = List.length lst > 1 in - List.map - (fun (hp, pc') -> - let store', cs' = - if dup then (Store.dup s.store, Callstack.dup s.cs) - else (s.store, s.cs) - in - ((), Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' })) - lst - | None -> failwith "InternalError: array is not defined" - in - let/ () = Choice.lift f_delete in - return cont + List.map + (fun (hp, pc') -> + let store', cs' = + if dup then (Store.dup s.store, Callstack.dup s.cs) + else (s.store, s.cs) + in + ((), Sstate.{ heap = hp; pc = pc'; store = store'; cs = cs' }) ) + lst + | None -> failwith "InternalError: array is not defined" + in + let/ () = Choice.lift f_delete in + return cont | _ -> assert false (* The 'search' function contains all the logic of the search of the state space, it kinda is like a scheduler of states *) let rec search (gas : int) (prog : program) (cont : Program.stmt list) : - Outcome.t Choice.t = + Outcome.t Choice.t = if gas = 0 then Choice.return Outcome.EndGas else match cont with (* allows programs to terminate without return-stmt *) | [] -> Choice.return (Outcome.Return "0") | s :: cont' -> ( - let/ out = step prog s cont' in - match out with - | Cont cont'' -> search (gas - 1) prog cont'' - | _ -> Choice.return out) + let/ out = step prog s cont' in + match out with + | Cont cont'' -> search (gas - 1) prog cont'' + | _ -> Choice.return out ) let interpret (prog : program) : (Outcome.t * state) list = let state, cont = initial_state prog in diff --git a/lib/list_choice.ml b/lib/list_choice.ml index 95b07ac..0d2b048 100644 --- a/lib/list_choice.ml +++ b/lib/list_choice.ml @@ -10,10 +10,10 @@ module Make (Eval : Eval_intf.M) (Heap : Heap_intf.M with type vt = Eval.t) : let return x s = [ (x, s) ] let bind f k - (* f : 'a t *) - (* k : 'a -> 'b t *) - (* 'b t *) - s = + (* f : 'a t *) + (* k : 'a -> 'b t *) + (* 'b t *) + s = let lst = f s in (* ('a * state) list *) let lst' = List.map (fun (a, s') -> (k a) s' (* ('b * state) list *)) lst in @@ -33,10 +33,9 @@ module Make (Eval : Eval_intf.M) (Heap : Heap_intf.M with type vt = Eval.t) : | true, false -> [ (true, { s with pc = pc_v }) ] | false, true -> [ (false, { s with pc = pc_not_v }) ] | true, true -> - [ - (true, { (Sstate.dup s Heap.clone) with pc = pc_v }); - (false, { (Sstate.dup s Heap.clone) with pc = pc_not_v }); - ] + [ (true, { (Sstate.dup s Heap.clone) with pc = pc_v }) + ; (false, { (Sstate.dup s Heap.clone) with pc = pc_not_v }) + ] let lift (f : state -> ('a * state) list) : 'a t = f let run (s : state) (f : 'a t) : ('a * state) list = f s diff --git a/lib/model.ml b/lib/model.ml index 8f390c3..0d36a0d 100644 --- a/lib/model.ml +++ b/lib/model.ml @@ -5,30 +5,28 @@ let empty = Some [] let get_value (model : t) (var : string) : Value.t = match model with | None -> + Log.error + "InternalError: Model.value_of, tried to get the value of variable %s \ + with a None model" + var + | Some model -> ( + match List.assoc var model with + | exception Not_found -> Log.error - "InternalError: Model.value_of, tried to get the value of variable %s \ - with a None model" + "InternalError: Model.value_of, there is no variable with name %s in \ + this model" var - | Some model -> ( - match List.assoc var model with - | exception Not_found -> - Log.error - "InternalError: Model.value_of, there is no variable with name %s \ - in this model" - var - | v -> v) + | v -> v ) let pp ?(no_values = false) (fmt : Fmt.formatter) (model : t) : unit = let open Fmt in - let pp_binding fmt (x, v) = - fprintf fmt "%s : %a" x (Value.pp ~no_values) v - in + let pp_binding fmt (x, v) = fprintf fmt "%s : %a" x (Value.pp ~no_values) v in match model with | None -> pp_print_string fmt "No model" | Some [] -> pp_print_string fmt "Empty model" | Some m -> - let m = List.sort (fun (x1, _) (x2, _) -> String.compare x1 x2) m in - pp_lst ~pp_sep:pp_newline pp_binding fmt m + let m = List.sort (fun (x1, _) (x2, _) -> String.compare x1 x2) m in + pp_lst ~pp_sep:pp_newline pp_binding fmt m let to_string (model : t) : string = Fmt.asprintf "%a" (pp ~no_values:false) model diff --git a/lib/operations.ml b/lib/operations.ml index 9c17389..b321b20 100644 --- a/lib/operations.ml +++ b/lib/operations.ml @@ -1,18 +1,18 @@ let pick_head states = match states with | [] -> - failwith - "InternalError: Tried to pick a state to expand from an empty \ - collection of states" + failwith + "InternalError: Tried to pick a state to expand from an empty collection \ + of states" | h :: t -> (h, t) let pick_last states = let rec aux acc states = match states with | [] -> - failwith - "InternalError: Tried to pick a state to expand from an empty \ - collection of states" + failwith + "InternalError: Tried to pick a state to expand from an empty \ + collection of states" | [ h ] -> (h, List.rev acc) (*meh*) | h :: t -> aux (h :: acc) t in diff --git a/lib/outcome.ml b/lib/outcome.ml index 9a8b6ba..04ee17b 100644 --- a/lib/outcome.ml +++ b/lib/outcome.ml @@ -9,9 +9,8 @@ type t = let pp ?(no_values = false) fmt = function | Cont _ -> Fmt.pp_print_string fmt "Continue" | Error e -> - Fmt.fprintf fmt - "Assertion violated, counter example:@\n@[ %a@]" - (Model.pp ~no_values) e + Fmt.fprintf fmt "Assertion violated, counter example:@\n@[ %a@]" + (Model.pp ~no_values) e | AssumeF -> Fmt.pp_print_string fmt "Assumption evaluated to false" | Return e -> Fmt.fprintf fmt "Returned %s" e | EndGas -> Fmt.pp_print_string fmt "EndGas" diff --git a/lib/program.ml b/lib/program.ml index 4115524..30e86dd 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -19,7 +19,12 @@ type stmt = | Delete of string [@@deriving yojson] -type func = { id : string; args : string list; body : stmt } +type func = + { id : string + ; args : string list + ; body : stmt + } + type program = (string, func) Hashtbl.t (* Helper functions *) @@ -36,29 +41,35 @@ let rec pp_stmt (fmt : Fmt.t) (s : stmt) : unit = | Clear -> fprintf fmt "Clear@\n" | Assign (x, e) -> fprintf fmt "Assignment: %s = %a" x Term.pp e | Symbol_bool (s, v) -> - fprintf fmt "Boolean Symbol declaration: name=%s, value=§__%s" s v + fprintf fmt "Boolean Symbol declaration: name=%s, value=§__%s" s v | Symbol_int (s, v) -> - fprintf fmt "Integer Symbol declaration: name=%s, value=§__%s" s v + fprintf fmt "Integer Symbol declaration: name=%s, value=§__%s" s v | Symbol_int_c (s, v, e) -> - fprintf fmt "Integer Symbol declaration: name=%s, value=§__%s, cond=%a" s - v Term.pp e - | Sequence s -> fprintf fmt "Sequence:@\n %a" (pp_lst ~pp_sep:(fun fmt () -> fprintf fmt "@\n ") pp_stmt) s + fprintf fmt "Integer Symbol declaration: name=%s, value=§__%s, cond=%a" s v + Term.pp e + | Sequence s -> + fprintf fmt "Sequence:@\n %a" + (pp_lst ~pp_sep:(fun fmt () -> fprintf fmt "@\n ") pp_stmt) + s | Return e -> fprintf fmt "Return: %a" Term.pp e | Assert e -> fprintf fmt "Assert: %a" Term.pp e | Assume e -> fprintf fmt "Assume: %a" Term.pp e - | Print exprs -> fprintf fmt "Print: %a" (pp_lst ~pp_sep:pp_comma Term.pp) exprs + | Print exprs -> + fprintf fmt "Print: %a" (pp_lst ~pp_sep:pp_comma Term.pp) exprs | IfElse (expr, s1, s2) -> - fprintf fmt "If (%a)@\n %a@\nElse@\n %a" Term.pp expr pp_stmt s1 pp_stmt s2 + fprintf fmt "If (%a)@\n %a@\nElse@\n %a" Term.pp expr pp_stmt s1 pp_stmt + s2 | FunCall (x, f, args) -> - fprintf fmt "Function Call: %s=%s(%a)" x f (pp_lst ~pp_sep:pp_comma Term.pp) args + fprintf fmt "Function Call: %s=%s(%a)" x f + (pp_lst ~pp_sep:pp_comma Term.pp) + args | While (expr, s) -> fprintf fmt "While (%a)@\n %a" Term.pp expr pp_stmt s | New (arr, sz) -> fprintf fmt "New array: %s has size %a" arr Term.pp sz | Update (arr, e1, e2) -> - fprintf fmt "Update: %s at loc %a is assigned %a" arr Term.pp e1 Term.pp - e2 + fprintf fmt "Update: %s at loc %a is assigned %a" arr Term.pp e1 Term.pp e2 | LookUp (x, arr, e) -> - fprintf fmt "LookUp: %s is assigned the value at loc %a from arr %s" x - Term.pp e arr + fprintf fmt "LookUp: %s is assigned the value at loc %a from arr %s" x + Term.pp e arr | Delete arr -> fprintf fmt "Delete: %s" arr let string_of_stmt (s : stmt) : string = Fmt.asprintf "%a" pp_stmt s @@ -66,7 +77,8 @@ let string_of_stmt (s : stmt) : string = Fmt.asprintf "%a" pp_stmt s let pp_func (fmt : Fmt.t) (f : func) : unit = let open Fmt in fprintf fmt " Function id: %s@\nArguments : (%a)@\nBody : %a@\n" f.id - (pp_lst ~pp_sep:pp_comma pp_str) f.args pp_stmt f.body + (pp_lst ~pp_sep:pp_comma pp_str) + f.args pp_stmt f.body let string_of_function (f : func) : string = Fmt.asprintf "%a" pp_func f let print_statement (s : stmt) : unit = s |> string_of_stmt |> print_endline diff --git a/lib/return.ml b/lib/return.ml index 9c20710..9bb1298 100644 --- a/lib/return.ml +++ b/lib/return.ml @@ -1,17 +1,20 @@ type ('v, 'h) t = ('v, 'h) State.t * Outcome.t let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (fmt : Fmt.t) (ret : ('v, 'h) t) : unit = + (fmt : Fmt.t) (ret : ('v, 'h) t) : unit = let open Fmt in let (_, _, st, _, pc, h), out = ret in fprintf fmt - "#RETURN:@\n -Outcome : %a@\n -Store : %a@\n -Path cond.: %a@\n \ - -Heap : %a@\n" + "#RETURN:@\n\ + \ -Outcome : %a@\n\ + \ -Store : %a@\n\ + \ -Path cond.: %a@\n\ + \ -Heap : %a@\n" (Outcome.pp ~no_values:false) out (Store.pp pp_val) st (Pc.pp pp_val) pc pp_heap h let string_of_return (pp_val : Fmt.t -> 'v -> unit) - (pp_heap : Fmt.t -> 'h -> unit) (ret : ('v, 'h) t) : string = + (pp_heap : Fmt.t -> 'h -> unit) (ret : ('v, 'h) t) : string = Fmt.asprintf "%a" (pp pp_val pp_heap) ret let get_outcome (ret : ('v, 'h) t) : Outcome.t = @@ -23,5 +26,5 @@ let get_pc (ret : ('v, 'h) t) : 'v Pc.t = State.get_pathcondition state let print (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (ret : ('v, 'h) t) : unit = + (ret : ('v, 'h) t) : unit = print_endline (string_of_return pp_val pp_heap ret) diff --git a/lib/sstate.ml b/lib/sstate.ml index 0e77d57..6dfedff 100644 --- a/lib/sstate.ml +++ b/lib/sstate.ml @@ -1,30 +1,33 @@ -type ('v, 'h) t = { - store : 'v Store.t; - cs : 'v Callstack.t; - pc : 'v Pc.t; - heap : 'h; -} +type ('v, 'h) t = + { store : 'v Store.t + ; cs : 'v Callstack.t + ; pc : 'v Pc.t + ; heap : 'h + } let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (fmt : Fmt.formatter) (state : ('v, 'h) t) : unit = + (fmt : Fmt.formatter) (state : ('v, 'h) t) : unit = Fmt.fprintf fmt - "{@\n-Store : %a@\n-Callstack : %a@\n-Path cond. : \ - %a@\n-Heap : %a@\n}" + "{@\n\ + -Store : %a@\n\ + -Callstack : %a@\n\ + -Path cond. : %a@\n\ + -Heap : %a@\n\ + }" (Store.pp pp_val) state.store (Callstack.pp pp_val) state.cs (Pc.pp pp_val) state.pc pp_heap state.heap let to_string (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (state : ('v, 'h) t) : string = + (state : ('v, 'h) t) : string = Fmt.asprintf "%a" (pp pp_val pp_heap) state let print (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (state : ('v, 'h) t) : unit = + (state : ('v, 'h) t) : unit = to_string pp_val pp_heap state |> print_endline let dup (state : ('v, 'h) t) heap_dup : ('v, 'h) t = - { - state with - store = Store.dup state.store; - cs = Callstack.dup state.cs; - heap = heap_dup state.heap; + { state with + store = Store.dup state.store + ; cs = Callstack.dup state.cs + ; heap = heap_dup state.heap } diff --git a/lib/state.ml b/lib/state.ml index 84b8330..861a075 100644 --- a/lib/state.ml +++ b/lib/state.ml @@ -22,26 +22,33 @@ let get_pathcondition (state : ('v, 'h) t) : 'v Pc.t = pc let push_statements (state : ('v, 'h) t) (to_add : Program.stmt list) : - ('v, 'h) t = + ('v, 'h) t = let stmt, stmts, st, cs, pc, heap = state in (stmt, to_add @ stmts, st, cs, pc, heap) let pp (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (fmt : Fmt.t) (state : ('v, 'h) t) : unit = + (fmt : Fmt.t) (state : ('v, 'h) t) : unit = let open Fmt in let s, cont, store, cs, pc, heap = state in fprintf fmt - ">STATE:@\n -Cur Statement : %a@\n -Continuation : %a@\n -Store : \ - %a@\n -Callstack : %a@\n -Path cond. : %a@\n -Heap : %a@\n" - Program.pp_stmt s (pp_lst ~pp_sep:(fun fmt () -> fprintf fmt "; ") Program.pp_stmt) cont (Store.pp pp_val) store - (Callstack.pp pp_val) cs (Pc.pp pp_val) pc pp_heap heap + ">STATE:@\n\ + \ -Cur Statement : %a@\n\ + \ -Continuation : %a@\n\ + \ -Store : %a@\n\ + \ -Callstack : %a@\n\ + \ -Path cond. : %a@\n\ + \ -Heap : %a@\n" + Program.pp_stmt s + (pp_lst ~pp_sep:(fun fmt () -> fprintf fmt "; ") Program.pp_stmt) + cont (Store.pp pp_val) store (Callstack.pp pp_val) cs (Pc.pp pp_val) pc + pp_heap heap let to_string (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (state : ('v, 'h) t) : string = + (state : ('v, 'h) t) : string = Fmt.asprintf "%a" (pp pp_val pp_heap) state let print (pp_val : Fmt.t -> 'v -> unit) (pp_heap : Fmt.t -> 'h -> unit) - (state : ('v, 'h) t) : unit = + (state : ('v, 'h) t) : unit = to_string pp_val pp_heap state |> print_endline let dup (state : ('v, 'h) t) heap_dup : ('v, 'h) t = diff --git a/lib/term.ml b/lib/term.ml index f5ddc40..d206e5c 100644 --- a/lib/term.ml +++ b/lib/term.ml @@ -1,4 +1,9 @@ -type unop = Neg | Not | Abs | StringOfInt [@@deriving yojson] +type unop = + | Neg + | Not + | Abs + | StringOfInt +[@@deriving yojson] type binop = | Plus @@ -44,9 +49,9 @@ let get_value_from_expr (e : t) : Value.t = match e with | Val v -> v | _ -> - failwith - "InternalError: Expression.get_value_from_expr, tried to retrieve a \ - value from a non value constructor" + failwith + "InternalError: Expression.get_value_from_expr, tried to retrieve a \ + value from a non value constructor" let rec flatten (e : t) : t list = match e with diff --git a/lib/translator.ml b/lib/translator.ml index 448520e..146ed00 100644 --- a/lib/translator.ml +++ b/lib/translator.ml @@ -28,7 +28,7 @@ let translate_uop (op : unop) (v : Z3.Expr.expr) : Z3.Expr.expr = | StringOfInt -> assert false let translate_binop (op : binop) (v1 : Z3.Expr.expr) (v2 : Z3.Expr.expr) : - Z3.Expr.expr = + Z3.Expr.expr = match op with | Plus -> Z3.Arithmetic.mk_add ctx [ v1; v2 ] | Minus -> Z3.Arithmetic.mk_sub ctx [ v1; v2 ] @@ -45,30 +45,30 @@ let translate_binop (op : binop) (v1 : Z3.Expr.expr) (v2 : Z3.Expr.expr) : | And -> Z3.Boolean.mk_and ctx [ v1; v2 ] | Xor -> Z3.Boolean.mk_xor ctx v1 v2 | _ -> - Fmt.kasprintf failwith - "TODO: Encoding.encode_binop, missing implementation of %a" - Term.pp_binop op + Fmt.kasprintf failwith + "TODO: Encoding.encode_binop, missing implementation of %a" Term.pp_binop + op let rec translate (e : Term.t) : Z3.Expr.expr = match e with | Val v -> translate_value v | Var v -> - failwith - ("InternalError: Encoding.encode_expr, tried to encode variable " ^ v) + failwith + ("InternalError: Encoding.encode_expr, tried to encode variable " ^ v) | Unop (op, e) -> - let e' = translate e in - translate_uop op e' + let e' = translate e in + translate_uop op e' | Binop (op, e1, e2) -> - let e1' = translate e1 in - let e2' = translate e2 in - translate_binop op e1' e2' + let e1' = translate e1 in + let e2' = translate e2 in + translate_binop op e1' e2' | B_symb s -> Z3.Boolean.mk_const_s ctx s | I_symb s -> Z3.Arithmetic.Integer.mk_const_s ctx s | Ite (e1, e2, e3) -> - let e1' = translate e1 in - let e2' = translate e2 in - let e3' = translate e3 in - Z3.Boolean.mk_ite ctx e1' e2' e3' + let e1' = translate e1 in + let e2' = translate e2 in + let e3' = translate e3 in + Z3.Boolean.mk_ite ctx e1' e2' e3' let is_sat (exprs : Term.t list) : bool = let exprs' = List.map translate exprs in @@ -80,26 +80,24 @@ let is_sat (exprs : Term.t list) : bool = | Z3.Solver.UNKNOWN -> assert false let get_interp (model : Z3.Model.model) (const : Z3.FuncDecl.func_decl) : - (string * Value.t) option = + (string * Value.t) option = let* interp = Z3.Model.get_const_interp model const in let* v = match Z3.Expr.get_sort interp |> Z3.Sort.get_sort_kind with | Z3enums.INT_SORT -> - let x = - int_of_string @@ Z3.Arithmetic.Integer.numeral_to_string interp - in - Some (Integer x) + let x = int_of_string @@ Z3.Arithmetic.Integer.numeral_to_string interp in + Some (Integer x) | Z3enums.BOOL_SORT -> ( - match Z3.Boolean.get_bool_value interp with - | Z3enums.L_TRUE -> Some (Boolean true) - | Z3enums.L_FALSE -> Some (Boolean false) - | Z3enums.L_UNDEF -> assert false) + match Z3.Boolean.get_bool_value interp with + | Z3enums.L_TRUE -> Some (Boolean true) + | Z3enums.L_FALSE -> Some (Boolean false) + | Z3enums.L_UNDEF -> assert false ) | _ -> None in Some (Z3.Symbol.to_string @@ Z3.FuncDecl.get_name const, v) let find_model ?(print_model = false) (es : Term.t list) : - (string * Value.t) list option = + (string * Value.t) list option = assert (is_sat es); let* model = Z3.Solver.get_model solver in if print_model then Fmt.printf "%s@." (Z3.Model.to_string model); diff --git a/lib/value.ml b/lib/value.ml index af8307c..568f852 100644 --- a/lib/value.ml +++ b/lib/value.ml @@ -1,13 +1,17 @@ -type t = Integer of int | Boolean of bool | Loc of int | Error +type t = + | Integer of int + | Boolean of bool + | Loc of int + | Error [@@deriving yojson] let pp ?(no_values = false) fmt (v : t) = let open Fmt in match v with | Integer n -> - if no_values then fprintf fmt "Int _" else fprintf fmt "Int %d" n + if no_values then fprintf fmt "Int _" else fprintf fmt "Int %d" n | Boolean b -> - if no_values then fprintf fmt "Bool _ " else fprintf fmt "Bool %b" b + if no_values then fprintf fmt "Bool _ " else fprintf fmt "Bool %b" b | Loc l -> if no_values then fprintf fmt "Loc _ " else fprintf fmt "Loc %d" l | Error -> pp_print_string fmt "Error"