symbolic execution of internal nodes with hash-consing

1 files changed, 70 insertions, 81 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index dd8e80d7..264706d5 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -129,10 +129,10 @@ Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr
    hC_hsval {| hdata:=HSload hsm trap chunk addr hlsv unknown_hid; hcodes :=hv |}.
 
 
-Definition hSTnil (_: unit): ?? hlist_sval :=
+Definition hSnil (_: unit): ?? hlist_sval :=
    hC_hlist_sval {| hdata:=HSnil unknown_hid; hcodes := nil |}.
 
-Definition hSTcons (hsv: hsval) (hlsv: hlist_sval): ?? hlist_sval :=
+Definition hScons (hsv: hsval) (hlsv: hlist_sval): ?? hlist_sval :=
    hC_hlist_sval {| hdata:=HScons hsv hlsv unknown_hid; hcodes := [hsval_get_hid hsv; hlist_sval_get_hid hlsv] |}.
 
 Definition hSinit (_: unit): ?? hsmem :=
@@ -149,63 +149,57 @@ Definition hSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hli
    hC_hsmem {| hdata:=HSstore hsm chunk addr hlsv srce unknown_hid; hcodes := hv |}.
 
 
-
-
-(*
-
-Fixpoint list_sval_inj (l: list sval): list_sval :=
-  match l with
-  | nil => Snil
-  | v::l => Scons v (list_sval_inj l)
-  end.
-
-
 (** * Implementation of local symbolic internal states 
-TODO: use refined symbolic values instead of those from RTLpathSE_theory.
 *)
 
 (** name : Hash-consed Symbolic Internal state local. Later on we will use the
     refinement to introduce hash consing *)
 Record hsistate_local := 
   { 
-    (** [hsi_lsmem] represents the list of smem symbolic evaluations.
-        The first one of the list is the current smem *)
-    hsi_lsmem:> list smem;
+    (** [hsi_smem] represents the current smem symbolic evaluations.
+        (we can recover the previous one from smem)  *)
+    hsi_smem:> hsmem;
     (** For the values in registers:
         1) we store a list of sval evaluations
         2) we encode the symbolic regset by a PTree *)
-    hsi_ok_lsval: list sval;
-    hsi_sreg:> PTree.t sval
+    hsi_ok_lsval: list hsval;
+    hsi_sreg:> PTree.t hsval
   }.
 
-Definition hsi_sreg_get (hst: PTree.t sval) r: sval :=
+Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
    match PTree.get r hst with 
-   | None => Sinput r
-   | Some sv => sv
+   | None => hSinput r
+   | Some sv => RET sv
    end.
 
+Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? hlist_sval :=
+  match l with
+  | nil => hSnil()
+  | r::l =>
+    DO v <~ hsi_sreg_get hst r;;
+    DO hlsv <~ hlist_args hst l;;
+    hScons v hlsv
+  end.
 
-Definition hsi_smem_get (hst: list smem): smem :=
-   match hst with 
-   | nil => Sinit
-   | sm::_ => sm
-   end.
 
 (* Syntax and semantics of symbolic exit states *)
-(* TODO: add hash-consing *)
 Record hsistate_exit := mk_hsistate_exit
-  { hsi_cond: condition; hsi_scondargs: list_sval; hsi_elocal: hsistate_local; hsi_ifso: node }.
+  { hsi_cond: condition; hsi_scondargs: hlist_sval; hsi_elocal: hsistate_local; hsi_ifso: node }.
 
 
 (** * Syntax and Semantics of symbolic internal state *)
 Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }.
 
 (** ** Assignment of memory *)
-Definition hslocal_set_smem (hst:hsistate_local) (sm:smem) :=
-  {| hsi_lsmem := sm::hsi_lsmem hst;
-     hsi_ok_lsval := hsi_ok_lsval hst;
-     hsi_sreg:= hsi_sreg hst
-  |}.
+Definition hslocal_store (hst:hsistate_local) chunk addr args src: ?? hsistate_local :=
+   let pt := hst.(hsi_sreg) in
+   DO hargs <~ hlist_args pt args;;
+   DO hsrc <~ hsi_sreg_get pt src;;
+   DO hm <~ hSstore hst chunk addr hargs hsrc;;
+   RET {| hsi_smem := hm;
+         hsi_ok_lsval := hsi_ok_lsval hst;
+         hsi_sreg:= hsi_sreg hst
+       |}.
 
 (** ** Assignment of local state *)
 
@@ -220,17 +214,17 @@ Inductive root_sval: Type :=
 | Rload (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing)
 .
 
-Definition root_apply (rsv: root_sval) (lsv: list sval) (sm: smem): sval :=
+Definition root_apply (rsv: root_sval) (lsv: list reg) (hst: hsistate_local) : ?? hsval :=
+  DO hlsv <~ hlist_args hst lsv;;
   match rsv with
-  | Rop op => Sop op (list_sval_inj lsv) sm
-  | Rload trap chunk addr => Sload sm trap chunk addr (list_sval_inj lsv)
+  | Rop op => hSop op hlsv hst
+  | Rload trap chunk addr => hSload hst trap chunk addr hlsv
   end.
-Coercion root_apply: root_sval >-> Funclass.
 
 Local Open Scope lazy_bool_scope.
 
 (* NB: return [false] if the rsv cannot fail *)
-Definition may_trap (rsv: root_sval) (lsv: list sval) (sm: smem): bool :=
+Definition may_trap (rsv: root_sval) (lsv: list reg): bool :=
   match rsv with 
   | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lsv) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
   | Rload TRAP _ _  => true
