starting implem of hsilocal_simu_test

1 files changed, 75 insertions, 119 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 708c98f5..0bf67110 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -74,7 +74,7 @@ Definition hlist_sval_set_hid (hlsv: hlist_sval) (hid: hashcode): hlist_sval :=
   | HScons hsv hlsv _ => HScons hsv hlsv hid
   end.
 
-Definition hsmem_get_sid (hsm: hsmem ) (hid: hashcode): hsmem :=
+Definition hsmem_set_hid (hsm: hsmem ) (hid: hashcode): hsmem :=
   match hsm with
   | HSinit _ => HSinit hid
   | HSstore hsm chunk addr hlsv srce _ => HSstore hsm chunk addr hlsv srce hid
@@ -402,133 +402,89 @@ Definition hsexec (f: function) (pc:node): ?? hsstate :=
 
 End CanonBuilding.
 
-(*
-(** * The simulation test of concrete symbolic execution *)
+(** * 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.
 
-(* TODO - generalize it with a list of registers to test ? *)
-Definition hsilocal_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate_local) := OK tt.
+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 revmap_check_single (dm: PTree.t node) (n tn: node) : res unit :=
-  match dm ! tn with
-  | None => Error (msg "revmap_check_single: no mapping for tn")
-  | Some res => if (Pos.eq_dec n res) then OK tt
-                else Error (msg "revmap_check_single: n and res do not match")
+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.
 
-(* WARNING: ce code va bouger pas mal quand on aura le hash-consing ! *)
-Fixpoint sval_simub (sv1 sv2: sval) :=
-  match sv1 with
-  | Sinput r =>
-      match sv2 with
-      | Sinput r' => if (Pos.eq_dec r r') then OK tt else Error (msg "sval_simub: Sinput different registers")
-      | _ => Error (msg "sval_simub: Sinput expected")
-      end
-  | Sop op lsv sm =>
-      match sv2 with
-      | Sop op' lsv' sm' =>
-          if (eq_operation op op') then
-            do _ <- list_sval_simub lsv lsv';
-            smem_simub sm sm'
-          else Error (msg "sval_simub: different operations in Sop")
-      | _ => Error (msg "sval_simub: Sop expected")
-      end
-  | Sload sm trap chk addr lsv =>
-      match sv2 with
-      | Sload sm' trap' chk' addr' lsv' =>
-          if (trapping_mode_eq trap trap') then
-            if (chunk_eq chk chk') then
-              if (eq_addressing addr addr') then
-                do _ <- smem_simub sm sm';
-                list_sval_simub lsv lsv'
-              else Error (msg "sval_simub: addressings do not match")
-            else Error (msg "sval_simub: chunks do not match")
-          else Error (msg "sval_simub: trapping modes do not match")
-          (* FIXME - should be refined once we introduce non trapping loads *)
-      | _ => Error (msg "sval_simub: Sload expected")
-      end
-  end
-with list_sval_simub (lsv1 lsv2: list_sval) :=
-  match lsv1 with
-  | Snil =>
-      match lsv2 with
-      | Snil => OK tt
-      | _ => Error (msg "list_sval_simub: lists of different lengths (lsv2 is bigger)")
-      end
-  | Scons sv1 lsv1 =>
-      match lsv2 with
-      | Snil => Error (msg "list_sval_simub: lists of different lengths (lsv1 is bigger)")
-      | Scons sv2 lsv2 =>
-          do _ <- sval_simub sv1 sv2;
-          list_sval_simub lsv1 lsv2
-      end
-  end
-with smem_simub (sm1 sm2: smem) :=
-  match sm1 with
-  | Sinit =>
-      match sm2 with
-      | Sinit => OK tt
-      | _ => Error (msg "smem_simub: Sinit expected")
-      end
-  | Sstore sm chk addr lsv sv =>
-      match sm2 with
-      | Sstore sm' chk' addr' lsv' sv' => 
-          if (chunk_eq chk chk') then
-            if (eq_addressing addr addr') then
-              do _ <- smem_simub sm sm';
-              do _ <- list_sval_simub lsv lsv';
-              sval_simub sv sv'
-            else Error (msg "smem_simub: addressings do not match")
-          else Error (msg "smem_simub: chunks not match")
-      | _ => Error (msg "smem_simub: Sstore expected")
-      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.
 
-Lemma sval_simub_correct sv1: forall sv2,
-  sval_simub sv1 sv2 = OK tt -> sv1 = sv2.
-Proof.
-  induction sv1 using sval_mut with
-    (P0 := fun lsv1 => forall lsv2, list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2)
-    (P1 := fun sm1 => forall sm2, smem_simub sm1 sm2 = OK tt -> sm1 = sm2); simpl; auto.
-  (* Sinput *)
-  - destruct sv2; try discriminate.
-    destruct (Pos.eq_dec r r0); [congruence|discriminate].
-  (* Sop *)
-  - destruct sv2; try discriminate.
-    destruct (eq_operation _ _); [|discriminate]. subst.
-    intro. explore. apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
-  (* Sload *)
-  - destruct sv2; try discriminate.
-    destruct (trapping_mode_eq _ _); [|discriminate].
-    destruct (chunk_eq _ _); [|discriminate].
-    destruct (eq_addressing _ _); [|discriminate].
-    intro. explore. assert (sm = sm0) by auto. assert (lsv = lsv0) by auto.
-    congruence.
-  (* Snil *)
-  - destruct lsv2; [|discriminate]. congruence.
-  (* Scons *)
-  - destruct lsv2; [discriminate|]. intro. explore.
-    apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence.
-  (* Sinit *)
-  - destruct sm2; [|discriminate]. congruence.
-  (* Sstore *)
-  - destruct sm2; [discriminate|].
-    destruct (chunk_eq _ _); [|discriminate].
-    destruct (eq_addressing _ _); [|discriminate].
-    intro. explore.
-    assert (sm = sm2) by auto. assert (lsv = lsv0) by auto. assert (sv1 = srce) by auto.
-    congruence.
-Qed.
+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.
 
-Lemma list_sval_simub_correct lsv1: forall lsv2,
-  list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2.
-Proof.
-  induction lsv1; simpl; auto.
-  - destruct lsv2; try discriminate. reflexivity.
-  - destruct lsv2; try discriminate. intro. explore.
-    apply sval_simub_correct in EQ. assert (lsv1 = lsv2) by auto.
-    congruence.
+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.
 
+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.
+
+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";;
+  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
+  (* TODO - compare on the whole ptree *) RET tt.
+
+(*
 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);