Implem of hsiexit_simu_check

1 files changed, 167 insertions, 102 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 0bf67110..359f4578 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -24,7 +24,9 @@ Local Open Scope impure.
 Import ListNotations.
 Local Open Scope list_scope.
 
-(** * Refinement of symbolic values/symbolic memories with hash-consing data *)
+(** * Implementation of Data-structure use in Hash-consing *)
+
+(** ** Implementation of symbolic values/symbolic memories with hash-consing data *)
 
 Inductive hsval :=
   | HSinput (r: reg) (hid:hashcode)
@@ -80,6 +82,75 @@ Definition hsmem_set_hid (hsm: hsmem ) (hid: hashcode): hsmem :=
   | HSstore hsm chunk addr hlsv srce _ => HSstore hsm chunk addr hlsv srce hid
   end.
 
+(* Now, we build the hash-Cons value from a "hash_eq".
+
+Informal specification: 
+  [hash_eq] must be consistent with the "hashed" constructors defined above.
+
+We expect that hashinfo values in the code of these "hashed" constructors verify:
+
+  (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
+*)
+
+Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
+  match sv1, sv2 with
+  | HSinput r1 _, HSinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *)
+  | HSop op1 lsv1 sm1 _, HSop op2 lsv2 sm2 _  =>
+     DO b1 <~ phys_eq lsv1 lsv2;;
+     DO b2 <~ phys_eq sm1 sm2;;
+     if b1 && b2 
+     then struct_eq op1 op2 (* NB: really need a struct_eq here ? *)
+     else RET false
+  | HSload sm1 trap1 chk1 addr1 lsv1 _, HSload sm2 trap2 chk2 addr2 lsv2 _ =>
+     DO b1 <~ phys_eq lsv1 lsv2;;
+     DO b2 <~ phys_eq sm1 sm2;;
+     DO b3 <~ struct_eq trap1 trap2;;
+     DO b4 <~ struct_eq chk1 chk2;;
+     if b1 && b2 && b3 && b4
+     then struct_eq addr1 addr2
+     else RET false
+  | _,_ => RET false
+  end.
+
+Definition hlist_sval_hash_eq (lsv1 lsv2: hlist_sval): ?? bool :=
+  match lsv1, lsv2 with
+  | HSnil _, HSnil _ => RET true
+  | HScons sv1 lsv1' _, HScons sv2 lsv2' _  =>
+     DO b <~ phys_eq lsv1' lsv2';;
+     if b 
+     then phys_eq sv1 sv2
+     else RET false
+  | _,_ => RET false
+  end.
+
+Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool :=
+  match sm1, sm2 with
+  | HSinit _, HSinit _ => RET true
+  | HSstore sm1 chk1 addr1 lsv1 sv1 _, HSstore sm2 chk2 addr2 lsv2 sv2 _ =>
+     DO b1 <~ phys_eq lsv1 lsv2;;
+     DO b2 <~ phys_eq sm1 sm2;;
+     DO b3 <~ phys_eq sv1 sv2;;
+     DO b4 <~ struct_eq chk1 chk2;;
+     if b1 && b2 && b3 && b4
+     then struct_eq addr1 addr2
+     else RET false
+  | _,_ => RET false
+  end.
+
+Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. 
+Definition hLSVAL: hashP hlist_sval := {| hash_eq := hlist_sval_hash_eq; get_hid:= hlist_sval_get_hid; set_hid:= hlist_sval_set_hid |}.
+Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}.
+
+Program Definition mk_hash_params: Dict.hash_params hsval :=
+ {|
+    Dict.test_eq := phys_eq;
+    Dict.hashing := fun (ht: hsval) => RET (hsval_get_hid ht);
+    Dict.log := fun _ => RET () (* NB no log *) |}.
+Obligation 1.
+  wlp_simplify.
+Qed.
+
+
 (* Symbolic final value -- from hash-consed values
 It does not seem useful to hash-consed these final values (because they are final).
 *)
@@ -92,6 +163,35 @@ Inductive hsfval :=
   | HSreturn (res:option hsval)
 .
 
