diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rwxr-xr-x | configure | 4 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_impl_junk.v | 758 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v (renamed from kvx/lib/RTLpathSE_simu_specs.v) | 0 |
4 files changed, 2 insertions, 762 deletions
@@ -114,7 +114,7 @@ BACKEND=\ $(BACKENDLIB) SCHEDULING= \ - RTLpathLivegenproof.v RTLpathSE_impl_junk.v \ + RTLpathLivegenproof.v RTLpathSE_simu_specs.v \ RTLpathLivegen.v RTLpathSE_impl.v \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ @@ -847,12 +847,10 @@ EXECUTE=kvx-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __KVX_COS__ SIMU=kvx-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_simu_specs.v RTLpathSE_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ - AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ - ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v + AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v EOF fi diff --git a/scheduling/RTLpathSE_impl_junk.v b/scheduling/RTLpathSE_impl_junk.v deleted file mode 100644 index 652f4ca3..00000000 --- a/scheduling/RTLpathSE_impl_junk.v +++ /dev/null @@ -1,758 +0,0 @@ -(** 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. - -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 *) - -(** ** 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 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. - - -(* 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 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_hSinit op hlsv - | 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 hlsv <~ hlist_args hst lsv;; - hSop_hSinit op hlsv - 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;; - 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; - 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 => - 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 - 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 := - 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);; - 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);; - 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";; - 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) := - 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 - | 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 *) - 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. - -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);; - DEBUG("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.
\ No newline at end of file diff --git a/kvx/lib/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index 0c5ed3b8..0c5ed3b8 100644 --- a/kvx/lib/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v |