full symbolic execution with hash-consing

1 files changed, 95 insertions, 35 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 264706d5..708c98f5 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -80,6 +80,17 @@ Definition hsmem_get_sid (hsm: hsmem ) (hid: hashcode): hsmem :=
   | HSstore hsm chunk addr hlsv srce _ => HSstore hsm chunk addr hlsv srce hid
   end.
 
+(* Symbolic final value -- from hash-consed values
+It does not seem useful to hash-consed these final values (because they are final).
+*)
+Inductive hsfval :=
+  | HSnone
+  | HScall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval) (res:reg) (pc:node)
+  | HStailcall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval)
+  | HSbuiltin (ef:external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc:node)
+  | HSjumptable (sv: hsval) (tbl: list node)
+  | HSreturn (res:option hsval)
+.
 
 Section CanonBuilding.
 
@@ -281,7 +292,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
   | Istore chunk addr args src pc' =>
       DO next <~ hslocal_store hst.(hsi_local) chunk addr args src;;
       RET (Some (hsist_set_local hst pc' next))
-   | Icond cond args ifso ifnot _ =>
+  | Icond cond args ifso ifnot _ =>
       let prev := hst.(hsi_local) in
       DO vargs <~ hlist_args prev args ;;
       let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
@@ -289,56 +300,105 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
   | _ => RET None (* TODO jumptable ? *)
   end.
 
+Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
+  match o with
+  | Some x => RET x
+  | None => FAILWITH msg
+  end.
+
 Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate :=
   match path with
   | O => RET hst
   | S p =>
-    DO i <~ match (fn_code f)!(hst.(hsi_pc)) with Some i => RET i | _ => FAILWITH "hsiexec_path: invalid node" end;;
+    DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsiexec_path.internal_error.1";;
     DO ohst1 <~ hsiexec_inst i hst;;
-    DO hst1 <~ match ohst1 with Some x => RET x | _ => FAILWITH "hsiexec_path: invalid path" end;;
+    DO hst1 <~ some_or_fail ohst1 "hsiexec_path.internal_error.2";;
     hsiexec_path p f hst1
   end.
 
-(*
-Record hsstate := { hinternal:> hsistate; hfinal: sfval }.
+Record hsstate := { hinternal:> hsistate; hfinal: hsfval }.
+
+Fixpoint hbuiltin_arg (hst: PTree.t hsval) (arg : builtin_arg reg): ?? builtin_arg hsval := 
+  match arg with
+  | BA r => 
+         DO v <~ hsi_sreg_get hst r;;
+         RET (BA v)
+  | BA_int n => RET (BA_int (A:=hsval) n)
+  | BA_long n => RET (BA_long (A:=hsval) n)
+  | BA_float f0 => RET (BA_float (A:=hsval) f0)
+  | BA_single s => RET (BA_single (A:=hsval) s)
+  | BA_loadstack chunk ptr => RET (BA_loadstack (A:=hsval) chunk ptr)
+  | BA_addrstack ptr => RET (BA_addrstack (A:=hsval) ptr)
+  | BA_loadglobal chunk id ptr => RET (BA_loadglobal (A:=hsval) chunk id ptr)
+  | BA_addrglobal id ptr => RET (BA_addrglobal (A:=hsval) id ptr)
+  | BA_splitlong ba1 ba2 => 
+    DO v1 <~ hbuiltin_arg hst ba1;;
+    DO v2 <~ hbuiltin_arg hst ba2;;
+    RET (BA_splitlong v1 v2)
+  | BA_addptr ba1 ba2 => 
+    DO v1 <~ hbuiltin_arg hst ba1;;
+    DO v2 <~ hbuiltin_arg hst ba2;;
+    RET (BA_addptr v1 v2)
+  end.
+
+Fixpoint hbuiltin_args (hst: PTree.t hsval) (args: list (builtin_arg reg)): ?? list (builtin_arg hsval) :=
+  match args with
+  | nil => RET nil
+  | a::l =>
+    DO ha <~ hbuiltin_arg hst a;;
+    DO hl <~ hbuiltin_args hst l;;
+    RET (ha::hl)
+    end.
+
+Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident) :=
+  match ros with
+  | inl r => DO hr <~ hsi_sreg_get hst r;; RET (inl hr) 
+  | inr s => RET (inr s)
+  end.
 
-Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := 
+Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := 
   match i with
   | Icall sig ros args res pc => 
-    let svos := sum_left_map (hsi_sreg_get prev) ros in
-    let sargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
-    Scall sig svos sargs res pc
+    DO svos <~ hsum_left hst ros;;
+    DO sargs <~ hlist_args hst args;;
+    RET (HScall sig svos sargs res pc)
   | Itailcall sig ros args =>
-    let svos := sum_left_map (hsi_sreg_get prev) ros in
-    let sargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
-    Stailcall sig svos sargs
+    DO svos <~ hsum_left hst ros;;
+    DO sargs <~ hlist_args hst args;;
+    RET (HStailcall sig svos sargs)
   | Ibuiltin ef args res pc =>
-    let sargs := List.map (builtin_arg_inj (hsi_sreg_get prev)) args in
-    Sbuiltin ef sargs res pc
-  | Ireturn or => 
-    let sor := SOME r <- or IN Some (hsi_sreg_get prev r) in
-    Sreturn sor
+    DO sargs <~ hbuiltin_args hst args;;
+    RET (HSbuiltin ef sargs res pc)
   | Ijumptable reg tbl =>
-    let sv := hsi_sreg_get prev reg in
-    Sjumptable sv tbl
-  | _ => Snone
+    DO sv <~ hsi_sreg_get hst reg;;
+    RET (HSjumptable sv tbl)
+  | Ireturn or => 
+    match or with
+    | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr))
+    | None => RET (HSreturn None)
+    end
+  | _ => RET (HSnone)
   end.
 
-Definition init_hsistate_local := {| hsi_lsmem := Sinit::nil; hsi_ok_lsval := nil; hsi_sreg := PTree.empty sval |}.
-
-Definition init_hsistate pc := {| hsi_pc := pc; hsi_exits := nil; hsi_local := init_hsistate_local |}.
-
-Definition hsexec (f: function) (pc:node): option hsstate :=
-  SOME path <- (fn_path f)!pc IN
-  SOME hst <- hsiexec_path path.(psize) f (init_hsistate pc) IN
-  SOME i <- (fn_code f)!(hst.(hsi_pc)) IN
-  Some (match hsiexec_inst i hst with
-       | Some hst' => {| hinternal := hst'; hfinal := Snone |}
-       | None => {| hinternal := hst; hfinal := hsexec_final i hst.(hsi_local) |}
-       end).
-
-
-*)
+Definition init_hsistate_local (_:unit): ?? hsistate_local
+  := DO hm <~ hSinit ();;
+     RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}.
+
+Definition init_hsistate pc: ?? hsistate 
+  := DO hst <~ init_hsistate_local ();;
+     RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}.
+
+Definition hsexec (f: function) (pc:node): ?? hsstate :=
+  DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";;
+  DO hinit <~ init_hsistate pc;;
+  DO hst <~ hsiexec_path path.(psize) f hinit;;
+  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
+  DO ohst <~ hsiexec_inst i hst;;
+  match ohst with
+  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
+  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
+            RET {| hinternal := hst; hfinal := hsvf |}
+  end.
 
 End CanonBuilding.