path: root/kvx/lib/RTLpathSE_impl_junk.v

(** Implementation and refinement of the symbolic execution

* a JUNK VERSION WITHOUT ANY FORMAL PROOF !!!

 *)

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL RTLpath.
Require Import Errors Duplicate.
Require Import RTLpathSE_theory.
Require Import Axioms.

Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.

Require Export Impure.ImpHCons.
Export Notations.
Import HConsing.

Local Open Scope impure.

Import ListNotations.
Local Open Scope list_scope.

(** * Implementation of Data-structure use in Hash-consing *)

(** ** Implementation of symbolic values/symbolic memories with hash-consing data *)

Inductive hsval :=
  | HSinput (r: reg) (hid:hashcode)
  | HSop (op:operation) (hlsv: hlist_sval)  (hsm: hsmem) (hid:hashcode)
  | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (hid:hashcode)
with hlist_sval := 
  | HSnil (hid:hashcode)
  | HScons (hsv: hsval) (hlsv: hlist_sval) (hid:hashcode)
(* symbolic memory *)
with hsmem :=
  | HSinit (hid:hashcode)
  | HSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval) (hid:hashcode).

Scheme hsval_mut := Induction for hsval Sort Prop
with hlist_sval_mut := Induction for hlist_sval Sort Prop
with hsmem_mut := Induction for hsmem Sort Prop.

Definition hsval_get_hid (hsv: hsval): hashcode :=
  match hsv with
  | HSinput _ hid => hid
  | HSop _ _ _ hid => hid
  | HSload _ _ _ _ _ hid => hid
  end.

Definition hlist_sval_get_hid (hlsv: hlist_sval): hashcode :=
  match hlsv with
  | HSnil hid => hid
  | HScons _ _ hid => hid
  end.

Definition hsmem_get_hid (hsm: hsmem ): hashcode :=
  match hsm with
  | HSinit hid => hid
  | HSstore _ _ _ _ _ hid => hid
  end.

Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval :=
  match hsv with
  | HSinput r _ => HSinput r hid
  | HSop o hlsv hsm _ => HSop o hlsv hsm hid
  | HSload hsm trap chunk addr hlsv _ => HSload hsm trap chunk addr hlsv hid
  end.

Definition hlist_sval_set_hid (hlsv: hlist_sval) (hid: hashcode): hlist_sval :=
  match hlsv with
  | HSnil _ => HSnil hid
  | HScons hsv hlsv _ => HScons hsv hlsv hid
  end.

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
  end.

(* Now, we build the hash-Cons value from a "hash_eq".

Informal specification: 
  [hash_eq] must be consistent with the "hashed" constructors defined above.

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 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.

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.

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.

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.


(* Symbolic final value -- from hash-consed values
It does not seem useful to hash-consed these final values (because they are final).
*)
Inductive hsfval :=
  | HSnone
  | HScall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval) (res:reg) (pc:node)
  | HStailcall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval)
  | HSbuiltin (ef:external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc:node)
  | HSjumptable (sv: hsval) (tbl: list node)
  | HSreturn (res:option hsval)
.

(** ** Implementation of symbolic states 
*)

(** name : Hash-consed Symbolic Internal state local.  *)
Record hsistate_local := 
  { 
    (** [hsi_smem] represents the current smem symbolic evaluations.
        (we can recover the previous one from smem)  *)
    hsi_smem:> hsmem;
    (** For the values in registers:
        1) we store a list of sval evaluations
        2) we encode the symbolic regset by a PTree *)
    hsi_ok_lsval: list hsval;
    hsi_sreg:> PTree.t hsval
  }.

(* Syntax and semantics of symbolic exit states *)
Record hsistate_exit := mk_hsistate_exit
  { hsi_cond: condition; hsi_scondargs: hlist_sval; hsi_elocal: hsistate_local; hsi_ifso: node }.


(** ** Syntax and Semantics of symbolic internal state *)
Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }.

(** ** Syntax and Semantics of symbolic state *)
Record hsstate := { hinternal:> hsistate; hfinal: hsfval }.


(** * Implementation of symbolic execution *)
Section CanonBuilding.

Variable hC_hsval: hashinfo hsval -> ?? hsval.
(*Hypothesis hC_hsval_correct: TODO *)

Variable hC_hlist_sval: hashinfo hlist_sval -> ?? hlist_sval.
(*Hypothesis hC_hlist_sval_correct: TODO *)

Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.
(*Hypothesis hC_hsval_correct: TODO *)

(* First, we wrap constructors for hashed values !*)

Definition hSinput_hcodes (r: reg) :=
   DO hc <~ hash 1;;
   DO hv <~ hash r;;
   RET [hc;hv].
Extraction Inline hSinput_hcodes.