+(** ** Implementation of symbolic states 
+*)
+
+(** name : Hash-consed Symbolic Internal state local.  *)
+Record hsistate_local := 
+  { 
+    (** [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 hsval;
+    hsi_sreg:> PTree.t hsval
+  }.
+
+(* Syntax and semantics of symbolic exit states *)
+Record hsistate_exit := mk_hsistate_exit
+  { 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 }.
+
+(** ** Syntax and Semantics of symbolic state *)
+Record hsstate := { hinternal:> hsistate; hfinal: hsfval }.
+
+
+(** * Implementation of symbolic execution *)
 Section CanonBuilding.
 
 Variable hC_hsval: hashinfo hsval -> ?? hsval.
@@ -160,23 +260,6 @@ Definition hSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hli
    hC_hsmem {| hdata:=HSstore hsm chunk addr hlsv srce unknown_hid; hcodes := hv |}.
 
 
-(** * Implementation of local symbolic internal states 
-*)
-
-(** name : Hash-consed Symbolic Internal state local. Later on we will use the
-    refinement to introduce hash consing *)
-Record hsistate_local := 
-  { 
-    (** [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 hsval;
-    hsi_sreg:> PTree.t hsval
-  }.
-
 Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
    match PTree.get r hst with 
    | None => hSinput r
@@ -192,15 +275,6 @@ Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? hlist_sval :=
     hScons v hlsv
   end.
 
-
-(* Syntax and semantics of symbolic exit states *)
-Record hsistate_exit := mk_hsistate_exit
-  { 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_store (hst:hsistate_local) chunk addr args src: ?? hsistate_local :=
    let pt := hst.(hsi_sreg) in
@@ -316,8 +390,6 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate :=
     hsiexec_path p f hst1
   end.
 
-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 => 
@@ -404,95 +476,88 @@ End CanonBuilding.
 
 (** * The simulation test of concrete hash-consed symbolic execution *)
 
-(* Now, we build the hash-Cons value from a "hash_eq".
-
-Informal specification: 
-  [hash_eq] must be consistent with the "hashed" constructors defined above.
-
-We expect that hashinfo values in the code of these "hashed" constructors verify:
+Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
+  DO b <~ phys_eq x y;;
+  assert_b b msg;;
+  RET tt.
 
-  (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
-*)
+Definition struct_check {A} (x y:A) (msg: pstring): ?? unit :=
+  DO b <~ struct_eq x y;;
+  assert_b b msg;;
+  RET tt.
 
-Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
-  match sv1, sv2 with
-  | HSinput r1 _, HSinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *)
-  | HSop op1 lsv1 sm1 _, HSop op2 lsv2 sm2 _  =>
-     DO b1 <~ phys_eq lsv1 lsv2;;
-     DO b2 <~ phys_eq sm1 sm2;;
-     if b1 && b2 
-     then struct_eq op1 op2 (* NB: really need a struct_eq here ? *)
-     else RET false
-  | HSload sm1 trap1 chk1 addr1 lsv1 _, HSload sm2 trap2 chk2 addr2 lsv2 _ =>
-     DO b1 <~ phys_eq lsv1 lsv2;;
-     DO b2 <~ phys_eq sm1 sm2;;
-     DO b3 <~ struct_eq trap1 trap2;;
-     DO b4 <~ struct_eq chk1 chk2;;
-     if b1 && b2 && b3 && b4
-     then struct_eq addr1 addr2
-     else RET false
-  | _,_ => RET false
+Definition option_eq_check {A} (o1 o2: option A): ?? unit :=
+  match o1, o2 with
+  | Some x1, Some x2 => phys_check x1 x2 "option_eq_check: data physically differ"
+  | None, None => RET tt
+  | _, _ => FAILWITH "option_eq_check: structure differs"
   end.
 
-Definition hlist_sval_hash_eq (lsv1 lsv2: hlist_sval): ?? bool :=
-  match lsv1, lsv2 with
-  | HSnil _, HSnil _ => RET true
-  | HScons sv1 lsv1' _, HScons sv2 lsv2' _  =>
-     DO b <~ phys_eq lsv1' lsv2';;
-     if b 
-     then phys_eq sv1 sv2
-     else RET false
-  | _,_ => RET false
+Lemma option_eq_check_correct A (o1 o2: option A): WHEN option_eq_check o1 o2 ~> _ THEN o1=o2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque option_eq_check.
+Global Hint Resolve option_eq_check_correct:wlp.
+
+Import PTree.
+
+Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
+  match d1, d2 with
+  | Leaf, Leaf => RET tt
+  | Node l1 o1 r1, Node l2 o2 r2 =>
+      option_eq_check o1 o2;;
+      PTree_eq_check l1 l2;;
+      PTree_eq_check r1 r2
+  | _, _ => FAILWITH "PTree_eq_check: some key is absent"
   end.
 
-Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool :=
-  match sm1, sm2 with
-  | HSinit _, HSinit _ => RET true
-  | HSstore sm1 chk1 addr1 lsv1 sv1 _, HSstore sm2 chk2 addr2 lsv2 sv2 _ =>
-     DO b1 <~ phys_eq lsv1 lsv2;;
-     DO b2 <~ phys_eq sm1 sm2;;
-     DO b3 <~ phys_eq sv1 sv2;;
-     DO b4 <~ struct_eq chk1 chk2;;
-     if b1 && b2 && b3 && b4
-     then struct_eq addr1 addr2
-     else RET false
-  | _,_ => RET false
+Lemma PTree_eq_check_correct A d1: forall (d2: t A),
+ WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2.
+Proof.
+  induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; 
+  wlp_simplify. destruct x; simpl; auto.
+Qed.
+Global Opaque PTree_eq_check.
+
+Fixpoint PTree_frame_eq_check {A} (frame: list positive) (d1 d2: PTree.t A): ?? unit :=
+  match frame with
+  | nil => RET tt
+  | k::l => 
+    option_eq_check (PTree.get k d1) (PTree.get k d2);;
+    PTree_frame_eq_check l d1 d2
   end.
 
-Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. 
-Definition hLSVAL: hashP hlist_sval := {| hash_eq := hlist_sval_hash_eq; get_hid:= hlist_sval_get_hid; set_hid:= hlist_sval_set_hid |}.
-Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}.
-
-Program Definition mk_hash_params: Dict.hash_params hsval :=
- {|
-    Dict.test_eq := phys_eq;
-    Dict.hashing := fun (ht: hsval) => RET (hsval_get_hid ht);
-    Dict.log := fun _ => RET () (* NB no log *) |}.
-Obligation 1.
-  wlp_simplify.
+Lemma PTree_frame_eq_check_correct A l (d1 d2: t A):
+ WHEN PTree_frame_eq_check l d1 d2 ~> _ THEN forall x, List.In x l -> PTree.get x d1 = PTree.get x d2.
+Proof.
+  induction l as [|k l]; simpl; wlp_simplify.
+  subst; auto.
 Qed.
+Global Opaque PTree_frame_eq_check.
+
+Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
+  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
+  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
+  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2).
 
 Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit :=
   DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";;
-  DO b <~ phys_eq n res;; (* NB: phys_eq on nodes is probably sufficient *)
-  assert_b b "revmap_check_single: n and res are physically different";;
-  RET tt.
+  phys_check n res "revmap_check_single: n and res are physically different".
 
-Definition hsilocal_simu_test hst1 hst2 : ?? unit :=
-  DO b <~ phys_eq (hsi_smem hst2) (hsi_smem hst1);;
-  assert_b b "hsi_smem sets aren't equiv";;
+Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
+  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
-  (* TODO - compare on the whole ptree *) RET tt.
+  PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2).
 
-(*
-Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) :=
-  if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then
-    do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2);
-    do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2);
-    revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2)
-  else Error (msg "siexit_simub: conditions do not match")
-.
+Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit): ?? unit :=
+  struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";;
+  phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";;
+  revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2);;
+  DO path <~ some_or_fail ((fn_path f) ! (hsi_ifso hse1)) "hsiexit_simu_check: internal error";;
+  hsilocal_frame_simu_check (Regset.elements path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2).
 
+(*
 Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
   match lhse1 with
   | nil =>