hsstate_simu_check

1 files changed, 89 insertions, 220 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 359f4578..f08998b4 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -395,14 +395,14 @@ Fixpoint hbuiltin_arg (hst: PTree.t hsval) (arg : builtin_arg reg): ?? builtin_a
   | BA r => 
          DO v <~ hsi_sreg_get hst r;;
          RET (BA v)
-  | BA_int n => RET (BA_int (A:=hsval) n)
-  | BA_long n => RET (BA_long (A:=hsval) n)
-  | BA_float f0 => RET (BA_float (A:=hsval) f0)
-  | BA_single s => RET (BA_single (A:=hsval) s)
-  | BA_loadstack chunk ptr => RET (BA_loadstack (A:=hsval) chunk ptr)
-  | BA_addrstack ptr => RET (BA_addrstack (A:=hsval) ptr)
-  | BA_loadglobal chunk id ptr => RET (BA_loadglobal (A:=hsval) chunk id ptr)
-  | BA_addrglobal id ptr => RET (BA_addrglobal (A:=hsval) id ptr)
+  | BA_int n => RET (BA_int n)
+  | BA_long n => RET (BA_long n)
+  | BA_float f0 => RET (BA_float f0)
+  | BA_single s => RET (BA_single s)
+  | BA_loadstack chunk ptr => RET (BA_loadstack chunk ptr)
+  | BA_addrstack ptr => RET (BA_addrstack ptr)
+  | BA_loadglobal chunk id ptr => RET (BA_loadglobal chunk id ptr)
+  | BA_addrglobal id ptr => RET (BA_addrglobal id ptr)
   | BA_splitlong ba1 ba2 => 
     DO v1 <~ hbuiltin_arg hst ba1;;
     DO v2 <~ hbuiltin_arg hst ba2;;
@@ -557,218 +557,87 @@ Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse
   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 =>