Definition hSinput (r:reg): ?? hsval :=
   DO hv <~ hSinput_hcodes r;;
   hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}.


Definition hSop_hcodes (op:operation) (hlsv: hlist_sval)  (hsm: hsmem) :=
   DO hc <~ hash 2;;
   DO hv <~ hash op;;
   RET [hc;hv;hlist_sval_get_hid hlsv; hsmem_get_hid hsm].
Extraction Inline hSop_hcodes.

Definition hSop (op:operation) (hlsv: hlist_sval)  (hsm: hsmem): ?? hsval :=
   DO hv <~ hSop_hcodes op hlsv hsm;;
   hC_hsval {| hdata:=HSop op hlsv hsm unknown_hid; hcodes :=hv |}.


Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval):=
   DO hc <~ hash 3;;
   DO hv1 <~ hash trap;;
   DO hv2 <~ hash chunk;;
   DO hv3 <~ hash addr;;
   RET [hc;hsmem_get_hid hsm;hv1;hv2;hv3;hlist_sval_get_hid hlsv].
Extraction Inline hSload_hcodes.

Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval): ?? hsval :=
   DO hv <~ hSload_hcodes hsm trap chunk addr hlsv;;
   hC_hsval {| hdata:=HSload hsm trap chunk addr hlsv unknown_hid; hcodes :=hv |}.


Definition hSnil (_: unit): ?? hlist_sval :=
   hC_hlist_sval {| hdata:=HSnil unknown_hid; hcodes := nil |}.

Definition hScons (hsv: hsval) (hlsv: hlist_sval): ?? hlist_sval :=
   hC_hlist_sval {| hdata:=HScons hsv hlsv unknown_hid; hcodes := [hsval_get_hid hsv; hlist_sval_get_hid hlsv] |}.

Definition hSinit (_: unit): ?? hsmem :=
   hC_hsmem {| hdata:=HSinit unknown_hid; hcodes := nil |}.

Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval):=
   DO hv1 <~ hash chunk;;
   DO hv2 <~ hash addr;;
   RET [hsmem_get_hid hsm;hv1;hv2;hlist_sval_get_hid hlsv;hsval_get_hid srce].
Extraction Inline hSstore_hcodes.

Definition hSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval): ?? hsmem :=
   DO hv <~ hSstore_hcodes hsm chunk addr hlsv srce;;
   hC_hsmem {| hdata:=HSstore hsm chunk addr hlsv srce unknown_hid; hcodes := hv |}.


Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
   match PTree.get r hst with 
   | None => hSinput r
   | Some sv => RET sv
   end.

Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? hlist_sval :=
  match l with
  | nil => hSnil()
  | r::l =>
    DO v <~ hsi_sreg_get hst r;;
    DO hlsv <~ hlist_args hst l;;
    hScons v hlsv
  end.

(** ** Assignment of memory *)
Definition hslocal_store (hst:hsistate_local) chunk addr args src: ?? hsistate_local :=
   let pt := hst.(hsi_sreg) in
   DO hargs <~ hlist_args pt args;;
   DO hsrc <~ hsi_sreg_get pt src;;
   DO hm <~ hSstore hst chunk addr hargs hsrc;;
   RET {| hsi_smem := hm;
         hsi_ok_lsval := hsi_ok_lsval hst;
         hsi_sreg:= hsi_sreg hst
       |}.

(** ** Assignment of local state *)

Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hsistate :=
   {| hsi_pc := pc; hsi_exits := hst.(hsi_exits); hsi_local:= hnxt |}.

(** ** Assignment of registers *)

(* locally new symbolic values during symbolic execution *)
Inductive root_sval: Type :=
| Rop (op:operation)
| Rload (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing)
.

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
  | Rload trap chunk addr => hSload hst trap chunk addr hlsv
  end.

Local Open Scope lazy_bool_scope.

(* NB: return [false] if the rsv cannot fail *)
Definition may_trap (rsv: root_sval) (lsv: list reg): bool :=
  match rsv with 
  | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lsv) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
  | Rload TRAP _ _  => true
  | _ => false
  end.

(* simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lsv: list reg) (hst: hsistate_local): ?? hsval :=
  match rsv with
  | Rop op =>
     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 ! *)
     end
  | Rload _ chunk addr => 
       DO hlsv <~ hlist_args hst lsv;;
       hSload hst NOTRAP chunk addr hlsv
  end.

Definition red_PTree_set (r:reg) (sv: hsval) (hst: PTree.t hsval): PTree.t hsval :=
  match sv with
  | HSinput r' _ =>
     if Pos.eq_dec r r' 
     then PTree.remove r' hst
     else PTree.set r sv hst
  | _ => PTree.set r sv hst
  end.

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))
    else RET (hsi_ok_lsval hst));;
  DO simp <~ simplify rsv lsv hst;;
  RET {| hsi_smem := hst;
         hsi_ok_lsval := hsiok;
         hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}.

