diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml index faec481..61a0008 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,16 @@ 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/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/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..6dcbf21 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) @@ -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/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_array_fork.ml b/lib/heap/heap_array_fork.ml index 7c0c2e4..85474a4 100644 --- a/lib/heap/heap_array_fork.ml +++ b/lib/heap/heap_array_fork.ml @@ -1,17 +1,20 @@ 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 } + exception BlockNotInHeap - let pp_block fmt (block : bt) = + let init ?(next = 0) () : t = + { map = Hashtbl.create Parameters.size; i = next } + + 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,28 +26,25 @@ 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 | 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" 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,8 @@ 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,36 +62,36 @@ 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') -> 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 : 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') -> @@ -98,37 +99,55 @@ 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 : 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 + 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 -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..766c8bd 100644 --- a/lib/heap/heap_arrayite.ml +++ b/lib/heap/heap_arrayite.ml @@ -1,13 +1,15 @@ 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) + exception BlockNotInHeap - let pp_block fmt (block : bt) = + let init ?(next = 0) () : t = (Hashtbl.create Parameters.size, next) + + 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,29 +21,26 @@ 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) -> ( 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" 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 +50,8 @@ 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 @@ -70,23 +70,21 @@ 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 : 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,19 +137,35 @@ 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) -> ( 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 -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..36fa8d5 100644 --- a/lib/heap/heap_concolic.ml +++ b/lib/heap/heap_concolic.ml @@ -1,29 +1,41 @@ 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 block = value array + type t = (int, block) Hashtbl.t + + let init ?(next = 0) () : t = + ignore next; + Hashtbl.create Parameters.size - 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 update _h (_arr : vt) (_index : vt) (_v : vt) (_pc : vt Pc.t) : - (t * vt 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 : 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 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 -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..e927c40 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 init ?(next = 0) () : t = (Hashtbl.create Parameters.size, next) - 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,8 @@ 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 +29,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 +44,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 +60,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 +71,8 @@ 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 @@ -83,10 +85,12 @@ 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 -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_hierarchy.ml b/lib/heap/heap_hierarchy.ml new file mode 100644 index 0000000..c8a0439 --- /dev/null +++ b/lib/heap/heap_hierarchy.ml @@ -0,0 +1,93 @@ +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 62cf1bf..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 vt (* the type of the index and size of the arrays *) + 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 -> 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 + 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 47848e7..ecfaadc 100644 --- a/lib/heap/heap_oplist.ml +++ b/lib/heap/heap_oplist.ml @@ -1,21 +1,24 @@ 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 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 @@ -28,14 +31,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 @@ -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 : 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,8 +68,8 @@ 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 let _, ops = arr' in @@ -81,14 +82,32 @@ module M = struct in [ (h, v, pc) ] - let free h (arr : vt) (pc : vt Pc.t) : (t * vt 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 -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..2e0432a 100644 --- a/lib/heap/heap_symbolic.ml +++ b/lib/heap/heap_symbolic.ml @@ -1,31 +1,40 @@ module M = struct - type vt = Encoding.Expr.t - type t = (int, vt array) Hashtbl.t + type value = Encoding.Expr.t + type block = value array + type t = (int, block) Hashtbl.t + + let init ?(next = 0) () : t = + ignore next; + Hashtbl.create Parameters.size - 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 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 -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 9225ea1..661753d 100644 --- a/lib/heap/heap_tree.ml +++ b/lib/heap/heap_tree.ml @@ -1,27 +1,27 @@ 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 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 : 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 +50,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 +135,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 +143,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,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 : 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 match Expr.view arr with @@ -188,17 +189,20 @@ 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; *) ( 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) ] - let in_bounds (heap : t) (arr : vt) (i : vt) (pc : vt Pc.t) : bool = - (* Printf.printf "In_bounds .array: %s, i: %s\n PC: %s\n" (Term.to_string arr) (Term.string_of_expression i) (Pc.to_string Term.string_of_expression pc); *) + let in_bounds (heap : t) (arr : value) (i : value) (pc : value Pc.t) : bool = let h', _ = heap in match Expr.view arr with | Val (Int l) -> ( @@ -211,9 +215,29 @@ 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 -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 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/test/test_sh.t b/test/test_sh.t new file mode 100644 index 0000000..856900f --- /dev/null +++ b/test/test_sh.t @@ -0,0 +1,1842 @@ +Tests Model Hierarchy Heap using 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 + diff --git a/whilloc.opam b/whilloc.opam index 97d1a5b..62a271c 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: [