CLEAN THE PREVIOUS COMMIT !

By default: restore the initial behavior of abstractbb/ImpSimuTest

In order to print the dump:
  set the boolean FULL_DEBUG_DUMP (at the top of the file) to true.
And recompile Coq files.

1 files changed, 73 insertions, 69 deletions

diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v
index e5a15e5f..6b64e1d8 100644
--- a/kvx/abstractbb/ImpSimuTest.v
+++ b/kvx/abstractbb/ImpSimuTest.v
@@ -23,9 +23,8 @@ Require Export Impure.ImpHCons. (**r Import the Impure library. See https://gith
 Export Notations.
 Import HConsing.
 
-
+Require Import Coq.Bool.Bool.
 Require Export SeqSimuTheory.
-
 Require Import PArith.
 
 
@@ -35,6 +34,8 @@ Import ListNotations.
 Local Open Scope list_scope.
 
 
+Definition FULL_DEBUG_DUMP : bool := false. (* print debug traces, even if the verifier succeeds. *)
+
 (** * Interface of (impure) equality tests for operators *)
 Module Type ImpParam.
 
@@ -673,8 +674,8 @@ Hypothesis hco_term_correct: forall t, WHEN hco_term.(hC) t ~> t' THEN forall ge
 Variable hco_list: hashConsing list_term.
 Hypothesis hco_list_correct: forall t, WHEN hco_list.(hC) t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m.
 
-Variable print_error_end: hsmem -> hsmem -> ?? unit.
-Variable print_error: pstring -> ?? unit.
+Variable print_end_error: hsmem -> hsmem -> ?? unit.
+Variable print_dump: (option pstring) -> ?? unit.
 
 Variable check_failpreserv: bool.
 Variable dbg_failpreserv: term -> ?? unit. (* info of additional failure of the output bbloc p2 wrt the input bbloc p1 *) 
@@ -687,24 +688,23 @@ Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool :=
     DO d2 <~ bblock_hsmem hco_term.(hC) hco_list.(hC) no_log_assign log_new_term log_inst2 p2;;
     DO b <~ Dict.eq_test d1 d2 ;;
     if b then (
-      if check_failpreserv then (
+      (if check_failpreserv then
           let hp := mk_hash_params dbg_failpreserv in
           failure_in_failpreserv.(set)(true);;
-          Sets.assert_list_incl hp d2.(hpre) d1.(hpre);;
-          print_error_end d1 d2;;
-          RET true
-      ) else (
-        print_error_end d1 d2;;
-        RET false
-      )
+          Sets.assert_list_incl hp d2.(hpre) d1.(hpre)
+      else RET tt);;
+      (if FULL_DEBUG_DUMP then
+        print_dump None (* not an error... *)
+      else RET tt);;
+      RET check_failpreserv
     ) else (
-      print_error_end d1 d2 ;;
+      print_end_error d1 d2 ;;
       RET false
     )
   CATCH_FAIL s, _ =>
     DO b <~ failure_in_failpreserv.(get)();;
     if b then RET false 
-         else print_error s;; RET false
+         else print_dump (Some s);; RET false
   ENSURE (fun b => b=true -> forall ge, bblock_simu ge p1 p2));;
   RET (`r).
 Obligation 1.
@@ -777,12 +777,16 @@ Definition msg_unknow_term: pstring := "unknown term".
 Definition msg_number: pstring := "on 2nd bblock -- on inst num ".
 Definition msg_notfailpreserv: pstring := "a possible failure of 2nd bblock is absent in 1st bblock (INTERNAL ERROR: this error is expected to be detected before!!!)".
 
-Definition print_error_end (_ _: hsmem): ?? unit
- := println (""). (*msg_prefix +; msg_error_on_end). *)
+Definition print_end_error (_ _: hsmem): ?? unit
+ := println (msg_prefix +; msg_error_on_end).
 
-Definition print_error (log: logger unit) (s:pstring): ?? unit
- := DO n <~ log_info log ();;
-    println (msg_prefix +; msg_number +; n +; " -- " +; s). 
+Definition print_error (log: logger unit) (os: option pstring): ?? unit
+ := match os with
+    | Some s =>
+      DO n <~ log_info log ();;
+      println (msg_prefix +; msg_number +; n +; " -- " +; s)
+    | None => RET tt
+    end.
 
 Definition failpreserv_error (_: term): ?? unit
   := println (msg_prefix +; msg_notfailpreserv).
@@ -812,7 +816,7 @@ Program Definition bblock_simu_test (p1 p2: bblock): ?? bool :=
     (log_insert log)
     hco_term _
     hco_list _
-    print_error_end
+    print_end_error
     (print_error log)
     true (* check_failpreserv *)
     failpreserv_error
@@ -909,7 +913,6 @@ with string_of_list_term (l: list_term): ?? pstring :=
      RET (st +; ";" +; sl)
   end.
 
-
 End PrettryPrint.
 
 
@@ -952,8 +955,7 @@ Definition print_tables gdi ext exl: ?? unit :=
   iterall exl (fun head _ pl => print_list gdi head pl.(hdata));;
   println "----------------".
 
-Definition print_final_debug {A} (gdi:A) (d1 d2: hsmem): ?? unit := RET tt.
-(* 
+Definition print_final_debug gdi (d1 d2: hsmem): ?? unit
  := DO b <~ Dict.not_eq_witness d1 d2 ;;
     match b with
     | Some x =>
@@ -973,7 +975,6 @@ Definition print_final_debug {A} (gdi:A) (d1 d2: hsmem): ?? unit := RET tt.
       end
     | None => FAILWITH "bug in Dict.not_eq_witness ?"
     end.
-*)
 
 Definition witness:= option term.
 
@@ -992,39 +993,44 @@ Definition print_witness gdi cr (*msg*) :=
   | None => println "Unexpected failure: no witness info (hint: hash-consing bug ?)"
   end.
 
-
-Definition print_error_end1 gdi hct hcl (d1 d2:hsmem): ?? unit
+Definition print_end_error1 gdi hct hcl (d1 d2:hsmem): ?? unit
  := println "- GRAPH of 1st bblock";;
     DO ext <~ export hct ();;
     DO exl <~ export hcl ();;
     print_tables gdi ext exl;;
-    print_error_end d1 d2;;
+    print_end_error d1 d2;;
     print_final_debug gdi d1 d2.
 
-Definition print_error1 gdi hct hcl cr log s : ?? unit
+Definition print_dump1 gdi hct hcl cr log os : ?? unit
  := println "- GRAPH of 1st bblock";;
     DO ext <~ export hct ();;
     DO exl <~ export hcl ();;
     print_tables gdi ext exl;;
-    print_error log s;;
-    print_witness gdi cr (*"1st"*).
-
+    print_error log os;;
+    match os with
+    | Some _ => print_witness gdi cr (*"1st"*)
+    | None => RET tt
+    end.
 
 Definition xmsg_number: pstring := "on 1st bblock -- on inst num ".
 
-Definition print_error_end2 gdi hct hcl (d1 d2:hsmem): ?? unit
- := (* println (msg_prefix +; msg_error_on_end);; *)
+Definition print_end_error2 gdi hct hcl (d1 d2:hsmem): ?? unit
+ := println (msg_prefix +; msg_error_on_end);;
     println "- GRAPH of 2nd bblock";;
     DO ext <~ export hct ();;
     DO exl <~ export hcl ();;
     print_tables gdi ext exl.
 
-Definition print_error2 gdi hct hcl cr (log: logger unit) (s:pstring): ?? unit
+Definition print_dump2 gdi hct hcl cr (log: logger unit) (os:option pstring): ?? unit
  := DO n <~ log_info log ();;
     DO ext <~ export hct ();;
     DO exl <~ export hcl ();;
-    println (msg_prefix +; xmsg_number +; n +; " -- " +; s);;
-    print_witness gdi cr (*"2nd"*);;
+    match os with
+    | Some s =>
+      println (msg_prefix +; xmsg_number +; n +; " -- " +; s);;
+      print_witness gdi cr (*"2nd"*)
+    | None => RET tt
+    end;;
     println "- GRAPH of 2nd bblock";;
     print_tables gdi ext exl.
 
@@ -1057,23 +1063,25 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
   DO cr <~ make_cref None;;
   DO hco_term <~ mk_annot (hCons hpt);;
   DO hco_list <~ mk_annot (hCons hplt);;
-  println("");;
-  println("-- START simu checker --");;
-  DO result1 <~ g_bblock_simu_test
+  (if FULL_DEBUG_DUMP then
+      println("");;
+      println("-- START simu checker --")
+   else RET tt);;
+  DO result1 <~ (g_bblock_simu_test
      (log_assign dict_info log1)
      (log_new_term (msg_term cr))
      (hlog log1 hco_term hco_list)
      (log_insert log2)
      hco_term _
      hco_list _
-     (print_error_end1 dict_info.(D.get) hco_term hco_list)
-     (print_error1 dict_info.(D.get) hco_term hco_list cr log2)
+     (print_end_error1 dict_info.(D.get) hco_term hco_list)
+     (print_dump1 dict_info.(D.get) hco_term hco_list cr log2)
      true
      failpreserv_error
-     p1 p2;;
-(*  if result1 
-  then RET true
-  else *)
+     p1 p2);;
+   if (if FULL_DEBUG_DUMP then false else result1)
+   then RET true
+   else (
     DO dict_info <~ make_dict (mk_hash_params (fun _ => RET tt));;
     DO log1 <~ count_logger ();;
     DO log2 <~ count_logger ();;
@@ -1088,41 +1096,37 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool :=
        (log_insert log2)
        hco_term _
        hco_list _
-       (print_error_end2 dict_info.(D.get) hco_term hco_list)
-       (print_error2 dict_info.(D.get) hco_term hco_list cr log2)
+       (print_end_error2 dict_info.(D.get) hco_term hco_list)
+       (print_dump2 dict_info.(D.get) hco_term hco_list cr log2)
        false
        (fun _ => RET tt)
        p2 p1;;
-    println("-- END simu checker --");;
-    println("");;
-    RET result1.
-(*
-    if result2 
-    then (
-      println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test  => this is a bug of bblock_simu_test ??");;
-      RET false
-    ) else RET false
-   .*)
+     if FULL_DEBUG_DUMP then
+        println("-- END simu checker --");;
+        println("");;
+        RET result1
+     else if result2
+     then (
+       println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test  => this is a bug of bblock_simu_test ??");;
+       RET false
+     ) else RET false
+  ).
 Obligation 1.
-Admitted. (*
-  generalize (hCons_correct _ _ _ H0); clear H0.
+  generalize (hCons_correct _ _ _ H1); clear H1.
   wlp_simplify.
-Qed.*)
+Qed.
 Obligation 2.
-Admitted. (*
-  generalize (hCons_correct _ _ _ H); clear H.
+  generalize (hCons_correct _ _ _ H0); clear H0.
   wlp_simplify.
-Qed.*)
+Qed.
 Obligation 3.
-Admitted. (*
-  generalize (hCons_correct _ _ _ H0); clear H0.
+  generalize (hCons_correct _ _ _ H1); clear H1.
   wlp_simplify.
-Qed.*)
+Qed.
 Obligation 4.
-Admitted. (*
-  generalize (hCons_correct _ _ _ H); clear H.
+  generalize (hCons_correct _ _ _ H0); clear H0.
   wlp_simplify.
-Qed.*)
+Qed.
 
 Theorem verb_bblock_simu_test_correct p1 p2:
   WHEN verb_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.