fix issue 210 in simu_check

2 files changed, 33 insertions, 15 deletions

diff --git a/lib/Impure/ocaml/ImpHConsOracles.ml b/lib/Impure/ocaml/ImpHConsOracles.ml
index 2b66899b..68a33a91 100644
--- a/lib/Impure/ocaml/ImpHConsOracles.ml
+++ b/lib/Impure/ocaml/ImpHConsOracles.ml
@@ -38,12 +38,18 @@ let xhCons (type a) (hp:a hashP) =
   let t = MyHashtbl.create 1000 in
   let logs = ref [] in
   {
-   hC = (fun (k:a hashinfo) ->
+    hC = (fun (k:a hashinfo) ->
+     (* DEBUG:
+     Printf.printf "*in %d -- look for hcodes= " (Obj.magic t);
+     List.iter (fun i -> Printf.printf "%d " i) k.hcodes;
+     print_newline();
+     *)
      match MyHashtbl.find_opt t k with
      | Some d -> d
-     | None -> (*print_string "+";*)
-        let d = hp.set_hid k.hdata (MyHashtbl.length t) in
-        MyHashtbl.add t {k with hdata = d } d; d);
+     | None ->
+         (* DEBUG: Printf.printf "*in %d -- new hid:%d" (Obj.magic t) (MyHashtbl.length t); print_newline(); *)
+         let d = hp.set_hid k.hdata (MyHashtbl.length t) in
+         MyHashtbl.add t {k with hdata = d } d; d);
    next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs));
    next_hid = (fun () -> MyHashtbl.length t);
    remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x);
diff --git a/scheduling/RTLpathSE_impl_junk.v b/scheduling/RTLpathSE_impl_junk.v
index 20ba6161..652f4ca3 100644
--- a/scheduling/RTLpathSE_impl_junk.v
+++ b/scheduling/RTLpathSE_impl_junk.v
@@ -24,9 +24,10 @@ Local Open Scope impure.
 Import ListNotations.
 Local Open Scope list_scope.
 
-(* Definition DEBUG (s: pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)*)
-Definition DEBUG (s: pstring): ?? unit := println("DEBUG simu_check:" +; s).
+Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
+(* Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *) *)
 
+Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).
 
 (** * Implementation of Data-structure use in Hash-consing *)
 
@@ -86,6 +87,7 @@ 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: 
@@ -149,7 +151,9 @@ 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 *) |}.
+    Dict.log := fun hv => 
+         DO hv_name <~ string_of_hashcode (hsval_get_hid hv);;
+         println ("unexpected undef behavior of hashcode:" +; (CamlStr hv_name)) |}.
 Obligation 1.
   wlp_simplify.
 Qed.
@@ -303,10 +307,15 @@ Inductive root_sval: Type :=
 | Rload (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing)
 .
 
+Definition hSop_hSinit (op:operation) (hlsv: hlist_sval): ?? hsval :=
+  DO hsi <~ hSinit ();;
+  hSop op hlsv hsi (* magically remove the dependency on sm ! *)
+  .
+
 Definition root_apply (rsv: root_sval) (lsv: list reg) (hst: hsistate_local) : ?? hsval :=
   DO hlsv <~ hlist_args hst lsv;;
   match rsv with
-  | Rop op => hSop op hlsv hst
+  | Rop op => hSop_hSinit op hlsv
   | Rload trap chunk addr => hSload hst trap chunk addr hlsv
   end.
 
@@ -327,9 +336,8 @@ Definition simplify (rsv: root_sval) (lsv: list reg) (hst: hsistate_local): ?? h
      match is_move_operation op lsv with
      | 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 ! *)
+       hSop_hSinit op hlsv
      end
   | Rload _ chunk addr => 
        DO hlsv <~ hlist_args hst lsv;;
@@ -348,7 +356,9 @@ Definition red_PTree_set (r:reg) (sv: hsval) (hst: PTree.t hsval): PTree.t hsval
 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))
+    then DO hv <~ root_apply rsv lsv hst;;
+         XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);;
+         RET (hv::(hsi_ok_lsval hst))
     else RET (hsi_ok_lsval hst));;
   DO simp <~ simplify rsv lsv hst;;
   RET {| hsi_smem := hst;
@@ -388,7 +398,9 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): ?? hsistate :=
   match path with
   | O => RET hst
   | S p =>
-    DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsiexec_path.internal_error.1";;
+    let pc := hst.(hsi_pc) in
+    XDEBUG pc (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("- sym exec node: " +; name_pc)%string);;
+    DO i <~ some_or_fail ((fn_code f)!pc) "hsiexec_path.internal_error.1";;
     DO ohst1 <~ hsiexec_inst i hst;;
     DO hst1 <~ some_or_fail ohst1 "hsiexec_path.internal_error.2";;
     hsiexec_path p f hst1
@@ -653,9 +665,9 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
   DO hC_hsmem <~ hCons hSMEM;;
   let hsexec := hsexec hC_sval.(hC) hC_hlist_sval.(hC) hC_hsmem.(hC) in
   (* performing the hash-consed executions *)
-  DO name_pc1 <~ string_of_Z (Zpos pc1);; (* DEBUG info *)
-  DEBUG ("entry-point of input superblock: " +; name_pc1);;
+  XDEBUG pc1 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of input superblock: " +; name_pc)%string);;
   DO hst1 <~ hsexec f pc1;;
+  XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);;
   DO hst2 <~ hsexec tf pc2;;
   (* comparing the executions *)
   hsstate_simu_check dm f hst1 hst2.
@@ -708,7 +720,7 @@ Program Definition aux_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf:
        imp_simu_check dm f tf;; 
        RET true
       CATCH_FAIL s, _ =>
-       DEBUG ("simu_check_failure:" +; s);;
+       println ("simu_check_failure:" +; s);;
        RET false
       ENSURE (fun b => b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2));;
    RET (`r).