(** ** Execution of one instruction *)

Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := 
  match i with
  | Inop pc' => 
      RET (Some (hsist_set_local hst pc' hst.(hsi_local)))
  | Iop op args dst pc' =>
      DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rop op) args;;
      RET (Some (hsist_set_local hst pc' next))
  | Iload trap chunk addr args dst pc' =>
      DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rload trap chunk addr) args;;
      RET (Some (hsist_set_local hst pc' next))
  | Istore chunk addr args src pc' =>
      DO next <~ hslocal_store hst.(hsi_local) chunk addr args src;;
      RET (Some (hsist_set_local hst pc' next))
  | Icond cond args ifso ifnot _ =>
      let prev := hst.(hsi_local) in
      DO vargs <~ hlist_args prev args ;;
      let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
      RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |})
  | _ => RET None (* TODO jumptable ? *)
  end.

Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
  match o with
  | Some x => RET x
  | None => FAILWITH msg
  end.

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";;
    DO ohst1 <~ hsiexec_inst i hst;;
    DO hst1 <~ some_or_fail ohst1 "hsiexec_path.internal_error.2";;
    hsiexec_path p f hst1
  end.

Fixpoint hbuiltin_arg (hst: PTree.t hsval) (arg : builtin_arg reg): ?? builtin_arg hsval := 
  match arg with
  | BA r => 
         DO v <~ hsi_sreg_get hst r;;
         RET (BA v)
  | 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;;
    RET (BA_splitlong v1 v2)
  | BA_addptr ba1 ba2 => 
    DO v1 <~ hbuiltin_arg hst ba1;;
    DO v2 <~ hbuiltin_arg hst ba2;;
    RET (BA_addptr v1 v2)
  end.

Fixpoint hbuiltin_args (hst: PTree.t hsval) (args: list (builtin_arg reg)): ?? list (builtin_arg hsval) :=
  match args with
  | nil => RET nil
  | a::l =>
    DO ha <~ hbuiltin_arg hst a;;
    DO hl <~ hbuiltin_args hst l;;
    RET (ha::hl)
    end.

Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident) :=
  match ros with
  | inl r => DO hr <~ hsi_sreg_get hst r;; RET (inl hr) 
  | inr s => RET (inr s)
  end.

Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := 
  match i with
  | Icall sig ros args res pc => 
    DO svos <~ hsum_left hst ros;;
    DO sargs <~ hlist_args hst args;;
    RET (HScall sig svos sargs res pc)
  | Itailcall sig ros args =>
    DO svos <~ hsum_left hst ros;;
    DO sargs <~ hlist_args hst args;;
    RET (HStailcall sig svos sargs)
  | Ibuiltin ef args res pc =>
    DO sargs <~ hbuiltin_args hst args;;
    RET (HSbuiltin ef sargs res pc)
  | Ijumptable reg tbl =>
    DO sv <~ hsi_sreg_get hst reg;;
    RET (HSjumptable sv tbl)
  | Ireturn or => 
    match or with
    | Some r => DO hr <~ hsi_sreg_get hst r;; RET (HSreturn (Some hr))
    | None => RET (HSreturn None)
    end
  | _ => RET (HSnone)
  end.

Definition init_hsistate_local (_:unit): ?? hsistate_local
  := DO hm <~ hSinit ();;
     RET {| hsi_smem := hm; hsi_ok_lsval := nil; hsi_sreg := PTree.empty hsval |}.

Definition init_hsistate pc: ?? hsistate 
  := DO hst <~ init_hsistate_local ();;
     RET {| hsi_pc := pc; hsi_exits := nil; hsi_local := hst |}.

Definition hsexec (f: function) (pc:node): ?? hsstate :=
  DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";;
  DO hinit <~ init_hsistate pc;;
  DO hst <~ hsiexec_path path.(psize) f hinit;;
  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
  DO ohst <~ hsiexec_inst i hst;;
  match ohst with
  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
            RET {| hinternal := hst; hfinal := hsvf |}
  end.

End CanonBuilding.

(** * The simulation test of concrete hash-consed symbolic execution *)

Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
  DO b <~ phys_eq x y;;
  assert_b b msg;;
  RET tt.

Definition struct_check {A} (x y:A) (msg: pstring): ?? unit :=
  DO b <~ struct_eq x y;;
  assert_b b msg;;
  RET tt.

Definition option_eq_check {A} (o1 o2: option A): ?? unit :=
  match o1, o2 with
  | Some x1, Some x2 => phys_check x1 x2 "option_eq_check: data physically differ"
  | None, None => RET tt
  | _, _ => FAILWITH "option_eq_check: structure differs"
  end.

Lemma option_eq_check_correct A (o1 o2: option A): WHEN option_eq_check o1 o2 ~> _ THEN o1=o2.
Proof.
  wlp_simplify.
Qed.
Global Opaque option_eq_check.
Global Hint Resolve option_eq_check_correct:wlp.

Import PTree.

Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
  match d1, d2 with
  | Leaf, Leaf => RET tt
  | Node l1 o1 r1, Node l2 o2 r2 =>
      option_eq_check o1 o2;;
      PTree_eq_check l1 l2;;
      PTree_eq_check r1 r2
  | _, _ => FAILWITH "PTree_eq_check: some key is absent"
  end.

Lemma PTree_eq_check_correct A d1: forall (d2: t A),
 WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2.
Proof.
  induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; 
  wlp_simplify. destruct x; simpl; auto.
Qed.
Global Opaque PTree_eq_check.

Fixpoint PTree_frame_eq_check {A} (frame: list positive) (d1 d2: PTree.t A): ?? unit :=
  match frame with
  | nil => RET tt
  | k::l => 
    option_eq_check (PTree.get k d1) (PTree.get k d2);;
    PTree_frame_eq_check l d1 d2
  end.

Lemma PTree_frame_eq_check_correct A l (d1 d2: t A):
 WHEN PTree_frame_eq_check l d1 d2 ~> _ THEN forall x, List.In x l -> PTree.get x d1 = PTree.get x d2.
Proof.
  induction l as [|k l]; simpl; wlp_simplify.
  subst; auto.
Qed.
Global Opaque PTree_frame_eq_check.

Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2).

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 :=
  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
  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).

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";;
  phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";;
  revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2);;
  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_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): ?? unit :=
  let (pc2, pc1) := m in
  (* creating the hash-consing tables *)
  DO hC_sval <~ hCons hSVAL;;
  DO hC_hlist_sval <~ hCons hLSVAL;;
  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 hst1 <~ hsexec f pc1;;
  DO hst2 <~ hsexec tf pc2;;
  (* comparing the executions *)
  hsstate_simu_check dm f hst1 hst2.