-      match lhse2 with
-      | nil => OK tt
-      | _ => Error (msg "siexists_simub: sle1 and sle2 lengths do not match")
-      end
-  | hse1 :: lhse1 =>
-      match lhse2 with
-      | nil => Error (msg "siexits_simub: sle1 and sle2 lengths do not match")
-      | hse2 :: lhse2 =>
-          do _ <- hsiexit_simub dm f hse1 hse2;
-          do _ <- hsiexits_simub dm f lhse1 lhse2;
-          OK tt
-      end
-  end.
-
-Definition hsistate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
-  do _ <- hsilocal_simub dm f (hsi_local hst1) (hsi_local hst2);
-  do _ <- hsiexits_simub dm f (hsi_exits hst1) (hsi_exits hst2);
-  OK tt.
-
-Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): res unit :=
-  match ln with
-  | nil =>
-      match ln' with
-      | nil => OK tt
-      | _ => Error (msg "revmap_check_list: lists have different lengths")
-      end
-  | n::ln =>
-      match ln' with
-      | nil => Error (msg "revmap_check_list: lists have different lengths")
-      | n'::ln' => do _ <- revmap_check_single dm n n'; revmap_check_list dm ln ln'
-      end
-  end.
-
-Definition svos_simub (svos1 svos2: sval + ident) :=
-  match svos1 with
-  | inl sv1 =>
-      match svos2 with
-      | inl sv2 => sval_simub sv1 sv2
-      | _ => Error (msg "svos_simub: expected sval")
-      end
-  | inr id1 =>
-      match svos2 with
-      | inr id2 =>
-          if (ident_eq id1 id2) then OK tt
-          else Error (msg "svos_simub: ids do not match")
-      | _ => Error (msg "svos_simub: expected id")
-      end
-  end.
-
-Fixpoint builtin_arg_simub (bs bs': builtin_arg sval) :=
-  match bs with
-  | BA sv =>
-      match bs' with
-      | BA sv' => sval_simub sv sv'
-      | _ => Error (msg "builtin_arg_simub: BA expected")
-      end
-  | BA_int n =>
-      match bs' with
-      | BA_int n' => if (Integers.int_eq n n') then OK tt else Error (msg "builtin_arg_simub: integers do not match")
-      | _ => Error (msg "buitin_arg_simub: BA_int expected")
-      end
-  | BA_long n =>
-      match bs' with
-      | BA_long n' => if (int64_eq n n') then OK tt else Error (msg "builtin_arg_simub: integers do not match")
-      | _ => Error (msg "buitin_arg_simub: BA_long expected")
-      end
-  | BA_float f =>
-      match bs' with
-      | BA_float f' => if (float_eq f f') then OK tt else Error (msg "builtin_arg_simub: floats do not match")
-      | _ => Error (msg "builtin_arg_simub: BA_float expected")
-      end
-  | BA_single f =>
-      match bs' with
-      | BA_single f' => if (float32_eq f f') then OK tt else Error (msg "builtin_arg_simub: floats do not match")
-      | _ => Error (msg "builtin_arg_simub: BA_single expected")
-      end
-  | BA_loadstack chk ptr =>
-      match bs' with
-      | BA_loadstack chk' ptr' =>
-          if (chunk_eq chk chk') then
-            if (ptrofs_eq ptr ptr') then OK tt
-            else Error (msg "builtin_arg_simub: ptr do not match")
-          else Error (msg "builtin_arg_simub: chunks do not match")
-      | _ => Error (msg "builtin_arg_simub: BA_loadstack expected")
-      end
-  | BA_addrstack ptr =>
-      match bs' with
-      | BA_addrstack ptr' => if (ptrofs_eq ptr ptr') then OK tt else Error (msg "builtin_arg_simub: ptr do not match")
-      | _ => Error (msg "builtin_arg_simub: BA_addrstack expected")
-      end
-  | BA_loadglobal chk id ofs =>
-      match bs' with
-      | BA_loadglobal chk' id' ofs' =>
-          if (chunk_eq chk chk') then
-            if (ident_eq id id') then
-              if (ptrofs_eq ofs ofs') then OK tt
-              else Error (msg "builtin_arg_simub: offsets do not match")
-            else Error (msg "builtin_arg_simub: identifiers do not match")
-          else Error (msg "builtin_arg_simub: chunks do not match")
-      | _ => Error (msg "builtin_arg_simub: BA_loadglobal expected")
-      end
-  | BA_addrglobal id ofs =>
-      match bs' with
-      | BA_addrglobal id' ofs' =>
-          if (ident_eq id id') then
-            if (ptrofs_eq ofs ofs') then OK tt
-            else Error (msg "builtin_arg_simub: offsets do not match")
-          else Error (msg "builtin_arg_simub: identifiers do not match")
-      | _ => Error (msg "builtin_arg_simub: BA_addrglobal expected")
-      end
-  | BA_splitlong lo hi =>
-      match bs' with
-      | BA_splitlong lo' hi' => do _ <- builtin_arg_simub lo lo'; builtin_arg_simub hi hi'
-      | _ => Error (msg "builtin_arg_simub: BA_splitlong expected")
-      end
-  | BA_addptr b1 b2 =>
-      match bs' with
-      | BA_addptr b1' b2' => do _ <- builtin_arg_simub b1 b1'; builtin_arg_simub b2 b2'
-      | _ => Error (msg "builtin_arg_simub: BA_addptr expected")
-      end
-  end.
-
-Fixpoint list_builtin_arg_simub lbs1 lbs2 :=
-  match lbs1 with
-  | nil =>
-      match lbs2 with
-      | nil => OK tt
-      | _ => Error (msg "list_builtin_arg_simub: lists of different lengths (lbs2 is bigger)")
-      end
-  | bs1::lbs1 =>
-      match lbs2 with
-      | nil => Error (msg "list_builtin_arg_simub: lists of different lengths (lbs1 is bigger)")
-      | bs2::lbs2 =>
-          do _ <- builtin_arg_simub bs1 bs2;
-          list_builtin_arg_simub lbs1 lbs2
-      end
-  end.
-
-(* WARNING: ce code va bouger pas mal quand on aura le hash-consing ! *)
-Definition sfval_simub (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: sfval) :=
-  match fv1 with
-  | Snone =>
-      match fv2 with
-      | Snone => revmap_check_single dm pc1 pc2
-      | _ => Error (msg "sfval_simub: Snone expected")
-      end
-  | Scall sig svos lsv res pc1 =>
-      match fv2 with
-      | Scall sig2 svos2 lsv2 res2 pc2 =>
-          do _ <- revmap_check_single dm pc1 pc2;
-          if (signature_eq sig sig2) then
-            if (Pos.eq_dec res res2) then
-              do _ <- svos_simub svos svos2;
-              list_sval_simub lsv lsv2
-            else Error (msg "sfval_simub: Scall res do not match")
-          else Error (msg "sfval_simub: Scall different signatures")
-      | _ => Error (msg "sfval_simub: Scall expected")
-      end
-  | Stailcall sig svos lsv =>
-      match fv2 with
-      | Stailcall sig' svos' lsv' =>
-          if (signature_eq sig sig') then
-            do _ <- svos_simub svos svos';
-            list_sval_simub lsv lsv'
-          else Error (msg "sfval_simub: signatures do not match")
-      | _ => Error (msg "sfval_simub: Stailcall expected")
-      end
-  | Sbuiltin ef lbs br pc =>
-      match fv2 with
-      | Sbuiltin ef' lbs' br' pc' =>
-          if (external_function_eq ef ef') then
-            if (builtin_res_eq_pos br br') then
-              do _ <- revmap_check_single dm pc pc';
-              list_builtin_arg_simub lbs lbs'
-            else Error (msg "sfval_simub: builtin res do not match")
-          else Error (msg "sfval_simub: external functions do not match")
-      | _ => Error (msg "sfval_simub: Sbuiltin expected")
-      end
-  | Sjumptable sv ln =>
-      match fv2 with
-      | Sjumptable sv' ln' =>
-          do _ <- revmap_check_list dm ln ln'; sval_simub sv sv'
-      | _ => Error (msg "sfval_simub: Sjumptable expected")
-      end
-  | Sreturn osv =>
-      match fv2 with
-      | Sreturn osv' =>
-          match osv with
-          | Some sv =>
-              match osv' with
-              | Some sv' => sval_simub sv sv'
-              | None => Error (msg "sfval_simub sv' expected")
-              end
-          | None =>
-              match osv' with
-              | Some sv' => Error (msg "None expected")
-              | None => OK tt
-              end
-          end
-      | _ => Error (msg "sfval_simub: Sreturn expected")
-      end
-  end.
-
-Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
-  do u1 <- hsistate_simub dm f (hinternal hst1) (hinternal hst2);
-  do u2 <- sfval_simub dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2);
-  OK tt.
+Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
+  match lhse1,lhse2 with
+  | nil, nil => RET tt
+  | hse1 :: lhse1, hse2 :: lhse2 =>
+    hsiexit_simu_check dm f hse1 hse2;;
+    hsiexits_simu_check dm f lhse1 lhse2
+  | _, _ => FAILWITH "siexists_simu_check:  lengths do not match"
+  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).
+
+Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
+  match ln, ln' with
+  | nil, nil => RET tt
+  | n::ln, n'::ln' => 
+      revmap_check_single dm n n';;
+      revmap_check_list dm ln ln'
+  | _, _ => FAILWITH "revmap_check_list: lists have different lengths"
+  end.
+
+Definition svos_simu_check (svos1 svos2: hsval + ident) :=
+  match svos1, svos2 with
+  | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch"
+  | inr id1, inr id2 => phys_check id1 id2 "svos_simu_check: symbol mismatch"
+  | _, _ => FAILWITH "svos_simu_check: type mismatch"
+  end.
+
+Fixpoint builtin_arg_simu_check (bs bs': builtin_arg hsval) :=
+  match bs, bs' with
+  | BA sv, BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch"
+  | BA_splitlong lo hi, BA_splitlong lo' hi' => 
+      builtin_arg_simu_check lo lo';;
+      builtin_arg_simu_check hi hi'
+  | BA_addptr b1 b2, BA_addptr b1' b2' => 
+      builtin_arg_simu_check b1 b1';;
+      builtin_arg_simu_check b2 b2'
+  | _, _ => struct_check bs bs' "builtin_arg_simu_check: basic mismatch"
+  end.
+
+Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
+  match lbs1, lbs2 with
+  | nil, nil => RET tt
+  | bs1::lbs1, bs2::lbs2 =>
+    builtin_arg_simu_check bs1 bs2;;
+    list_builtin_arg_simu_check lbs1 lbs2
+  | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch"
+  end.
+
+Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: hsfval) :=
+  match fv1, fv2 with
+  | HSnone, HSnone => revmap_check_single dm pc1 pc2
+  | HScall sig1 svos1 lsv1 res1 pc1, HScall sig2 svos2 lsv2 res2 pc2 =>
+      revmap_check_single dm pc1 pc2;;
+      phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";;
+      phys_check res1 res2 "sfval_simu_check: Scall res do not match";;
+      svos_simu_check svos1 svos2;;
+      phys_check lsv1 lsv2 "sfval_simu_check: Scall args do not match"
+  | HStailcall sig1 svos1 lsv1, HStailcall sig2 svos2 lsv2 =>
+      phys_check sig1 sig2 "sfval_simu_check: Stailcall different signatures";;
+      svos_simu_check svos1 svos2;;
+      phys_check lsv1 lsv2 "sfval_simu_check: Stailcall args do not match"
+  | HSbuiltin ef1 lbs1 br1 pc1, HSbuiltin ef2 lbs2 br2 pc2 =>
+      revmap_check_single dm pc1 pc2;;
+      phys_check ef1 ef2 "sfval_simu_check: builtin ef do not match";;
+      phys_check br1 br2 "sfval_simu_check: builtin br do not match";;
+      list_builtin_arg_simu_check lbs1 lbs2
+  | HSjumptable sv ln, HSjumptable sv' ln' =>
+      revmap_check_list dm ln ln';;
+      phys_check sv sv' "sfval_simu_check: Sjumptable sval do not match"
+  | HSreturn osv1, HSreturn osv2 =>
+      option_eq_check osv1 osv2
+  | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
+  end.
+
+Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
+  hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
+  sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).
 
+(*
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node) :=
   let (pc2, pc1) := m in
   match (hsexec f pc1) with
@@ -776,7 +645,7 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
   | Some hst1 =>
       match (hsexec tf pc2) with
       | None => Error (msg "simu_check_single: hsexec tf pc2 failed")
-      | Some hst2 => hsstate_simub dm f hst1 hst2
+      | Some hst2 => hsstate_simu_check dm f hst1 hst2
       end
   end.