Merge pull request #22 from formalsec/heap_hierarchy

Refactor some variables and Add Heap hierarchy

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

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 =

dune-project

@@ -33,7 +33,7 @@
    bos 
    cmdliner 
    ppx_deriving_yojson
-   (encoding (>= "dev")))
+   (encoding (= "dev")))
  (tags
   (topics "to describe" your project)))
 

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)
 

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

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

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

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);