Lemma simu_check_single_correct dm tf f pc1 pc2:
  WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
  sexec_simu dm f tf pc1 pc2.
Admitted.
Global Opaque simu_check_single.
Global Hint Resolve simu_check_single_correct: wlp.

Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm : ?? unit :=
  match lm with
  | nil => RET tt
  | m :: lm => 
    simu_check_single dm f tf m;;
    simu_check_rec dm f tf lm
  end.

Lemma simu_check_rec_correct dm f tf lm:
  WHEN simu_check_rec dm f tf lm ~> _ THEN
  forall pc1 pc2, In (pc2, pc1) lm -> sexec_simu dm f tf pc1 pc2.
Proof.
  induction lm; wlp_simplify.
  match goal with
  | X: (_,_) = (_,_) |- _ => inversion X; subst
  end.
  subst; eauto.
Qed.
Global Opaque simu_check_rec.
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!").

Local Hint Resolve PTree.elements_correct: core.
Lemma imp_simu_check_correct dm f tf:
  WHEN imp_simu_check dm f tf ~> _ THEN
  forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2.
Proof.
  wlp_simplify.
Qed.
Global Opaque imp_simu_check.
Global Hint Resolve imp_simu_check_correct: wlp.

Program Definition aux_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? bool :=
   DO r <~ 
     (TRY 
       imp_simu_check dm f tf;; 
       RET true
      CATCH_FAIL 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).
Obligation 1.
  split; wlp_simplify. discriminate.
Qed.

Lemma aux_simu_check_correct dm f tf:
  WHEN aux_simu_check dm f tf ~> b THEN
  b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2.
Proof.
  unfold aux_simu_check; wlp_simplify.
  destruct exta; simpl; auto.
Qed.

(* Coerce aux_simu_check into a pure function (this is a little unsafe like all oracles in CompCert). *)

Import UnsafeImpure.

Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) : res unit := 
  match unsafe_coerce (aux_simu_check dm f tf) with
  | Some true => OK tt
  | _ => Error (msg "simu_check has failed")
  end.

Lemma simu_check_correct dm f tf:
  simu_check dm f tf = OK tt ->
  forall pc1 pc2, dm ! pc2 = Some pc1 ->
  sexec_simu dm f tf pc1 pc2.
Proof.
  unfold simu_check.
  destruct (unsafe_coerce (aux_simu_check dm f tf)) as [[|]|] eqn:Hres; simpl; try discriminate.
  intros; eapply aux_simu_check_correct; eauto.
  eapply unsafe_coerce_not_really_correct; eauto.
Qed.