more debug info for simu_check

1 files changed, 16 insertions, 6 deletions

diff --git a/scheduling/RTLpathSE_impl_junk.v b/scheduling/RTLpathSE_impl_junk.v
index 1b4efad7..20ba6161 100644
--- a/scheduling/RTLpathSE_impl_junk.v
+++ b/scheduling/RTLpathSE_impl_junk.v
@@ -24,6 +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).
+
+
 (** * Implementation of Data-structure use in Hash-consing *)
 
 (** ** Implementation of symbolic values/symbolic memories with hash-consing data *)
@@ -537,18 +541,22 @@ Qed.
 Global Opaque PTree_frame_eq_check.
 
 Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
+  DEBUG("? last check");;
   phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
+  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2);;
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
-  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2).
+  DEBUG("=> last check: OK").
 
 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";;
   struct_check n res "revmap_check_single: n and res are physically different".
 
 Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
+  DEBUG("? frame check");;
   phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
+  PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2);;
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
-  PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2).
+  DEBUG("=> frame check: OK").
 
 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";;
@@ -567,8 +575,8 @@ Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhs
   end.
 
 Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
-  hsilocal_simu_check (hsi_local hst1) (hsi_local hst2);;
-  hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2).
+  hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);;
+  hsilocal_simu_check (hsi_local hst1) (hsi_local hst2).
 
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   match ln, ln' with
@@ -645,6 +653,8 @@ 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);;
   DO hst1 <~ hsexec f pc1;;
   DO hst2 <~ hsexec tf pc2;;
   (* comparing the executions *)
@@ -680,7 +690,7 @@ Global Hint Resolve simu_check_rec_correct: wlp.
 
 Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit :=
    simu_check_rec dm f tf (PTree.elements dm);;
-   println("simu_check OK!").
+   DEBUG("simu_check OK!").
 
 Local Hint Resolve PTree.elements_correct: core.
 Lemma imp_simu_check_correct dm f tf:
@@ -698,7 +708,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, _ =>
-       println ("simu_check_failure:" +; s);;
+       DEBUG ("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).