diff options
Diffstat (limited to 'kvx/lib/RTLpathSE_theory.v')
| -rw-r--r-- | kvx/lib/RTLpathSE_theory.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v index 22b471fd..dd0b706e 100644 --- a/kvx/lib/RTLpathSE_theory.v +++ b/kvx/lib/RTLpathSE_theory.v @@ -469,6 +469,11 @@ Definition slocal_set_smem (st:sistate_local) (sm:smem) := Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): sistate := {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}. +Definition slocal_store st chunk addr args src : sistate_local := + let args := list_sval_inj (List.map (si_sreg st) args) in + let src := si_sreg st src in + let sm := Sstore (si_smem st) chunk addr args src + in slocal_set_smem st sm. Definition siexec_inst (i: instruction) (st: sistate): option sistate := match i with @@ -485,9 +490,7 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate := let next := slocal_set_sreg prev dst (Sload prev.(si_smem) trap chunk addr vargs) in Some (sist_set_local st pc' next) | Istore chunk addr args src pc' => - let prev := st.(si_local) in - let vargs := list_sval_inj (List.map prev.(si_sreg) args) in - let next := slocal_set_smem prev (Sstore prev.(si_smem) chunk addr vargs (prev.(si_sreg) src)) in + let next := slocal_store st.(si_local) chunk addr args src in Some (sist_set_local st pc' next) | Icond cond args ifso ifnot _ => let prev := st.(si_local) in @@ -497,7 +500,6 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate := | _ => None (* TODO jumptable ? *) end. - Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: (forall r : reg, seval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> seval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l). |