diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 589 | ||||
| -rw-r--r-- | kvx/lib/RTLpathScheduler.v | 2 |
3 files changed, 591 insertions, 2 deletions
@@ -845,7 +845,7 @@ 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_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ + RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_impl_junk.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\\ diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v new file mode 100644 index 00000000..8ae21a2d --- /dev/null +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -0,0 +1,589 @@ +(** 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. + + +(* +(** * TODO: refine symbolic values/symbolic memories with hash-consed symbolic values *) + +(** * Implementation of local symbolic internal states +TODO: use refined symbolic values instead of those from RTLpathSE_theory. +*) + +(** name : Hash-consed Symbolic Internal state local. Later on we will use the + refinement to introduce hash consing *) +Record hsistate_local := + { + (** [hsi_lsmem] represents the list of smem symbolic evaluations. + The first one of the list is the current smem *) + hsi_lsmem:> list smem; + (** 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 sval; + hsi_sreg:> PTree.t sval + }. + +Definition hsi_sreg_get (hst: PTree.t sval) r: sval := + match PTree.get r hst with + | None => Sinput r + | Some sv => sv + end. + + +Definition hsi_smem_get (hst: list smem): smem := + match hst with + | nil => Sinit + | sm::_ => sm + end. + +(* Syntax and semantics of symbolic exit states *) +(* TODO: add hash-consing *) +Record hsistate_exit := mk_hsistate_exit + { hsi_cond: condition; hsi_scondargs: list_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 }. + +(** ** Assignment of memory *) +Definition hslocal_set_smem (hst:hsistate_local) (sm:smem) := + {| hsi_lsmem := sm::hsi_lsmem hst; + 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 sval) (sm: smem): sval := + match rsv with + | Rop op => Sop op (list_sval_inj lsv) sm + | Rload trap chunk addr => Sload sm trap chunk addr (list_sval_inj lsv) + end. +Coercion root_apply: root_sval >-> Funclass. + +Local Open Scope lazy_bool_scope. + +(* NB: return [false] if the rsv cannot fail *) +Definition may_trap (rsv: root_sval) (lsv: list sval) (sm: smem): 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 sm: sval := + match rsv with + | Rload TRAP chunk addr => Sload sm NOTRAP chunk addr (list_sval_inj lsv) + | Rop op => + match is_move_operation op lsv with + | Some arg => arg (* optimization of Omove *) + | None => + if op_depends_on_memory op then + rsv lsv sm + else + Sop op (list_sval_inj lsv) Sinit (* magically remove the dependency on sm ! *) + end + | _ => rsv lsv sm + end. + +Definition red_PTree_set (r:reg) (sv: sval) (hst: PTree.t sval): PTree.t sval := + match sv with + | Sinput 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 sm := + {| hsi_lsmem := hsi_lsmem hst; + hsi_ok_lsval := if may_trap rsv lsv sm then (rsv lsv sm)::(hsi_ok_lsval hst) else hsi_ok_lsval hst; + hsi_sreg := red_PTree_set r (simplify rsv lsv sm) (hsi_sreg hst) |}. + +(** ** Execution of one instruction *) + +Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate := + match i with + | Inop pc' => + Some (hsist_set_local hst pc' hst.(hsi_local)) + | Iop op args dst pc' => + let prev := hst.(hsi_local) in + let vargs := List.map (hsi_sreg_get prev) args in + let next := hslocal_set_sreg prev dst (Rop op) vargs (hsi_smem_get prev) in + Some (hsist_set_local hst pc' next) + | Iload trap chunk addr args dst pc' => + let prev := hst.(hsi_local) in + let vargs := List.map (hsi_sreg_get prev) args in + let next := hslocal_set_sreg prev dst (Rload trap chunk addr) vargs (hsi_smem_get prev) in + Some (hsist_set_local hst pc' next) + | Istore chunk addr args src pc' => + let prev := hst.(hsi_local) in + let vargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in + let next := hslocal_set_smem prev (Sstore (hsi_smem_get prev) chunk addr vargs (hsi_sreg_get prev src)) in + Some (hsist_set_local hst pc' next) + | Icond cond args ifso ifnot _ => + let prev := hst.(hsi_local) in + let vargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in + let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in + Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |} + | _ => None (* TODO jumptable ? *) + end. + +Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate := + match path with + | O => Some hst + | S p => + SOME i <- (fn_code f)!(hst.(hsi_pc)) IN + SOME hst1 <- hsiexec_inst i hst IN + hsiexec_path p f hst1 + end. + +(* Definition hfinal_refines hfv fv := forall pge ge sp npc stk f rs0 m0 rs' m' t s', + ssem_final pge ge sp npc stk f rs0 m0 hfv rs' m' t s' <-> ssem_final pge ge sp npc stk f rs0 m0 fv rs' m' t s'. *) + +(* FIXME - too strong let's change it later.. *) +Definition hfinal_refines (hfv fv: sfval) := hfv = fv. + +Record hsstate := { hinternal:> hsistate; hfinal: sfval }. + +Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := + match i with + | Icall sig ros args res pc => + let svos := sum_left_map (hsi_sreg_get prev) ros in + let sargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in + Scall sig svos sargs res pc + | Itailcall sig ros args => + let svos := sum_left_map (hsi_sreg_get prev) ros in + let sargs := list_sval_inj (List.map (hsi_sreg_get prev) args) in + Stailcall sig svos sargs + | Ibuiltin ef args res pc => + let sargs := List.map (builtin_arg_inj (hsi_sreg_get prev)) args in + Sbuiltin ef sargs res pc + | Ireturn or => + let sor := SOME r <- or IN Some (hsi_sreg_get prev r) in + Sreturn sor + | Ijumptable reg tbl => + let sv := hsi_sreg_get prev reg in + Sjumptable sv tbl + | _ => Snone + end. + +Definition init_hsistate_local := {| hsi_lsmem := Sinit::nil; hsi_ok_lsval := nil; hsi_sreg := PTree.empty sval |}. + +Definition init_hsistate pc := {| hsi_pc := pc; hsi_exits := nil; hsi_local := init_hsistate_local |}. + +Definition hsexec (f: function) (pc:node): option hsstate := + SOME path <- (fn_path f)!pc IN + SOME hst <- hsiexec_path path.(psize) f (init_hsistate pc) IN + SOME i <- (fn_code f)!(hst.(hsi_pc)) IN + Some (match hsiexec_inst i hst with + | Some hst' => {| hinternal := hst'; hfinal := Snone |} + | None => {| hinternal := hst; hfinal := hsexec_final i hst.(hsi_local) |} + end). + +(** * The simulation test of concrete symbolic execution *) + +(* TODO - generalize it with a list of registers to test ? *) +Definition hsilocal_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate_local) := OK tt. + +Definition revmap_check_single (dm: PTree.t node) (n tn: node) : res unit := + match dm ! tn with + | None => Error (msg "revmap_check_single: no mapping for tn") + | Some res => if (Pos.eq_dec n res) then OK tt + else Error (msg "revmap_check_single: n and res do not match") + end. + +(* WARNING: ce code va bouger pas mal quand on aura le hash-consing ! *) +Fixpoint sval_simub (sv1 sv2: sval) := + match sv1 with + | Sinput r => + match sv2 with + | Sinput r' => if (Pos.eq_dec r r') then OK tt else Error (msg "sval_simub: Sinput different registers") + | _ => Error (msg "sval_simub: Sinput expected") + end + | Sop op lsv sm => + match sv2 with + | Sop op' lsv' sm' => + if (eq_operation op op') then + do _ <- list_sval_simub lsv lsv'; + smem_simub sm sm' + else Error (msg "sval_simub: different operations in Sop") + | _ => Error (msg "sval_simub: Sop expected") + end + | Sload sm trap chk addr lsv => + match sv2 with + | Sload sm' trap' chk' addr' lsv' => + if (trapping_mode_eq trap trap') then + if (chunk_eq chk chk') then + if (eq_addressing addr addr') then + do _ <- smem_simub sm sm'; + list_sval_simub lsv lsv' + else Error (msg "sval_simub: addressings do not match") + else Error (msg "sval_simub: chunks do not match") + else Error (msg "sval_simub: trapping modes do not match") + (* FIXME - should be refined once we introduce non trapping loads *) + | _ => Error (msg "sval_simub: Sload expected") + end + end +with list_sval_simub (lsv1 lsv2: list_sval) := + match lsv1 with + | Snil => + match lsv2 with + | Snil => OK tt + | _ => Error (msg "list_sval_simub: lists of different lengths (lsv2 is bigger)") + end + | Scons sv1 lsv1 => + match lsv2 with + | Snil => Error (msg "list_sval_simub: lists of different lengths (lsv1 is bigger)") + | Scons sv2 lsv2 => + do _ <- sval_simub sv1 sv2; + list_sval_simub lsv1 lsv2 + end + end +with smem_simub (sm1 sm2: smem) := + match sm1 with + | Sinit => + match sm2 with + | Sinit => OK tt + | _ => Error (msg "smem_simub: Sinit expected") + end + | Sstore sm chk addr lsv sv => + match sm2 with + | Sstore sm' chk' addr' lsv' sv' => + if (chunk_eq chk chk') then + if (eq_addressing addr addr') then + do _ <- smem_simub sm sm'; + do _ <- list_sval_simub lsv lsv'; + sval_simub sv sv' + else Error (msg "smem_simub: addressings do not match") + else Error (msg "smem_simub: chunks not match") + | _ => Error (msg "smem_simub: Sstore expected") + end + end. + +Lemma sval_simub_correct sv1: forall sv2, + sval_simub sv1 sv2 = OK tt -> sv1 = sv2. +Proof. + induction sv1 using sval_mut with + (P0 := fun lsv1 => forall lsv2, list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2) + (P1 := fun sm1 => forall sm2, smem_simub sm1 sm2 = OK tt -> sm1 = sm2); simpl; auto. + (* Sinput *) + - destruct sv2; try discriminate. + destruct (Pos.eq_dec r r0); [congruence|discriminate]. + (* Sop *) + - destruct sv2; try discriminate. + destruct (eq_operation _ _); [|discriminate]. subst. + intro. explore. apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence. + (* Sload *) + - destruct sv2; try discriminate. + destruct (trapping_mode_eq _ _); [|discriminate]. + destruct (chunk_eq _ _); [|discriminate]. + destruct (eq_addressing _ _); [|discriminate]. + intro. explore. assert (sm = sm0) by auto. assert (lsv = lsv0) by auto. + congruence. + (* Snil *) + - destruct lsv2; [|discriminate]. congruence. + (* Scons *) + - destruct lsv2; [discriminate|]. intro. explore. + apply IHsv1 in EQ. apply IHsv0 in EQ0. congruence. + (* Sinit *) + - destruct sm2; [|discriminate]. congruence. + (* Sstore *) + - destruct sm2; [discriminate|]. + destruct (chunk_eq _ _); [|discriminate]. + destruct (eq_addressing _ _); [|discriminate]. + intro. explore. + assert (sm = sm2) by auto. assert (lsv = lsv0) by auto. assert (sv1 = srce) by auto. + congruence. +Qed. + +Lemma list_sval_simub_correct lsv1: forall lsv2, + list_sval_simub lsv1 lsv2 = OK tt -> lsv1 = lsv2. +Proof. + induction lsv1; simpl; auto. + - destruct lsv2; try discriminate. reflexivity. + - destruct lsv2; try discriminate. intro. explore. + apply sval_simub_correct in EQ. assert (lsv1 = lsv2) by auto. + congruence. +Qed. + +Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) := + if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then + do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2); + do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2); + revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2) + else Error (msg "siexit_simub: conditions do not match") +. + +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. + +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 + | None => Error (msg "simu_check_single: hsexec f pc1 failed") + | 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 + end + end. + +Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm := + match lm with + | nil => OK tt + | m :: lm => do u1 <- simu_check_single dm f tf m; + do u2 <- simu_check_rec dm f tf lm; + OK tt + end. + +Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) := + simu_check_rec dm f tf (PTree.elements dm). +*) + + +Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) := OK tt. + +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. +Admitted.
\ No newline at end of file diff --git a/kvx/lib/RTLpathScheduler.v b/kvx/lib/RTLpathScheduler.v index 5a1c7f1c..b70c1685 100644 --- a/kvx/lib/RTLpathScheduler.v +++ b/kvx/lib/RTLpathScheduler.v @@ -6,7 +6,7 @@ This module is inspired from [Duplicate] and [Duplicateproof] Require Import AST Linking Values Maps Globalenvs Smallstep Registers. Require Import Coqlib Maps Events Errors Op. -Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl. +Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl_junk. Notation "'ASSERT' A 'WITH' MSG 'IN' B" := (if A then B else Error (msg MSG)) |