From 438c245e5ae19e97e8ce16603b1821ec983078cc Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 18 Mar 2024 17:23:03 +0000 Subject: [PATCH 1/5] refactor: Term to Expr --- lib/eval_concolic.ml | 2 +- lib/eval_concrete.ml | 2 +- lib/eval_expression.ml | 6 ++--- lib/eval_intf.ml | 2 +- lib/eval_symbolic.ml | 50 ++++++++++++++++++++-------------------- lib/{term.ml => expr.ml} | 0 lib/heap/heap_tree.ml | 1 - lib/parser.mly | 48 +++++++++++++++++++------------------- lib/pc.ml | 4 ++-- lib/program.ml | 48 +++++++++++++++++++------------------- whilloc.opam | 2 +- 11 files changed, 82 insertions(+), 83 deletions(-) rename lib/{term.ml => expr.ml} (100%) diff --git a/lib/eval_concolic.ml b/lib/eval_concolic.ml index 06ebee5..b49c1e4 100644 --- a/lib/eval_concolic.ml +++ b/lib/eval_concolic.ml @@ -15,7 +15,7 @@ module M = struct let symbolic_store = Store.create_store key_symbols in (concrete_store, symbolic_store) - let eval (store : st) (e : Term.t) : t = + let eval (store : st) (e : Expr.t) : t = let cstore, sstore = project_store store in (Eval_concrete.eval cstore e, Eval_symbolic.eval sstore e) diff --git a/lib/eval_concrete.ml b/lib/eval_concrete.ml index 38c6e05..e008c44 100644 --- a/lib/eval_concrete.ml +++ b/lib/eval_concrete.ml @@ -4,7 +4,7 @@ module M = struct type t = Value.t type st = t Store.t - let rec eval (store : st) (e : Term.t) : t = + let rec eval (store : st) (e : Expr.t) : t = match e with | Val v -> v | Var x -> Store.get store x diff --git a/lib/eval_expression.ml b/lib/eval_expression.ml index 3528ba5..b7393a1 100644 --- a/lib/eval_expression.ml +++ b/lib/eval_expression.ml @@ -167,16 +167,16 @@ let shr ((v1, v2) : t * t) : t = "Exception in Oper.shr: this operation is only applicable to Integer \ arguments" -let eval_unop_expr (op : Term.unop) (v : t) : t = +let eval_unop_expr (op : Expr.unop) (v : t) : t = match op with | Neg -> neg v | Not -> not_ v | Abs -> abs v | StringOfInt -> stoi v -let eval_ite (_ : Term.t) (_ : Term.t) (_ : Term.t) : t = assert false +let eval_ite (_ : Expr.t) (_ : Expr.t) (_ : Expr.t) : t = assert false -let eval_binop_expr (op : Term.binop) (v1 : t) (v2 : t) : t = +let eval_binop_expr (op : Expr.binop) (v1 : t) (v2 : t) : t = let f = match op with | Plus -> plus diff --git a/lib/eval_intf.ml b/lib/eval_intf.ml index d9f2919..c31e5db 100644 --- a/lib/eval_intf.ml +++ b/lib/eval_intf.ml @@ -1,7 +1,7 @@ module type M = sig type t - val eval : t Store.t -> Term.t -> t + val eval : t Store.t -> Expr.t -> t val is_true : t list -> bool val test_assert : t list -> bool * Model.t val negate : t -> t diff --git a/lib/eval_symbolic.ml b/lib/eval_symbolic.ml index a0551d3..10cfe81 100644 --- a/lib/eval_symbolic.ml +++ b/lib/eval_symbolic.ml @@ -1,5 +1,5 @@ module M = struct - open Term + open Expr module E = Encoding.Expr module V = Encoding.Value module T = Encoding.Ty @@ -11,34 +11,34 @@ module M = struct let solver = Slv.Z3_batch.create () - let eval_unop (op : Term.unop) = + let eval_unop (op : Expr.unop) = match op with - | Term.Neg -> (Some T.Neg, None) - | Term.Not -> (Some T.Not, None) - | Term.Abs -> (Some T.Abs, None) - | Term.StringOfInt -> (None, Some T.String_from_int) + | Expr.Neg -> (Some T.Neg, None) + | Expr.Not -> (Some T.Not, None) + | Expr.Abs -> (Some T.Abs, None) + | Expr.StringOfInt -> (None, Some T.String_from_int) - let eval_binop (op : Term.binop) = + let eval_binop (op : Expr.binop) = match op with - | Term.Plus -> (Some T.Add, None) - | Term.Minus -> (Some T.Sub, None) - | Term.Times -> (Some T.Mul, None) - | Term.Div -> (Some T.Div, None) - | Term.Modulo -> (Some T.Rem, None) - | Term.Pow -> (Some T.Pow, None) - | Term.Or -> (Some T.Or, None) - | Term.And -> (Some T.And, None) - | Term.Xor -> (Some T.Xor, None) - | Term.ShiftL -> (Some T.Shl, None) - | Term.ShiftR -> (Some T.ShrA, None) - | Term.Gt -> (None, Some T.Gt) - | Term.Lt -> (None, Some T.Lt) - | Term.Gte -> (None, Some T.Ge) - | Term.Lte -> (None, Some T.Le) - | Term.Equals -> (None, Some T.Eq) - | Term.NEquals -> (None, Some T.Ne) + | Expr.Plus -> (Some T.Add, None) + | Expr.Minus -> (Some T.Sub, None) + | Expr.Times -> (Some T.Mul, None) + | Expr.Div -> (Some T.Div, None) + | Expr.Modulo -> (Some T.Rem, None) + | Expr.Pow -> (Some T.Pow, None) + | Expr.Or -> (Some T.Or, None) + | Expr.And -> (Some T.And, None) + | Expr.Xor -> (Some T.Xor, None) + | Expr.ShiftL -> (Some T.Shl, None) + | Expr.ShiftR -> (Some T.ShrA, None) + | Expr.Gt -> (None, Some T.Gt) + | Expr.Lt -> (None, Some T.Lt) + | Expr.Gte -> (None, Some T.Ge) + | Expr.Lte -> (None, Some T.Le) + | Expr.Equals -> (None, Some T.Eq) + | Expr.NEquals -> (None, Some T.Ne) - let rec eval (store : st) (e : Term.t) : t = + let rec eval (store : st) (e : Expr.t) : t = match e with | Val (Integer n) -> E.(make @@ Val (V.Int n)) | Val (Boolean true) -> E.(make @@ Val V.True) diff --git a/lib/term.ml b/lib/expr.ml similarity index 100% rename from lib/term.ml rename to lib/expr.ml diff --git a/lib/heap/heap_tree.ml b/lib/heap/heap_tree.ml index 9225ea1..cc1b70e 100644 --- a/lib/heap/heap_tree.ml +++ b/lib/heap/heap_tree.ml @@ -198,7 +198,6 @@ module M = struct [ (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 h', _ = heap in match Expr.view arr with | Val (Int l) -> ( diff --git a/lib/parser.mly b/lib/parser.mly index 404c1fa..8967b09 100644 --- a/lib/parser.mly +++ b/lib/parser.mly @@ -65,19 +65,19 @@ value: (* e ::= v | x | -e | e+e | f(e) | (e) *) expression: | v = value; - { Term.Val v } + { Expr.Val v } | v = VAR; - { Term.Var v } + { Expr.Var v } | MINUS; e = expression; - { Term.Unop (Term.Neg, e) } %prec unopt_prec + { Expr.Unop (Expr.Neg, e) } %prec unopt_prec | NOT; e = expression; - { Term.Unop (Term.Not, e) } %prec unopt_prec + { Expr.Unop (Expr.Not, e) } %prec unopt_prec | ABS; e = expression; - { Term.Unop (Term.Abs, e) } %prec unopt_prec + { Expr.Unop (Expr.Abs, e) } %prec unopt_prec | STOI; e = expression; - { Term.Unop (Term.StringOfInt, e) } %prec unopt_prec + { Expr.Unop (Expr.StringOfInt, e) } %prec unopt_prec | e1 = expression; bop = binop_target; e2 = expression; - { Term.Binop (bop, e1, e2) } + { Expr.Binop (bop, e1, e2) } | LPAREN; e=expression ; RPAREN { e } @@ -126,20 +126,20 @@ statement_sequence: %inline binop_target: - | PLUS { Term.Plus } - | MINUS { Term.Minus } - | TIMES { Term.Times } - | DIVIDE { Term.Div } - | MODULO { Term.Modulo } - | POW { Term.Pow } - | GT { Term.Gt } - | LT { Term.Lt } - | GTE { Term.Gte } - | LTE { Term.Lte } - | EQUAL { Term.Equals } - | NEQUAL { Term.NEquals } - | OR { Term.Or } - | AND { Term.And } - | XOR { Term.Xor } - | SHL { Term.ShiftL } - | SHR { Term.ShiftR } + | PLUS { Expr.Plus } + | MINUS { Expr.Minus } + | TIMES { Expr.Times } + | DIVIDE { Expr.Div } + | MODULO { Expr.Modulo } + | POW { Expr.Pow } + | GT { Expr.Gt } + | LT { Expr.Lt } + | GTE { Expr.Gte } + | LTE { Expr.Lte } + | EQUAL { Expr.Equals } + | NEQUAL { Expr.NEquals } + | OR { Expr.Or } + | AND { Expr.And } + | XOR { Expr.Xor } + | SHL { Expr.ShiftL } + | SHR { Expr.ShiftR } diff --git a/lib/pc.ml b/lib/pc.ml index 96e7a55..fbb6b39 100644 --- a/lib/pc.ml +++ b/lib/pc.ml @@ -5,8 +5,8 @@ let add_condition (pc : 'v list) (t : 'v) : 'v list = t :: pc let negate (pc : 'v list) : 'v = List.fold_right - (fun x y -> Term.make_boperation Or (Term.negate x) y) - pc Term.make_false + (fun x y -> Expr.make_boperation Or (Expr.negate x) y) + pc Expr.make_false let pp (pp_val : Fmt.t -> 'v -> unit) (fmt : Fmt.t) (pc : 'value list) : unit = (Fmt.pp_lst ~pp_sep:(fun fmt () -> Fmt.fprintf fmt " AND ") pp_val) fmt pc diff --git a/lib/program.ml b/lib/program.ml index 30e86dd..97d8e03 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -1,21 +1,21 @@ type stmt = | Skip - | Assign of string * Term.t + | Assign of string * Expr.t | Sequence of stmt list - | FunCall of string * string * Term.t list - | IfElse of Term.t * stmt * stmt - | While of Term.t * stmt - | Return of Term.t - | Assert of Term.t - | Assume of Term.t + | FunCall of string * string * Expr.t list + | IfElse of Expr.t * stmt * stmt + | While of Expr.t * stmt + | Return of Expr.t + | Assert of Expr.t + | Assume of Expr.t | Clear - | Print of Term.t list + | Print of Expr.t list | Symbol_bool of string * string | Symbol_int of string * string - | Symbol_int_c of string * string * Term.t - | New of string * Term.t - | Update of string * Term.t * Term.t - | LookUp of string * string * Term.t + | Symbol_int_c of string * string * Expr.t + | New of string * Expr.t + | Update of string * Expr.t * Expr.t + | LookUp of string * string * Expr.t | Delete of string [@@deriving yojson] @@ -39,37 +39,37 @@ let rec pp_stmt (fmt : Fmt.t) (s : stmt) : unit = match s with | Skip -> fprintf fmt "Skip" | Clear -> fprintf fmt "Clear@\n" - | Assign (x, e) -> fprintf fmt "Assignment: %s = %a" x Term.pp e + | Assign (x, e) -> fprintf fmt "Assignment: %s = %a" x Expr.pp e | Symbol_bool (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 | Symbol_int_c (s, v, e) -> fprintf fmt "Integer Symbol declaration: name=%s, value=§__%s, cond=%a" s v - Term.pp e + Expr.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 + | Return e -> fprintf fmt "Return: %a" Expr.pp e + | Assert e -> fprintf fmt "Assert: %a" Expr.pp e + | Assume e -> fprintf fmt "Assume: %a" Expr.pp e | Print exprs -> - fprintf fmt "Print: %a" (pp_lst ~pp_sep:pp_comma Term.pp) exprs + fprintf fmt "Print: %a" (pp_lst ~pp_sep:pp_comma Expr.pp) exprs | IfElse (expr, s1, s2) -> - fprintf fmt "If (%a)@\n %a@\nElse@\n %a" Term.pp expr pp_stmt s1 pp_stmt + fprintf fmt "If (%a)@\n %a@\nElse@\n %a" Expr.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) + (pp_lst ~pp_sep:pp_comma Expr.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 + | While (expr, s) -> fprintf fmt "While (%a)@\n %a" Expr.pp expr pp_stmt s + | New (arr, sz) -> fprintf fmt "New array: %s has size %a" arr Expr.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 Expr.pp e1 Expr.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 + Expr.pp e arr | Delete arr -> fprintf fmt "Delete: %s" arr let string_of_stmt (s : stmt) : string = Fmt.asprintf "%a" pp_stmt s diff --git a/whilloc.opam b/whilloc.opam index 97d1a5b..a89cbd9 100644 --- a/whilloc.opam +++ b/whilloc.opam @@ -17,7 +17,7 @@ depends: [ "bos" "cmdliner" "ppx_deriving_yojson" - "encoding" {>= "0.0.4"} + "encoding" {>= "dev"} "odoc" {with-doc} ] build: [ From bbc616eb5b305365a1ec9182b3d05e234693818a Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 18 Mar 2024 17:27:58 +0000 Subject: [PATCH 2/5] refactor: vt to value, bt to block --- lib/heap/heap_array_fork.ml | 28 ++++++++++++++-------------- lib/heap/heap_arrayite.ml | 28 ++++++++++++++-------------- lib/heap/heap_concolic.ml | 20 ++++++++++---------- lib/heap/heap_concrete.ml | 24 ++++++++++++------------ lib/heap/heap_intf.ml | 12 ++++++------ lib/heap/heap_oplist.ml | 22 +++++++++++----------- lib/heap/heap_symbolic.ml | 20 ++++++++++---------- lib/heap/heap_tree.ml | 32 ++++++++++++++++---------------- lib/interpreter.ml | 2 +- lib/list_choice.ml | 2 +- 10 files changed, 95 insertions(+), 95 deletions(-) diff --git a/lib/heap/heap_array_fork.ml b/lib/heap/heap_array_fork.ml index 7c0c2e4..0d33f53 100644 --- a/lib/heap/heap_array_fork.ml +++ b/lib/heap/heap_array_fork.ml @@ -1,17 +1,17 @@ open Encoding module M = struct - type vt = Encoding.Expr.t - type bt = vt array + type value = Encoding.Expr.t + type block = value array type t = - { map : (int, bt) Hashtbl.t + { map : (int, block) Hashtbl.t ; i : int } let init () : t = { map = Hashtbl.create Parameters.size; i = 0 } - let pp_block fmt (block : bt) = + let pp_block fmt (block : block) = Fmt.fprintf fmt "%a" (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Expr.pp) (Array.to_list block) @@ -23,14 +23,14 @@ module M = 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 : value) (pc : value Pc.t) : bool = let e1 = Expr.(relop Ty.Ty_int Ty.Lt index (make @@ Val (Int 0))) in let e2 = Expr.(relop Ty.Ty_int Ty.Ge index (make @@ Val (Int sz))) in let e3 = Expr.(binop Ty.Ty_bool Ty.Or e1 e2) in not (Eval_symbolic.is_true (e3 :: pc)) - let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = + let in_bounds (heap : t) (arr : value) (i : value) (pc : value Pc.t) : bool = match Expr.view arr with | Val (Int l) -> ( match Hashtbl.find_opt heap.map l with @@ -44,7 +44,7 @@ module M = struct let copy (heap : t) : t = { heap with map = Hashtbl.copy heap.map } - let find_block (heap : t) (loc : vt) : int * bt = + let find_block (heap : t) (loc : value) : int * block = match Expr.view loc with | Val (Int loc') -> ( let block = Hashtbl.find_opt heap.map loc' in @@ -53,7 +53,7 @@ module M = 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 : value) (path : value Pc.t) : (t * value * value Pc.t) list = match Expr.view size with | Val (Int size') -> let block = Array.make size' Expr.(make @@ Val (Int 0)) in @@ -61,8 +61,8 @@ module M = struct [ ({ heap with i = heap.i + 1 }, Expr.(make @@ Val (Int 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 : value) (index : value) (path : value Pc.t) : + (t * value * value Pc.t) list = let _, block = find_block heap loc in match Expr.view index with | Val (Int index') -> @@ -89,8 +89,8 @@ module M = 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 : value) (index : value) (v : value) (path : value Pc.t) : + (t * value Pc.t) list = let loc, block = find_block heap loc in match Expr.view index with | Val (Int index') -> @@ -122,7 +122,7 @@ module M = 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 : value) (path : value Pc.t) : (t * value Pc.t) list = let loc', _ = find_block heap loc in let _ = Hashtbl.remove heap.map loc' in [ (heap, path) ] @@ -130,5 +130,5 @@ module M = struct let clone h = copy h end -module M' : Heap_intf.M with type vt = Encoding.Expr.t = M +module M' : Heap_intf.M with type value = Encoding.Expr.t = M include M diff --git a/lib/heap/heap_arrayite.ml b/lib/heap/heap_arrayite.ml index e827390..96c8fb2 100644 --- a/lib/heap/heap_arrayite.ml +++ b/lib/heap/heap_arrayite.ml @@ -1,13 +1,13 @@ open Encoding module M = struct - type vt = Encoding.Expr.t - type bt = vt array - type t = (int, bt) Hashtbl.t * int + type value = Encoding.Expr.t + type block = value array + type t = (int, block) Hashtbl.t * int let init () : t = (Hashtbl.create Parameters.size, 0) - let pp_block fmt (block : bt) = + let pp_block fmt (block : block) = Fmt.fprintf fmt "%a" (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Expr.pp) (Array.to_list block) @@ -19,14 +19,14 @@ module M = struct let to_string (heap : t) : string = Fmt.asprintf "%a" pp heap - let is_within (sz : int) (index : vt) (pc : vt Pc.t) : bool = + let is_within (sz : int) (index : value) (pc : value Pc.t) : bool = let e1 = Expr.(relop Ty.Ty_int Ty.Lt index (make @@ Val (Int 0))) in let e2 = Expr.(relop Ty.Ty_int Ty.Ge index (make @@ Val (Int sz))) in let e3 = Expr.(binop Ty.Ty_bool Ty.Or e1 e2) in not (Eval_symbolic.is_true (e3 :: pc)) - let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = + let in_bounds (heap : t) (arr : value) (i : value) (pc : value Pc.t) : bool = let h, _ = heap in match Expr.view arr with | Val (Int l) -> ( @@ -41,7 +41,7 @@ module M = struct let copy ((heap, i) : t) : t = (Hashtbl.copy heap, i) - let find_block (heap : t) (loc : vt) : int * bt = + let find_block (heap : t) (loc : value) : int * block = let heap', _ = heap in match Expr.view loc with | Val (Int loc') -> ( @@ -51,7 +51,7 @@ module M = 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 : value) (pc : value Pc.t) : (t * value * value Pc.t) list = let tbl, next = h in match Expr.view sz with | Val (Int i) -> @@ -60,8 +60,8 @@ module M = 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 : value) (index : value) (v : value) (path : value Pc.t) : + (t * value Pc.t) list = let heap', curr = heap in let loc, block = find_block heap loc in match Expr.view index with @@ -85,8 +85,8 @@ module M = 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 : value) (index : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let tbl, _ = h in match Expr.view index with | Val (Int i) -> ( @@ -139,7 +139,7 @@ module M = 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 : value) (pc : value Pc.t) : (t * value Pc.t) list = let tbl, _ = h in match Expr.view arr with | Val (Int l) -> ( @@ -153,5 +153,5 @@ module M = struct let clone h = copy h end -module M' : Heap_intf.M with type vt = Encoding.Expr.t = M +module M' : Heap_intf.M with type value = Encoding.Expr.t = M include M diff --git a/lib/heap/heap_concolic.ml b/lib/heap/heap_concolic.ml index a4dcc26..d3335f1 100644 --- a/lib/heap/heap_concolic.ml +++ b/lib/heap/heap_concolic.ml @@ -1,29 +1,29 @@ module M = struct - type vt = Value.t * Encoding.Expr.t (* indexes and sizes are always values *) - type t = (int, vt array) Hashtbl.t + type value = Value.t * Encoding.Expr.t (* indexes and sizes are always values *) + type t = (int, value array) Hashtbl.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 malloc _h (_sz : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = [] + let malloc _h (_sz : value) (_pc : value Pc.t) : (t * value * value 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 : value) (_index : value) (_v : value) (_pc : value Pc.t) : + (t * value Pc.t) list = [] - let lookup _h (_arr : vt) (_index : vt) (_pc : vt Pc.t) : - (t * vt * vt Pc.t) list = + let lookup _h (_arr : value) (_index : value) (_pc : value Pc.t) : + (t * value * value Pc.t) list = [] - let free _h (_arr : vt) (_pc : vt Pc.t) : (t * vt Pc.t) list = [] + let free _h (_arr : value) (_pc : value Pc.t) : (t * value Pc.t) list = [] - let in_bounds (_heap : t) (_v : vt) (_i : vt) (_pc : vt Pc.t) : bool = + let in_bounds (_heap : t) (_v : value) (_i : value) (_pc : value Pc.t) : bool = failwith "not implemented" let clone _ = assert false end -module M' : Heap_intf.M with type vt = Value.t * Encoding.Expr.t = M +module M' : Heap_intf.M with type value = Value.t * Encoding.Expr.t = M include M (* type t = (int, int arry) Hashtbl.t diff --git a/lib/heap/heap_concrete.ml b/lib/heap/heap_concrete.ml index cf60073..32e925c 100644 --- a/lib/heap/heap_concrete.ml +++ b/lib/heap/heap_concrete.ml @@ -1,13 +1,13 @@ open Value module M = struct - type bt = Value.t array - type t = (int, bt) Hashtbl.t * int - type vt = Value.t (* indexes and sizes are always values *) + type block = Value.t array + type t = (int, block) Hashtbl.t * int + type value = Value.t (* indexes and sizes are always values *) let init () : t = (Hashtbl.create Parameters.size, 0) - let pp_block fmt (block : bt) = + let pp_block fmt (block : block) = Fmt.fprintf fmt "%a" (Fmt.pp_lst ~pp_sep:Fmt.pp_comma Value.pp) (Array.to_list block) @@ -19,7 +19,7 @@ module M = struct 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 malloc (h : t) (sz : value) (pc : value Pc.t) : (t * value * value Pc.t) list = let tbl, next = h in match sz with | Integer i -> @@ -28,8 +28,8 @@ module M = 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 : value) (index : value) (v : value) (pc : value Pc.t) : + (t * value Pc.t) list = let tbl, _ = h in match (arr, index) with | Loc l, Integer i -> ( @@ -43,8 +43,8 @@ module M = 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 : value) (index : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let tbl, _ = h in match (arr, index) with | Loc l, Integer i -> ( @@ -59,7 +59,7 @@ module M = 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 : value) (pc : value Pc.t) : (t * value Pc.t) list = let tbl, _ = h in match arr with | Loc l -> ( @@ -70,7 +70,7 @@ module M = 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 : value) (i : value) (_pc : value Pc.t) : bool = match addr with | Loc l -> ( let tbl, _ = heap in @@ -86,7 +86,7 @@ module M = struct let clone _ = assert false end -module M' : Heap_intf.M with type vt = Value.t = M +module M' : Heap_intf.M with type value = Value.t = M include M (* diff --git a/lib/heap/heap_intf.ml b/lib/heap/heap_intf.ml index 62cf1bf..73e280b 100644 --- a/lib/heap/heap_intf.ml +++ b/lib/heap/heap_intf.ml @@ -1,14 +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 *) + type value (* 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 malloc : t -> value -> value Pc.t -> (t * value * value Pc.t) list + val lookup : t -> value -> value -> value Pc.t -> (t * value * value Pc.t) list + val update : t -> value -> value -> value -> value Pc.t -> (t * value Pc.t) list + val free : t -> value -> value Pc.t -> (t * value Pc.t) list + val in_bounds : t -> value -> value -> value Pc.t -> bool val clone : t -> t end diff --git a/lib/heap/heap_oplist.ml b/lib/heap/heap_oplist.ml index 47848e7..18ac5f1 100644 --- a/lib/heap/heap_oplist.ml +++ b/lib/heap/heap_oplist.ml @@ -1,10 +1,10 @@ open Encoding module M = struct - type vt = Encoding.Expr.t + type value = Encoding.Expr.t type addr = int - type size = vt - type op = vt * vt * vt Pc.t + type size = value + type op = value * value * value Pc.t type t = { map : (addr, size * op list) Hashtbl.t @@ -28,14 +28,14 @@ module M = 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 : value) (index : value) (pc : value Pc.t) : bool = let e1 = Expr.(relop Ty.Ty_int Ty.Lt index (make @@ Val (Int 0))) in let e2 = Expr.(relop Ty.Ty_int Ty.Ge index sz) in let e3 = Expr.(binop Ty.Ty_bool Ty.Or e1 e2) in not (Eval_symbolic.is_true (e3 :: pc)) - let in_bounds (heap : t) (v : vt) (i : vt) (pc : vt Pc.t) : bool = + let in_bounds (heap : t) (v : value) (i : value) (pc : value Pc.t) : bool = match Expr.view v with | Val (Int l) -> ( match Hashtbl.find_opt heap.map l with @@ -51,14 +51,14 @@ module M = struct 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 : value) (pc : value Pc.t) : (t * value * value Pc.t) list = let next = h.next in Hashtbl.add h.map next (sz, []); h.next <- h.next + 1; [ (h, Expr.(make @@ Val (Int 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 : value) (index : value) (v : value) (pc : value Pc.t) : + (t * value Pc.t) list = let lbl = match Expr.view arr with Val (Int i) -> i | _ -> assert false in let arr' = Hashtbl.find_opt h.map lbl in let f ((sz, oplist) : size * op list) : unit = @@ -67,7 +67,7 @@ module M = 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 : value) (index : value) (pc : value Pc.t) : (t * value * value Pc.t) list = let lbl = match Expr.view arr with Val (Int i) -> i | _ -> assert false in let arr' = Hashtbl.find h.map lbl in @@ -81,7 +81,7 @@ module M = struct in [ (h, v, pc) ] - let free h (arr : vt) (pc : vt Pc.t) : (t * vt Pc.t) list = + let free h (arr : value) (pc : value Pc.t) : (t * value Pc.t) list = let lbl = match Expr.view arr with Val (Int i) -> i | _ -> assert false in Hashtbl.remove h.map lbl; [ (h, pc) ] @@ -90,5 +90,5 @@ module M = struct let clone h = copy h end -module M' : Heap_intf.M with type vt = Encoding.Expr.t = M +module M' : Heap_intf.M with type value = Encoding.Expr.t = M include M diff --git a/lib/heap/heap_symbolic.ml b/lib/heap/heap_symbolic.ml index 8806708..e36dadb 100644 --- a/lib/heap/heap_symbolic.ml +++ b/lib/heap/heap_symbolic.ml @@ -1,31 +1,31 @@ module M = struct - type vt = Encoding.Expr.t - type t = (int, vt array) Hashtbl.t + type value = Encoding.Expr.t + type t = (int, value array) Hashtbl.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 malloc _h (_sz : vt) (_pc : vt Pc.t) : (t * vt * vt Pc.t) list = + let malloc _h (_sz : value) (_pc : value Pc.t) : (t * value * value 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 : value) (_index : value) (_v : value) (_pc : value Pc.t) : + (t * value 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 : value) (_index : value) (_pc : value Pc.t) : + (t * value * value 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 : value) (_pc : value Pc.t) : (t * value 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 : value) (_i : value) (_pc : value Pc.t) : bool = assert false let clone _ = assert false end -module M' : Heap_intf.M with type vt = Encoding.Expr.t = M +module M' : Heap_intf.M with type value = Encoding.Expr.t = M include M (* type t = (int, int arry) Hashtbl.t diff --git a/lib/heap/heap_tree.ml b/lib/heap/heap_tree.ml index cc1b70e..62fd9a3 100644 --- a/lib/heap/heap_tree.ml +++ b/lib/heap/heap_tree.ml @@ -1,11 +1,11 @@ open Encoding module M = struct - type vt = Encoding.Expr.t - type range = vt * vt + type value = Encoding.Expr.t + type range = value * value type tree_t = - | Leaf of range * vt + | Leaf of range * value | Node of range * tree_t list type t = (int, tree_t) Hashtbl.t * int @@ -41,7 +41,7 @@ module M = 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 : value) (pc : value Pc.t) : (t * value * value Pc.t) list = let h', curr = h in let tree = Leaf (Expr.(make @@ Val (Int 0), sz), Expr.(make @@ Val (Int 0))) @@ -49,11 +49,11 @@ module M = struct Hashtbl.replace h' curr tree; [ ((h', curr + 1), Expr.(make @@ Val (Int curr)), pc) ] - let update h (arr : vt) (index : vt) (v : vt) (pc : vt Pc.t) : - (t * vt Pc.t) list = + let update h (arr : value) (index : value) (v : value) (pc : value Pc.t) : + (t * value 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 : value) (v : value) (pc : value Pc.t) : + (tree_t * value Pc.t) list option = match tree with | Leaf ((left, right), old_v) -> let ge_left = Expr.(relop Ty.Ty_int Ty.Ge index left) in @@ -134,7 +134,7 @@ module M = 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 : value) (pc : value Pc.t) : bool = let lower, upper = r in let e1 = Expr.(relop Ty.Ty_int Ty.Lt index lower) in let e2 = Expr.(relop Ty.Ty_int Ty.Ge index upper) in @@ -142,15 +142,15 @@ module M = struct not (Eval_symbolic.is_true (e3 :: pc)) - let may_within_range (r : range) (index : vt) (pc : vt Pc.t) : bool = + let may_within_range (r : range) (index : value) (pc : value Pc.t) : bool = let lower, upper = r in let e1 = Expr.(relop Ty.Ty_int Ty.Ge index lower) in let e2 = Expr.(relop Ty.Ty_int Ty.Lt index upper) in Eval_symbolic.is_true ([ e1; e2 ] @ pc) - let rec search_tree (index : vt) (pc : vt Pc.t) (tree : tree_t) : - (vt * vt) list = + let rec search_tree (index : value) (pc : value Pc.t) (tree : tree_t) : + (value * value) list = match tree with | Leaf (r, v) -> let lower, upper = r in @@ -168,7 +168,7 @@ module M = 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 : value) (index : value) (pc : value Pc.t) : (t * value * value Pc.t) list = let tbl, _ = h in @@ -188,7 +188,7 @@ module M = struct "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 free h (arr : value) (pc : value Pc.t) : (t * value Pc.t) list = let h', _ = h in (* let ign = to_string h in ignore ign; *) @@ -197,7 +197,7 @@ module M = struct | _ -> failwith "Invalid allocation index" ); [ (h, pc) ] - let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = + let in_bounds (heap : t) (arr : value) (i : value) (pc : value Pc.t) : bool = let h', _ = heap in match Expr.view arr with | Val (Int l) -> ( @@ -214,5 +214,5 @@ module M = struct let clone h = copy h end -module M' : Heap_intf.M with type vt = Encoding.Expr.t = M +module M' : Heap_intf.M with type value = Encoding.Expr.t = M include M diff --git a/lib/interpreter.ml b/lib/interpreter.ml index 629e726..4fc2f5d 100644 --- a/lib/interpreter.ml +++ b/lib/interpreter.ml @@ -1,7 +1,7 @@ module Make (Eval : Eval_intf.M) (Search : Search_intf.M) - (Heap : Heap_intf.M with type vt = Eval.t) + (Heap : Heap_intf.M with type value = Eval.t) (Choice : Choice_intf.Choice with type v = Eval.t and type h = Heap.t) : Interpreter_intf.S with type t = Eval.t and type h = Heap.t = struct open Program diff --git a/lib/list_choice.ml b/lib/list_choice.ml index 0d2b048..50b796f 100644 --- a/lib/list_choice.ml +++ b/lib/list_choice.ml @@ -1,6 +1,6 @@ open Sstate -module Make (Eval : Eval_intf.M) (Heap : Heap_intf.M with type vt = Eval.t) : +module Make (Eval : Eval_intf.M) (Heap : Heap_intf.M with type value = 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 v = Eval.t From 2cdfd0e7339924d0a2bb850b5f2456dbe263b0ab Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 18 Mar 2024 18:56:22 +0000 Subject: [PATCH 3/5] add hierarchy heap using write lists --- bin/commands/cmd_execute.ml | 22 +- bin/utils/options.ml | 1 + lib/eval_symbolic.ml | 11 +- lib/heap/heap_array_fork.ml | 106 +- lib/heap/heap_arrayite.ml | 54 +- lib/heap/heap_concolic.ml | 23 +- lib/heap/heap_concrete.ml | 14 +- lib/heap/heap_hierarchy.ml | 94 ++ lib/heap/heap_intf.ml | 14 +- lib/heap/heap_oplist.ml | 49 +- lib/heap/heap_symbolic.ml | 20 +- lib/heap/heap_tree.ml | 43 +- test/test_sh.t | 1842 +++++++++++++++++++++++++++++++++++ 13 files changed, 2167 insertions(+), 126 deletions(-) create mode 100644 lib/heap/heap_hierarchy.ml create mode 100644 test/test_sh.t diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml index faec481..cf62901 100644 --- a/bin/commands/cmd_execute.ml +++ b/bin/commands/cmd_execute.ml @@ -1,15 +1,20 @@ open Whilloc open Utils +(* Heap *) + +module HeapHierarchy = Heap_hierarchy.M (Heap_oplist) + (* Choice *) -module C_Choice = List_choice.Make (Eval_concrete) (Heap_concrete.M) +module C_Choice = List_choice.Make (Eval_concrete) (Heap_concrete) module SAF_Choice = List_choice.Make (Eval_symbolic) (Heap_array_fork) module SAITE_Choice = List_choice.Make (Eval_symbolic) (Heap_arrayite) module ST_Choice = List_choice.Make (Eval_symbolic) (Heap_tree) module SOPL_Choice = List_choice.Make (Eval_symbolic) (Heap_oplist) +module SH_Choice = List_choice.Make (Eval_symbolic.M) (HeapHierarchy) (* Interpreter *) -module C = Interpreter.Make (Eval_concrete) (Dfs) (Heap_concrete.M) (C_Choice) +module C = Interpreter.Make (Eval_concrete) (Dfs) (Heap_concrete) (C_Choice) module SAF = Interpreter.Make (Eval_symbolic) (Dfs) (Heap_array_fork) (SAF_Choice) @@ -20,12 +25,16 @@ module SAITE = module ST = Interpreter.Make (Eval_symbolic) (Dfs) (Heap_tree) (ST_Choice) module SOPL = Interpreter.Make (Eval_symbolic) (Dfs) (Heap_oplist) (SOPL_Choice) +module SH = + Interpreter.Make (Eval_symbolic.M) (Dfs.M) (HeapHierarchy) (SH_Choice) + type mode = | Concrete | Saf | Saite | St | Sopl + | Sh [@@deriving yojson] type report = @@ -52,6 +61,7 @@ let mode_to_string = function | Saite -> "saite" | St -> "st" | Sopl -> "sopl" + | Sh -> "sh" let write_report report = let json = report |> report_to_yojson |> Yojson.Safe.to_string in @@ -118,6 +128,14 @@ let run ?(no_values = false) ?(test = false) input mode = | _ -> None ) rets , List.length rets ) + |Sh -> + let rets = SH.interpret program in + ( List.filter_map + (fun (out, _) -> + if test then Format.printf "%a@." (Outcome.pp ~no_values) out; + match out with + | Outcome.Error _ | Outcome.EndGas -> Some out + | _ -> None ) rets, List.length rets) in let execution_time = Sys.time () -. start in diff --git a/bin/utils/options.ml b/bin/utils/options.ml index ee4150b..baf0cdc 100644 --- a/bin/utils/options.ml +++ b/bin/utils/options.ml @@ -36,6 +36,7 @@ let mode_conv = ; ("saite", Cmd_execute.Saite) ; ("st", Cmd_execute.St) ; ("sopl", Cmd_execute.Sopl) + ; ("sh", Cmd_execute.Sh) ] let mode = diff --git a/lib/eval_symbolic.ml b/lib/eval_symbolic.ml index 10cfe81..6dcbf21 100644 --- a/lib/eval_symbolic.ml +++ b/lib/eval_symbolic.ml @@ -50,7 +50,7 @@ module M = struct let e' = eval store e in match op' with | Some T.Not, None -> E.(unop T.Ty_bool T.Not e') - | Some u, None -> E.(unop T.Ty_int u e') + | Some u, None -> E.(unop T.Ty_int u e') | None, Some c -> E.(cvtop T.Ty_int c e') | _ -> assert false ) | Binop (op, e1, e2) -> ( @@ -85,11 +85,10 @@ module M = struct "InternalError: EvalSymbolic.val_translator, value from Encoding not \ implemented" - let hashtbl_to_list (tbl : (S.t, V.t) Hashtbl.t) : - (string * Value.t) list = - (Hashtbl.fold - (fun k v acc -> (S.to_string k, translate_value v) :: acc) - tbl [] ) + let hashtbl_to_list (tbl : (S.t, V.t) Hashtbl.t) : (string * Value.t) list = + Hashtbl.fold + (fun k v acc -> (S.to_string k, translate_value v) :: acc) + tbl [] let test_assert (exprs : t list) : bool * Model.t = assert (is_true exprs); diff --git a/lib/heap/heap_array_fork.ml b/lib/heap/heap_array_fork.ml index 0d33f53..3ce3e8c 100644 --- a/lib/heap/heap_array_fork.ml +++ b/lib/heap/heap_array_fork.ml @@ -9,7 +9,9 @@ module M = struct ; i : int } - let init () : t = { map = Hashtbl.create Parameters.size; i = 0 } + exception BlockNotInHeap + + let init ?(next = 0) () : t = { map = Hashtbl.create Parameters.size; i = next } let pp_block fmt (block : block) = Fmt.fprintf fmt "%a" @@ -35,10 +37,7 @@ module M = struct | Val (Int 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" ) + | _ -> raise BlockNotInHeap ) | _ -> failwith "InternalError: HeapArrayFork.in_bounds, arr must be location" @@ -53,7 +52,8 @@ module M = struct | None -> failwith "Block does not exist" ) | _ -> failwith "Location needs to be a concrete value" - let malloc (heap : t) (size : value) (path : value Pc.t) : (t * value * value Pc.t) list = + let malloc (heap : t) (size : value) (path : value Pc.t) : + (t * value * value Pc.t) list = match Expr.view size with | Val (Int size') -> let block = Array.make size' Expr.(make @@ Val (Int 0)) in @@ -68,29 +68,29 @@ module M = struct | Val (Int index') -> let ret = Array.get block index' in [ (heap, ret, path) ] - | Symbol s when Symbol.type_of s = Ty_int -> - let blockList = Array.to_list block in - let temp = - List.mapi - (fun index' expr -> - let cond = - Expr.(relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int index'))) - in - (copy heap, expr, Pc.add_condition path cond) ) - blockList - in - List.filteri - (fun index' _ -> - (* can be optimized *) - let e = - Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index'))) + | Symbol s when Symbol.type_of s = Ty_int -> + let blockList = Array.to_list block in + let temp = + List.mapi + (fun index' expr -> + let cond = + Expr.(relop Ty.Ty_bool Ty.Eq index (make @@ Val (Int index'))) in - Eval_symbolic.is_true (e :: path) ) - temp + (copy heap, expr, Pc.add_condition path cond) ) + blockList + in + List.filteri + (fun index' _ -> + (* can be optimized *) + let e = + Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index'))) + in + Eval_symbolic.is_true (e :: path) ) + temp | _ -> failwith "Invalid index" - let update (heap : t) (loc : value) (index : value) (v : value) (path : value Pc.t) : - (t * value Pc.t) list = + let update (heap : t) (loc : value) (index : value) (v : value) + (path : value Pc.t) : (t * value Pc.t) list = let loc, block = find_block heap loc in match Expr.view index with | Val (Int index') -> @@ -98,35 +98,47 @@ module M = struct let _ = Hashtbl.replace heap.map loc block in [ (heap, path) ] | Symbol s when Symbol.type_of s = Ty_int -> - 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 = - Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int 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 = + 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 = Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index'))) in - Eval_symbolic.is_true (e :: path) ) - temp + ({ heap with map = newHeap }, Pc.add_condition path cond) ) + blockList + in + List.filteri + (fun index' _ -> + (* can be optimized *) + let e = + Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int index'))) + in + Eval_symbolic.is_true (e :: path) ) + temp | _ -> failwith "Invalid index" - let free (heap : t) (loc : value) (path : value Pc.t) : (t * value Pc.t) list = + let free (heap : t) (loc : value) (path : value Pc.t) : (t * value Pc.t) list + = let loc', _ = find_block heap loc in - let _ = Hashtbl.remove heap.map loc' in + let _ = Hashtbl.replace heap.map loc' (Array.make 0 Expr.(make @@ Val (Int 0))) in [ (heap, path) ] + let get_block (h : t) (addr : value) : block option = + let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + match Hashtbl.find_opt h.map addr' with + | Some block -> if Array.length block = 0 then None else Some block + | None -> None + + let set_block (h : t) (addr : value) (block : block) : t = + let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + Hashtbl.replace h.map addr' block; + h + let clone h = copy h end diff --git a/lib/heap/heap_arrayite.ml b/lib/heap/heap_arrayite.ml index 96c8fb2..458d760 100644 --- a/lib/heap/heap_arrayite.ml +++ b/lib/heap/heap_arrayite.ml @@ -5,7 +5,9 @@ module M = struct type block = value array type t = (int, block) Hashtbl.t * int - let init () : t = (Hashtbl.create Parameters.size, 0) + exception BlockNotInHeap + + let init ?(next = 0) () : t = (Hashtbl.create Parameters.size, next) let pp_block fmt (block : block) = Fmt.fprintf fmt "%a" @@ -32,10 +34,7 @@ module M = struct | Val (Int 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" ) + | _ -> raise BlockNotInHeap ) | _ -> failwith "InternalError: HeapArrayIte.in_bounds, arr must be location" @@ -51,7 +50,8 @@ module M = struct | None -> failwith "Block does not exist" ) | _ -> failwith "Location needs to be a concrete value" - let malloc (h : t) (sz : value) (pc : value Pc.t) : (t * value * value Pc.t) list = + let malloc (h : t) (sz : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let tbl, next = h in match Expr.view sz with | Val (Int i) -> @@ -60,8 +60,8 @@ module M = struct | _ -> failwith "InternalError: HeapArrayIte.malloc, size must be an integer" - let update (heap : t) (loc : value) (index : value) (v : value) (path : value Pc.t) : - (t * value Pc.t) list = + let update (heap : t) (loc : value) (index : value) (v : value) + (path : value Pc.t) : (t * value Pc.t) list = let heap', curr = heap in let loc, block = find_block heap loc in match Expr.view index with @@ -70,19 +70,17 @@ module M = struct let _ = Hashtbl.replace heap' loc block in [ ((heap', curr), path) ] | Symbol s when Symbol.type_of s = Ty_int -> - let block' = - Array.mapi - (fun j old_expr -> - let e = - Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int j))) - in - if Eval_symbolic.is_true (e :: path) then - Expr.(Bool.ite e v old_expr) - else old_expr ) - block - in - let _ = Hashtbl.replace heap' loc block' in - [ ((heap', curr), path) ] + let block' = + Array.mapi + (fun j old_expr -> + let e = Expr.(relop Ty.Ty_int Ty.Eq index (make @@ Val (Int j))) in + if Eval_symbolic.is_true (e :: path) then + Expr.(Bool.ite e v old_expr) + else old_expr ) + block + in + let _ = Hashtbl.replace heap' loc block' in + [ ((heap', curr), path) ] | _ -> failwith "Invalid index" let lookup (h : t) (arr : value) (index : value) (pc : value Pc.t) : @@ -145,11 +143,23 @@ module M = struct | Val (Int l) -> ( match Hashtbl.find_opt tbl l with | Some _ -> - Hashtbl.remove tbl l; + Hashtbl.replace tbl l (Array.make 0 Expr.(make @@ Val (Int 0))); [ (h, pc) ] | _ -> failwith "InternalError: HeapArrayIte.free, illegal free" ) | _ -> failwith "InternalError: HeapArrayIte.free, arr must be location" + let get_block ((h, _) : t) (addr : value) : block option = + let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + match Hashtbl.find_opt h addr' with + | Some block -> if Array.length block = 0 then None else Some block + | None -> None + + let set_block (h : t) (addr : value) (block : block) : t = + let h', _ = h in + let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + Hashtbl.replace h' addr' block; + h + let clone h = copy h end diff --git a/lib/heap/heap_concolic.ml b/lib/heap/heap_concolic.ml index d3335f1..a9b9745 100644 --- a/lib/heap/heap_concolic.ml +++ b/lib/heap/heap_concolic.ml @@ -1,14 +1,20 @@ module M = struct - type value = Value.t * Encoding.Expr.t (* indexes and sizes are always values *) - type t = (int, value array) Hashtbl.t + type value = + Value.t * Encoding.Expr.t (* indexes and sizes are always values *) - let init () : t = Hashtbl.create Parameters.size + type block = value array + type t = (int, block) Hashtbl.t + + let init ?(next = 0) () : t = ignore next;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 : value) (_pc : value Pc.t) : (t * value * value Pc.t) list = [] - let update _h (_arr : value) (_index : value) (_v : value) (_pc : value Pc.t) : - (t * value Pc.t) list = + let malloc _h (_sz : value) (_pc : value Pc.t) : (t * value * value Pc.t) list + = + [] + + let update _h (_arr : value) (_index : value) (_v : value) (_pc : value Pc.t) + : (t * value Pc.t) list = [] let lookup _h (_arr : value) (_index : value) (_pc : value Pc.t) : @@ -17,9 +23,12 @@ module M = struct let free _h (_arr : value) (_pc : value Pc.t) : (t * value Pc.t) list = [] - let in_bounds (_heap : t) (_v : value) (_i : value) (_pc : value Pc.t) : bool = + let in_bounds (_heap : t) (_v : value) (_i : value) (_pc : value Pc.t) : bool + = failwith "not implemented" + let get_block (_h : t) (_addr : value) : block option = assert false + let set_block (_h : t) (_addr : value) (_block : block) : t = assert false let clone _ = assert false end diff --git a/lib/heap/heap_concrete.ml b/lib/heap/heap_concrete.ml index 32e925c..e927c40 100644 --- a/lib/heap/heap_concrete.ml +++ b/lib/heap/heap_concrete.ml @@ -5,7 +5,7 @@ module M = struct type t = (int, block) Hashtbl.t * int type value = Value.t (* indexes and sizes are always values *) - let init () : t = (Hashtbl.create Parameters.size, 0) + let init ?(next = 0) () : t = (Hashtbl.create Parameters.size, next) let pp_block fmt (block : block) = Fmt.fprintf fmt "%a" @@ -19,7 +19,8 @@ module M = struct let to_string (heap : t) : string = Fmt.asprintf "%a" pp heap - let malloc (h : t) (sz : value) (pc : value Pc.t) : (t * value * value Pc.t) list = + let malloc (h : t) (sz : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let tbl, next = h in match sz with | Integer i -> @@ -28,8 +29,8 @@ module M = struct | _ -> failwith "InternalError: HeapConcrete.malloc, size must be an integer" - let update (h : t) (arr : value) (index : value) (v : value) (pc : value Pc.t) : - (t * value Pc.t) list = + let update (h : t) (arr : value) (index : value) (v : value) (pc : value Pc.t) + : (t * value Pc.t) list = let tbl, _ = h in match (arr, index) with | Loc l, Integer i -> ( @@ -70,7 +71,8 @@ module M = struct | _ -> failwith "InternalError: illegal free" ) | _ -> failwith "InternalError: HeapConcrete.update, arr must be location" - let in_bounds (heap : t) (addr : value) (i : value) (_pc : value Pc.t) : bool = + let in_bounds (heap : t) (addr : value) (i : value) (_pc : value Pc.t) : bool + = match addr with | Loc l -> ( let tbl, _ = heap in @@ -83,6 +85,8 @@ module M = struct | _ -> failwith "InternalError: HeapConcrete.in_bounds, arr must be location" + let get_block (_h : t) (_addr : value) : block option = assert false + let set_block (_h : t) (_addr : value) (_block : block) : t = assert false let clone _ = assert false end diff --git a/lib/heap/heap_hierarchy.ml b/lib/heap/heap_hierarchy.ml new file mode 100644 index 0000000..98c4b2d --- /dev/null +++ b/lib/heap/heap_hierarchy.ml @@ -0,0 +1,94 @@ +exception BlockNotInHeap + +module M (Heap : Heap_intf.M) : Heap_intf.M with type value = Heap.value = +struct + type value = Heap.value + type block = Heap.block + type h = Heap.t + + type t = + { map : h + ; parent : t option + ; mutable next : int + } + + + let init ?(next = 0) () = { map = Heap.init (); parent = None; next } + + let rec pp (fmt : Fmt.t) (hh : t) : unit = + match hh.parent with + | None -> Fmt.fprintf fmt "%a" Heap.pp hh.map + | Some hh' -> Fmt.fprintf fmt "%a@\n=>@\n%a" Heap.pp hh.map pp hh' + + let to_string (hh : t) = Fmt.asprintf "%a" pp hh + + let malloc (hh : t) (sz : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = + hh.next <- hh.next + 1; + List.map + (fun (h, v, pc) -> ({ hh with map = h }, v, pc)) + (Heap.malloc hh.map sz pc) + + let update (hh : t) (addr : value) (index : value) (v : value) + (pc : value Pc.t) : (t * value Pc.t) list = + let rec update (hh' : t) = + match Heap.get_block hh'.map addr with + | Some block -> + let new_h = Heap.set_block hh.map addr block in + List.map + (fun (h, pc) -> ({ hh' with map = h }, pc)) + (Heap.update new_h addr index v pc) + | None -> ( + match hh'.parent with + | Some parent -> update parent + | None -> failwith "Block not found in" ) + in + update hh + + let lookup (hh : t) (addr : value) (index : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = + let rec lookup (hh' : t) = + match Heap.get_block hh'.map addr with + | Some _ -> + List.map + (fun (h, v, pc) -> ({ hh' with map = h }, v, pc)) + (Heap.lookup hh'.map addr index pc) + | None -> ( + match hh'.parent with + | Some parent -> lookup parent + | None -> failwith "Block not found in" ) + in + lookup hh + + let free (hh : t) (addr : value) (pc : value Pc.t) : (t * value Pc.t) list = + let rec free (hh' : t) = + match Heap.get_block hh'.map addr with + | Some _ -> + List.map + (fun (h, pc) -> ({ hh' with map = h }, pc)) + (Heap.free hh'.map addr pc) + | None -> ( + match hh'.parent with + | Some parent -> free parent + | None -> failwith "Block not found in" ) + in + free hh + + let in_bounds (hh : t) (addr : value) (index : value) (pc : value Pc.t) : bool + = + let rec in_bounds (hh' : t) : bool = + try Heap.in_bounds hh.map addr index pc + with BlockNotInHeap -> ( + match hh'.parent with Some hh' -> in_bounds hh' | None -> false ) + in + in_bounds hh + + let clone hh = + { map = Heap.init () ~next:hh.next; parent = Some hh; next = hh.next } + + let get_block (hh : t) (addr : value) : block option = + Heap.get_block hh.map addr + + let set_block (hh : t) (addr : value) (block : block) : t = + Heap.set_block hh.map addr block |> fun map -> { hh with map } +end diff --git a/lib/heap/heap_intf.ml b/lib/heap/heap_intf.ml index 73e280b..666425b 100644 --- a/lib/heap/heap_intf.ml +++ b/lib/heap/heap_intf.ml @@ -1,14 +1,22 @@ module type M = sig type t (* the representation of the heap itself *) type value (* the type of the index and size of the arrays *) + type block (* the type of the block *) - val init : unit -> t + val init : ?next:int -> unit -> t val pp : Fmt.t -> t -> unit val to_string : t -> string val malloc : t -> value -> value Pc.t -> (t * value * value Pc.t) list - val lookup : t -> value -> value -> value Pc.t -> (t * value * value Pc.t) list - val update : t -> value -> value -> value -> value Pc.t -> (t * value Pc.t) list + + val lookup : + t -> value -> value -> value Pc.t -> (t * value * value Pc.t) list + + val update : + t -> value -> value -> value -> value Pc.t -> (t * value Pc.t) list + val free : t -> value -> value Pc.t -> (t * value Pc.t) list val in_bounds : t -> value -> value -> value Pc.t -> bool val clone : t -> t + val get_block : t -> value -> block option + val set_block : t -> value -> block -> t end diff --git a/lib/heap/heap_oplist.ml b/lib/heap/heap_oplist.ml index 18ac5f1..ecfaadc 100644 --- a/lib/heap/heap_oplist.ml +++ b/lib/heap/heap_oplist.ml @@ -5,17 +5,20 @@ module M = struct type addr = int type size = value type op = value * value * value Pc.t + type block = size * op list type t = - { map : (addr, size * op list) Hashtbl.t + { map : (addr, block) Hashtbl.t ; mutable next : int } + exception BlockNotInHeap + module Eval = Eval_symbolic - let init () : t = { map = Hashtbl.create Parameters.size; next = 0 } + let init ?(next = 0) () : t = { map = Hashtbl.create Parameters.size; next } - let pp_block (fmt : Fmt.t) (block : size * op list) = + let pp_block (fmt : Fmt.t) (block : block) = let open Fmt in let pp_op fmt (i, v, _) = fprintf fmt "(%a %a)" Expr.pp i Expr.pp v in let sz, ops = block in @@ -45,20 +48,18 @@ module M = struct | Symbol s when Symbol.type_of s = Ty_int -> is_within sz i pc | _ -> failwith "InternalError: HeapOpList.in_bounds, size not an integer" ) - | _ -> - failwith - "InternalError: HeapOpList.in_bounds, accessed OpList is not in the \ - heap" ) + | _ -> raise BlockNotInHeap ) | _ -> failwith "InternalError: HeapOpList.in_bounds, v must be location" - let malloc (h : t) (sz : value) (pc : value Pc.t) : (t * value * value Pc.t) list = + let malloc (h : t) (sz : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let next = h.next in Hashtbl.add h.map next (sz, []); h.next <- h.next + 1; [ (h, Expr.(make @@ Val (Int next)), pc) ] - let update (h : t) (arr : value) (index : value) (v : value) (pc : value Pc.t) : - (t * value Pc.t) list = + let update (h : t) (arr : value) (index : value) (v : value) (pc : value Pc.t) + : (t * value Pc.t) list = let lbl = match Expr.view arr with Val (Int i) -> i | _ -> assert false in let arr' = Hashtbl.find_opt h.map lbl in let f ((sz, oplist) : size * op list) : unit = @@ -67,8 +68,8 @@ module M = struct Option.fold ~none:() ~some:f arr'; [ (h, pc) ] - let lookup h (arr : value) (index : value) (pc : value Pc.t) : (t * value * value Pc.t) list - = + let lookup h (arr : value) (index : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let lbl = match Expr.view arr with Val (Int i) -> i | _ -> assert false in let arr' = Hashtbl.find h.map lbl in let _, ops = arr' in @@ -81,11 +82,29 @@ module M = struct in [ (h, v, pc) ] - let free h (arr : value) (pc : value Pc.t) : (t * value Pc.t) list = - let lbl = match Expr.view arr with Val (Int i) -> i | _ -> assert false in - Hashtbl.remove h.map lbl; + let free (h : t) (arr : value) (pc : value Pc.t) : (t * value Pc.t) list = + let addr' = + match Expr.view arr with Val (Int i) -> i | _ -> assert false + in + Hashtbl.replace h.map addr' (Expr.(make @@ Val (Int 0)), []); [ (h, pc) ] + let get_block (h : t) (addr : value) : block option = + let addr' = + match Expr.view addr with Val (Int i) -> i | _ -> assert false + in + match Hashtbl.find_opt h.map addr' with + | Some (size, ops) -> + if size = Expr.(make @@ Val (Int 0)) then None else Some (size, ops) + | None -> None + + let set_block (h : t) (addr : value) (block : block) : t = + let addr' = + match Expr.view addr with Val (Int i) -> i | _ -> assert false + in + Hashtbl.replace h.map addr' block; + h + let copy (heap : t) : t = { map = Hashtbl.copy heap.map; next = heap.next } let clone h = copy h end diff --git a/lib/heap/heap_symbolic.ml b/lib/heap/heap_symbolic.ml index e36dadb..1de3c8c 100644 --- a/lib/heap/heap_symbolic.ml +++ b/lib/heap/heap_symbolic.ml @@ -1,27 +1,33 @@ module M = struct type value = Encoding.Expr.t - type t = (int, value array) Hashtbl.t + type block = value array + type t = (int, block) Hashtbl.t - let init () : t = Hashtbl.create Parameters.size + let init ?(next = 0) () : t = ignore next; 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 : value) (_pc : value Pc.t) : (t * value * value Pc.t) list = + let malloc _h (_sz : value) (_pc : value Pc.t) : (t * value * value Pc.t) list + = assert false - let update _h (_arr : value) (_index : value) (_v : value) (_pc : value Pc.t) : - (t * value Pc.t) list = + let update _h (_arr : value) (_index : value) (_v : value) (_pc : value Pc.t) + : (t * value Pc.t) list = assert false let lookup _h (_arr : value) (_index : value) (_pc : value Pc.t) : (t * value * value Pc.t) list = assert false - let free _h (_arr : value) (_pc : value Pc.t) : (t * value Pc.t) list = assert false + let free _h (_arr : value) (_pc : value Pc.t) : (t * value Pc.t) list = + assert false - let in_bounds (_heap : t) (_v : value) (_i : value) (_pc : value Pc.t) : bool = + let in_bounds (_heap : t) (_v : value) (_i : value) (_pc : value Pc.t) : bool + = assert false + let get_block (_h : t) (_addr : value) : block option = assert false + let set_block (_h : t) (_addr : value) (_block : block) : t = assert false let clone _ = assert false end diff --git a/lib/heap/heap_tree.ml b/lib/heap/heap_tree.ml index 62fd9a3..ee44a73 100644 --- a/lib/heap/heap_tree.ml +++ b/lib/heap/heap_tree.ml @@ -8,20 +8,20 @@ module M = struct | Leaf of range * value | Node of range * tree_t list + type block = tree_t type t = (int, tree_t) Hashtbl.t * int - let init () : t = (Hashtbl.create Parameters.size, 0) + let init ?(next = 0) () : t = (Hashtbl.create Parameters.size, next) 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"} }|} - Expr.pp l Expr.pp r Expr.pp v + fprintf fmt {|{ "leaf": { "range": "[%a, %a]", "value": "%a"} }|} Expr.pp + l Expr.pp r Expr.pp v | Node ((l, r), ch) -> - fprintf fmt - {|{ "node": { "range": "[%a, %a]", "children": [ %a ]} }|} Expr.pp - l Expr.pp r + fprintf fmt {|{ "node": { "range": "[%a, %a]", "children": [ %a ]} }|} + Expr.pp l Expr.pp r (pp_lst ~pp_sep:pp_comma pp_block) ch @@ -41,7 +41,8 @@ module M = struct Hashtbl.iter tree_to_json h'; "Json files created in output directory." - let malloc (h : t) (sz : value) (pc : value Pc.t) : (t * value * value Pc.t) list = + let malloc (h : t) (sz : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let h', curr = h in let tree = Leaf (Expr.(make @@ Val (Int 0), sz), Expr.(make @@ Val (Int 0))) @@ -52,8 +53,8 @@ module M = struct let update h (arr : value) (index : value) (v : value) (pc : value Pc.t) : (t * value Pc.t) list = let h', next = h in - let rec update_tree (tree : tree_t) (index : value) (v : value) (pc : value Pc.t) : - (tree_t * value Pc.t) list option = + let rec update_tree (tree : tree_t) (index : value) (v : value) + (pc : value Pc.t) : (tree_t * value Pc.t) list option = match tree with | Leaf ((left, right), old_v) -> let ge_left = Expr.(relop Ty.Ty_int Ty.Ge index left) in @@ -168,8 +169,8 @@ module M = struct if in_range then List.concat (List.map (search_tree index pc) tree_list) else [] - let lookup h (arr : value) (index : value) (pc : value Pc.t) : (t * value * value Pc.t) list - = + let lookup h (arr : value) (index : value) (pc : value Pc.t) : + (t * value * value Pc.t) list = let tbl, _ = h in match Expr.view arr with @@ -193,7 +194,9 @@ module M = struct (* let ign = to_string h in ignore ign; *) ( match Expr.view arr with - | Val (Int i) -> Hashtbl.remove h' i + | Val (Int i) -> + Hashtbl.replace h' i + (Leaf (Expr.(make @@ Val (Int 0), make @@ Val (Int 0)), Expr.(make @@ Val (Int 0)))) | _ -> failwith "Invalid allocation index" ); [ (h, pc) ] @@ -210,6 +213,22 @@ module M = struct ) | _ -> failwith "InternalError: HeapTree.in_bounds, arr must be location" + let get_block ((h, _) : t) (addr : value) : block option = + let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + match Hashtbl.find_opt h addr' with + | Some tree -> ( + match tree with + | Leaf (r, _) | Node (r, _) -> + if r = (Expr.(make @@ Val (Int 0), make @@ Val (Int 0))) then None + else Some tree ) + | None -> None + + let set_block (h : t) (addr : value) (block : block) : t = + let h', _ = h in + let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + Hashtbl.replace h' addr' block; + h + let copy ((heap, i) : t) : t = (Hashtbl.copy heap, i) let clone h = copy h end diff --git a/test/test_sh.t b/test/test_sh.t new file mode 100644 index 0000000..7a21f98 --- /dev/null +++ b/test/test_sh.t @@ -0,0 +1,1842 @@ +Tests Model WriteLists: + $ wl test basic -p --mode sh + + ===================== + Whilloc + ===================== + + Input file: basic/arrayfork/1.wl + Execution mode: sh + + Returned 0 + Assertion violated, counter example: + $_i : Int _ + Assumption evaluated to false + Assumption evaluated to false + Found 1 problems! + + ===================== + Whilloc + ===================== + + Input file: basic/arrayfork/2.wl + Execution mode: sh + + Returned 0 + Assertion violated, counter example: + $_i : Int _ + $_v : Int _ + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Found 1 problems! + + ===================== + Whilloc + ===================== + + Input file: basic/arrayfork/3.wl + Execution mode: sh + + Returned 0 + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/arrayite/1.wl + Execution mode: sh + + Returned 0 + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/1.wl + Execution mode: sh + + >Program Print + 6 + + >Program Print + 28 + + >Program Print + 5 + + >Program Print + 5 + + >Program Print + 10 + + >Program Print + 9 + + >Program Print + 1 + 1 + + >Program Print + 1 + 2 + + >Program Print + 1 + 3 + + >Program Print + 1 + 4 + + >Program Print + 2 + 1 + + >Program Print + 2 + 2 + + >Program Print + 2 + 3 + + >Program Print + 2 + 4 + + >Program Print + 3 + 1 + + >Program Print + 3 + 2 + + >Program Print + 3 + 3 + + >Program Print + 3 + 4 + + >Program Print + 4 + 1 + + >Program Print + 4 + 2 + + >Program Print + 4 + 3 + + >Program Print + 4 + 4 + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/10.wl + Execution mode: sh + + >Program Print + 11 + + >Program Print + 12 + + Returned 1 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/11.wl + Execution mode: sh + + >Program Print + 6 + + >Program Print + $_descending + + >Program Print + (int.add (int.add $_descending 3) 10) + + >Program Print + (int.add (int.add (int.add $_descending 3) 10) 1) + + Returned (int.add (int.add $_descending 3) 10) + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/12.wl + Execution mode: sh + + >Program Print + (int.mul (int.add $_ok_computer 1) 2) + + Returned (int.add $_ok_computer 1) + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/13.wl + Execution mode: sh + + Returned true + Returned false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/14.wl + Execution mode: sh + + Returned 10 + Returned 12 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/15.wl + Execution mode: sh + + >Program Print + $_x + + Returned 5 + Returned 4 + Returned 3 + Assumption evaluated to false + Assumption evaluated to false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/16.wl + Execution mode: sh + + >Program Print + $_miguel + $_rita + $_XXXXXXXXXXXXXXXXXX + + >Program Print + (int.add (int.add $_miguel 1) $_rita) + $_rita + $_XXXXXXXXXXXXXXXXXX + + >Program Print + $_nvidia + $_rita + $_XXXXXXXXXXXXXXXXXX + + Returned (int.mul $_nvidia $_XXXXXXXXXXXXXXXXXX) + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/17.wl + Execution mode: sh + + Returned true + Returned false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/18.wl + Execution mode: sh + + >Program Print + true + + >Program Print + false + + Returned (int.add $_x 1) + Returned (int.add $_x 1) + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/2.wl + Execution mode: sh + + >Program Print + 6 + + >Program Print + false + + >Program Print + 3 + + >Program Print + 2 + + Returned -1 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/3.wl + Execution mode: sh + + Assertion violated, counter example: + Empty model + Found 1 problems! + + ===================== + Whilloc + ===================== + + Input file: basic/common/4.wl + Execution mode: sh + + >Program Print + 6 + + >Program Print + 7 + + Returned 9 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/5.wl + Execution mode: sh + + >Program Print + 24 + + Returned 12 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/6.wl + Execution mode: sh + + Assertion violated, counter example: + Empty model + Found 1 problems! + + ===================== + Whilloc + ===================== + + Input file: basic/common/7.wl + Execution mode: sh + + >Program Print + true + + >Program Print + 1 + + >Program Print + 0 + + >Program Print + 1 + + Returned 1 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/8.wl + Execution mode: sh + + >Program Print + true + true + + >Program Print + false + true + 5 + + >Program Print + 146 + + Returned 73 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/9.wl + Execution mode: sh + + >Program Print + -1 + + Returned -1 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/common/array.wl + Execution mode: sh + + >Program Print + 5 + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/factorial.wl + Execution mode: sh + + Returned 120 + Returned 24 + Returned 6 + Returned 2 + Returned 1 + Assumption evaluated to false + Assumption evaluated to false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/simple1.wl + Execution mode: sh + + Returned 0 + Assertion violated, counter example: + $_i : Int _ + Returned 0 + Assertion violated, counter example: + $_i : Int _ + Found 2 problems! + + ===================== + Whilloc + ===================== + + Input file: basic/statements/delete.wl + Execution mode: sh + + >Program Print + 0 + + >Program Print + 0 + + Returned 0 + Assumption evaluated to false + Assumption evaluated to false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/statements/symbol_int_c.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/tree/1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: basic/tree/2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: basic/tree/3.wl + Execution mode: sh + + Returned 0 + Assertion violated, counter example: + $_i : Int _ + $_j : Int _ + $_k : Int _ + $_v : Int _ + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Found 1 problems! + + ===================== + Whilloc + ===================== + + Input file: basic/tree/4.wl + Execution mode: sh + + Returned 0 + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Assumption evaluated to false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/tree/5.wl + Execution mode: sh + + Returned 0 + Assumption evaluated to false + Assumption evaluated to false + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: basic/wasm.wl + Execution mode: sh + + Returned 0 + Assertion violated, counter example: + $_x : Int _ + $_y : Int _ + Returned 0 + Returned 0 + Found 1 problems! + Total number of files tested: 33 + $ wl test large_arrays_fail -p --mode sh + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_c_read/10000.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_c_read/100000.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_c_read/50000.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/100000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/100000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/100000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/100000_3.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/10000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/10000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/10000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/10000_3.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/50000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/50000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/50000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_c_write_s_read/50000_3.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/100000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/100000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/100000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/10000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/10000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/10000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/50000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/50000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_c_read/50000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/100000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/100000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/100000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/10000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/10000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/10000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/50000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/50000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/c_array_s_write_s_read/50000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_c_read/10000.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_c_read/100000.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_c_read/50000.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/100000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/100000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/100000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/100000_3.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/10000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/10000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/10000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/10000_3.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/50000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/50000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/50000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_c_write_s_read/50000_3.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/100000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/100000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/100000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/10000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/10000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/10000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/50000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/50000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_c_read/50000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/100000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/100000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/100000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/10000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/10000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/10000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/50000_0.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/50000_1.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + + ===================== + Whilloc + ===================== + + Input file: large_arrays_fail/s_array_s_write_s_read/50000_2.wl + Execution mode: sh + + Fatal error: exception Failure("Index out of bounds") + Total number of files tested: 66 + $ wl test large_arrays_pass -p --mode sh + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_c_read/10000.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_c_read/100000.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_c_read/50000.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/100000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/100000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/100000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/100000_3.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/10000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/10000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/10000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/10000_3.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/50000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/50000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/50000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_c_write_s_read/50000_3.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/100000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/100000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/100000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/10000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/10000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/10000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/50000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/50000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_c_read/50000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/100000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/100000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/100000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/10000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/10000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/10000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/50000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/50000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/c_array_s_write_s_read/50000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_c_read/10000.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_c_read/100000.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_c_read/50000.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/100000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/100000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/100000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/100000_3.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/10000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/10000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/10000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/10000_3.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/50000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/50000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/50000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_c_write_s_read/50000_3.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/100000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/100000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/100000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/10000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/10000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/10000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/50000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/50000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_c_read/50000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/100000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/100000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/100000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/10000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/10000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/10000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/50000_0.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/50000_1.wl + Execution mode: sh + + Returned 0 + Everything Ok! + + ===================== + Whilloc + ===================== + + Input file: large_arrays_pass/s_array_s_write_s_read/50000_2.wl + Execution mode: sh + + Returned 0 + Everything Ok! + Total number of files tested: 66 + From 8d1186e024ec00b4b03f7de30a52abcdc53929c1 Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 18 Mar 2024 18:57:02 +0000 Subject: [PATCH 4/5] fmt --- bin/commands/cmd_execute.ml | 6 ++++-- lib/heap/heap_array_fork.ml | 15 +++++++++++---- lib/heap/heap_arrayite.ml | 8 ++++++-- lib/heap/heap_concolic.ml | 5 ++++- lib/heap/heap_hierarchy.ml | 1 - lib/heap/heap_symbolic.ml | 5 ++++- lib/heap/heap_tree.ml | 14 ++++++++++---- test/test_sh.t | 2 +- 8 files changed, 40 insertions(+), 16 deletions(-) diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml index cf62901..61a0008 100644 --- a/bin/commands/cmd_execute.ml +++ b/bin/commands/cmd_execute.ml @@ -128,14 +128,16 @@ let run ?(no_values = false) ?(test = false) input mode = | _ -> None ) rets , List.length rets ) - |Sh -> + | Sh -> let rets = SH.interpret program in ( List.filter_map (fun (out, _) -> if test then Format.printf "%a@." (Outcome.pp ~no_values) out; match out with | Outcome.Error _ | Outcome.EndGas -> Some out - | _ -> None ) rets, List.length rets) + | _ -> None ) + rets + , List.length rets ) in let execution_time = Sys.time () -. start in diff --git a/lib/heap/heap_array_fork.ml b/lib/heap/heap_array_fork.ml index 3ce3e8c..85474a4 100644 --- a/lib/heap/heap_array_fork.ml +++ b/lib/heap/heap_array_fork.ml @@ -11,7 +11,8 @@ module M = struct exception BlockNotInHeap - let init ?(next = 0) () : t = { map = Hashtbl.create Parameters.size; i = next } + let init ?(next = 0) () : t = + { map = Hashtbl.create Parameters.size; i = next } let pp_block fmt (block : block) = Fmt.fprintf fmt "%a" @@ -125,17 +126,23 @@ module M = struct let free (heap : t) (loc : value) (path : value Pc.t) : (t * value Pc.t) list = let loc', _ = find_block heap loc in - let _ = Hashtbl.replace heap.map loc' (Array.make 0 Expr.(make @@ Val (Int 0))) in + let _ = + Hashtbl.replace heap.map loc' (Array.make 0 Expr.(make @@ Val (Int 0))) + in [ (heap, path) ] let get_block (h : t) (addr : value) : block option = - let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + let addr' = + match Expr.view addr with Val (Int l) -> l | _ -> assert false + in match Hashtbl.find_opt h.map addr' with | Some block -> if Array.length block = 0 then None else Some block | None -> None let set_block (h : t) (addr : value) (block : block) : t = - let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + let addr' = + match Expr.view addr with Val (Int l) -> l | _ -> assert false + in Hashtbl.replace h.map addr' block; h diff --git a/lib/heap/heap_arrayite.ml b/lib/heap/heap_arrayite.ml index 458d760..766c8bd 100644 --- a/lib/heap/heap_arrayite.ml +++ b/lib/heap/heap_arrayite.ml @@ -149,14 +149,18 @@ module M = struct | _ -> failwith "InternalError: HeapArrayIte.free, arr must be location" let get_block ((h, _) : t) (addr : value) : block option = - let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + let addr' = + match Expr.view addr with Val (Int l) -> l | _ -> assert false + in match Hashtbl.find_opt h addr' with | Some block -> if Array.length block = 0 then None else Some block | None -> None let set_block (h : t) (addr : value) (block : block) : t = let h', _ = h in - let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + let addr' = + match Expr.view addr with Val (Int l) -> l | _ -> assert false + in Hashtbl.replace h' addr' block; h diff --git a/lib/heap/heap_concolic.ml b/lib/heap/heap_concolic.ml index a9b9745..36fa8d5 100644 --- a/lib/heap/heap_concolic.ml +++ b/lib/heap/heap_concolic.ml @@ -5,7 +5,10 @@ module M = struct type block = value array type t = (int, block) Hashtbl.t - let init ?(next = 0) () : t = ignore next;Hashtbl.create Parameters.size + let init ?(next = 0) () : t = + ignore next; + Hashtbl.create Parameters.size + let pp (_fmt : Fmt.t) (_heap : t) : unit = failwith "Not Implemented" let to_string (_h : t) : string = failwith "Not Implemented" diff --git a/lib/heap/heap_hierarchy.ml b/lib/heap/heap_hierarchy.ml index 98c4b2d..c8a0439 100644 --- a/lib/heap/heap_hierarchy.ml +++ b/lib/heap/heap_hierarchy.ml @@ -12,7 +12,6 @@ struct ; mutable next : int } - let init ?(next = 0) () = { map = Heap.init (); parent = None; next } let rec pp (fmt : Fmt.t) (hh : t) : unit = diff --git a/lib/heap/heap_symbolic.ml b/lib/heap/heap_symbolic.ml index 1de3c8c..2e0432a 100644 --- a/lib/heap/heap_symbolic.ml +++ b/lib/heap/heap_symbolic.ml @@ -3,7 +3,10 @@ module M = struct type block = value array type t = (int, block) Hashtbl.t - let init ?(next = 0) () : t = ignore next; Hashtbl.create Parameters.size + let init ?(next = 0) () : t = + ignore next; + Hashtbl.create Parameters.size + let pp (_fmt : Fmt.t) (_heap : t) : unit = failwith "Not Implemented" let to_string (_h : t) : string = failwith "Not Implemented" diff --git a/lib/heap/heap_tree.ml b/lib/heap/heap_tree.ml index ee44a73..661753d 100644 --- a/lib/heap/heap_tree.ml +++ b/lib/heap/heap_tree.ml @@ -196,7 +196,9 @@ module M = struct ( match Expr.view arr with | Val (Int i) -> Hashtbl.replace h' i - (Leaf (Expr.(make @@ Val (Int 0), make @@ Val (Int 0)), Expr.(make @@ Val (Int 0)))) + (Leaf + ( Expr.(make @@ Val (Int 0), make @@ Val (Int 0)) + , Expr.(make @@ Val (Int 0)) ) ) | _ -> failwith "Invalid allocation index" ); [ (h, pc) ] @@ -214,18 +216,22 @@ module M = struct | _ -> failwith "InternalError: HeapTree.in_bounds, arr must be location" let get_block ((h, _) : t) (addr : value) : block option = - let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + let addr' = + match Expr.view addr with Val (Int l) -> l | _ -> assert false + in match Hashtbl.find_opt h addr' with | Some tree -> ( match tree with | Leaf (r, _) | Node (r, _) -> - if r = (Expr.(make @@ Val (Int 0), make @@ Val (Int 0))) then None + if r = Expr.(make @@ Val (Int 0), make @@ Val (Int 0)) then None else Some tree ) | None -> None let set_block (h : t) (addr : value) (block : block) : t = let h', _ = h in - let addr' = match Expr.view addr with Val (Int l) -> l | _ -> assert false in + let addr' = + match Expr.view addr with Val (Int l) -> l | _ -> assert false + in Hashtbl.replace h' addr' block; h diff --git a/test/test_sh.t b/test/test_sh.t index 7a21f98..856900f 100644 --- a/test/test_sh.t +++ b/test/test_sh.t @@ -1,4 +1,4 @@ -Tests Model WriteLists: +Tests Model Hierarchy Heap using WriteLists: $ wl test basic -p --mode sh ===================== From 427e871905048cf7a262049622c36db767887f0a Mon Sep 17 00:00:00 2001 From: julianayang777 Date: Mon, 18 Mar 2024 19:15:34 +0000 Subject: [PATCH 5/5] update whilloc.opam --- dune-project | 2 +- whilloc.opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dune-project b/dune-project index f2f0cd5..ee09e88 100644 --- a/dune-project +++ b/dune-project @@ -33,7 +33,7 @@ bos cmdliner ppx_deriving_yojson - (encoding (>= "dev"))) + (encoding (= "dev"))) (tags (topics "to describe" your project))) diff --git a/whilloc.opam b/whilloc.opam index a89cbd9..62a271c 100644 --- a/whilloc.opam +++ b/whilloc.opam @@ -17,7 +17,7 @@ depends: [ "bos" "cmdliner" "ppx_deriving_yojson" - "encoding" {>= "dev"} + "encoding" {= "dev"} "odoc" {with-doc} ] build: [