@@ -238,79 +232,74 @@ Definition may_trap (rsv: root_sval) (lsv: list sval) (sm: smem): bool :=
   end.
 
 (* simplify a symbolic value before assignment to a register *)
-Definition simplify (rsv: root_sval) lsv sm: sval :=
+Definition simplify (rsv: root_sval) (lsv: list reg) (hst: hsistate_local): ?? hsval :=
   match rsv with
-  | Rload TRAP chunk addr => Sload sm NOTRAP chunk addr (list_sval_inj lsv)
   | Rop op =>
      match is_move_operation op lsv with
-     | Some arg => arg  (* optimization of Omove *)
-     | None => 
-       if op_depends_on_memory op then
-          rsv lsv sm
-       else
-          Sop op (list_sval_inj lsv) Sinit (* magically remove the dependency on sm ! *)
+     | Some arg => hsi_sreg_get hst arg (* optimization of Omove *)
+     | None =>
+       DO hsi <~ hSinit ();;
+       DO hlsv <~ hlist_args hst lsv;;
+       hSop op hlsv hsi (* magically remove the dependency on sm ! *)
      end
-  | _ => rsv lsv sm
+  | Rload _ chunk addr => 
+       DO hlsv <~ hlist_args hst lsv;;
+       hSload hst NOTRAP chunk addr hlsv
   end.
 
-Definition red_PTree_set (r:reg) (sv: sval) (hst: PTree.t sval): PTree.t sval :=
+Definition red_PTree_set (r:reg) (sv: hsval) (hst: PTree.t hsval): PTree.t hsval :=
   match sv with
-  | Sinput r' =>
+  | HSinput r' _ =>
      if Pos.eq_dec r r' 
      then PTree.remove r' hst
      else PTree.set r sv hst
   | _ => PTree.set r sv hst
   end.
 
-Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv sm :=
-  {| hsi_lsmem := hsi_lsmem hst;
-     hsi_ok_lsval := if may_trap rsv lsv sm then (rsv lsv sm)::(hsi_ok_lsval hst) else hsi_ok_lsval hst;
-     hsi_sreg := red_PTree_set r (simplify rsv lsv sm) (hsi_sreg hst) |}.
+Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv: ?? hsistate_local :=
+  DO hsiok <~ 
+   (if may_trap rsv lsv
+    then DO hv <~ root_apply rsv lsv hst;; RET (hv::(hsi_ok_lsval hst))
+    else RET (hsi_ok_lsval hst));;
+  DO simp <~ simplify rsv lsv hst;;
+  RET {| hsi_smem := hst;
+         hsi_ok_lsval := hsiok;
+         hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}.
 
 (** ** Execution of one instruction *)
 
-Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate := 
+Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := 
   match i with
   | Inop pc' => 
-      Some (hsist_set_local hst pc' hst.(hsi_local))
+      RET (Some (hsist_set_local hst pc' hst.(hsi_local)))
   | Iop op args dst pc' =>
-      let prev := hst.(hsi_local) in
-      let vargs := List.map (hsi_sreg_get prev) args in
-      let next := hslocal_set_sreg prev dst (Rop op) vargs (hsi_smem_get prev) in
-      Some (hsist_set_local hst pc' next)
+      DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rop op) args;;
+      RET (Some (hsist_set_local hst pc' next))
   | Iload trap chunk addr args dst pc' =>
-      let prev := hst.(hsi_local) in
-      let vargs := List.map (hsi_sreg_get prev) args in
-      let next := hslocal_set_sreg prev dst (Rload trap chunk addr) vargs (hsi_smem_get prev) in
-      Some (hsist_set_local hst pc' next)
+      DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rload trap chunk addr) args;;
+      RET (Some (hsist_set_local hst pc' next))
   | Istore chunk addr args src pc' =>
-      let prev := hst.(hsi_local) in
-      let vargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
-      let next := hslocal_set_smem prev (Sstore (hsi_smem_get prev) chunk addr vargs (hsi_sreg_get prev src)) in
-      Some (hsist_set_local hst pc' next)
+      DO next <~ hslocal_store hst.(hsi_local) chunk addr args src;;
+      RET (Some (hsist_set_local hst pc' next))
    | Icond cond args ifso ifnot _ =>
       let prev := hst.(hsi_local) in
-      let vargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in
+      DO vargs <~ hlist_args prev args ;;
       let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
-      Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}
-  | _ => None (* TODO jumptable ? *)
+      RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |})
+  | _ => RET None (* TODO jumptable ? *)
   end.
 
-Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate :=
+Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate :=
   match path with
-  | O => Some hst
+  | O => RET hst
   | S p =>
-    SOME i <- (fn_code f)!(hst.(hsi_pc)) IN
-    SOME hst1 <- hsiexec_inst i hst IN
+    DO i <~ match (fn_code f)!(hst.(hsi_pc)) with Some i => RET i | _ => FAILWITH "hsiexec_path: invalid node" end;;
+    DO ohst1 <~ hsiexec_inst i hst;;
+    DO hst1 <~ match ohst1 with Some x => RET x | _ => FAILWITH "hsiexec_path: invalid path" end;;
     hsiexec_path p f hst1
   end.
 
-(* Definition hfinal_refines hfv fv := forall pge ge sp npc stk f rs0 m0 rs' m' t s',
-  ssem_final pge ge sp npc stk f rs0 m0 hfv rs' m' t s' <-> ssem_final pge ge sp npc stk f rs0 m0 fv rs' m' t s'. *)
-
-(* FIXME - too strong let's change it later.. *)
-Definition hfinal_refines (hfv fv: sfval) := hfv = fv.
-
+(*
 Record hsstate := { hinternal:> hsistate; hfinal: sfval }.
 
 Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval :=