aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/Allocation.v2
-rw-r--r--backend/Allocproof.v8
-rw-r--r--backend/CSE.v6
-rw-r--r--backend/Constprop.v4
-rw-r--r--backend/Deadcode.v4
-rw-r--r--backend/Inlining.v4
-rw-r--r--backend/Inliningspec.v6
-rw-r--r--backend/Liveness.v2
-rw-r--r--backend/RTL.v40
-rw-r--r--backend/RTLgen.v2
-rw-r--r--backend/RTLgenspec.v2
-rw-r--r--backend/RTLtyping.v12
-rw-r--r--backend/Renumber.v2
-rw-r--r--backend/Renumberproof.v12
-rw-r--r--backend/Tailcallproof.v13
-rw-r--r--backend/Unusedglob.v2
-rw-r--r--backend/Unusedglobproof.v32
-rw-r--r--backend/ValueAnalysis.v2
-rw-r--r--mppa_k1c/Op.v39
19 files changed, 153 insertions, 41 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 13e14530..c2e80f1c 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -226,7 +226,7 @@ Definition pair_instr_block
| operation_other _ _ =>
pair_Iop_block op args res s b
end
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
let (mv1, b1) := extract_moves nil b in
match b1 with
| Lload chunk' addr' args' dst' :: b2 =>
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 1804f46b..ac4122bc 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -96,10 +96,10 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr
expand_block_shape (BSopdead op args res mv s)
(Iop op args res s)
(expand_moves mv (Lbranch s :: k))
- | ebs_load: forall chunk addr args dst mv1 args' dst' mv2 s k,
+ | ebs_load: forall trap chunk addr args dst mv1 args' dst' mv2 s k,
wf_moves mv1 -> wf_moves mv2 ->
expand_block_shape (BSload chunk addr args dst mv1 args' dst' mv2 s)
- (Iload chunk addr args dst s)
+ (Iload trap chunk addr args dst s)
(expand_moves mv1
(Lload chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k)))
| ebs_load2: forall addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k,
@@ -130,10 +130,10 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr
(expand_moves mv1
(Lload Mint32 addr2 args' dst' ::
expand_moves mv2 (Lbranch s :: k)))
- | ebs_load_dead: forall chunk addr args dst mv s k,
+ | ebs_load_dead: forall trap chunk addr args dst mv s k,
wf_moves mv ->
expand_block_shape (BSloaddead chunk addr args dst mv s)
- (Iload chunk addr args dst s)
+ (Iload trap chunk addr args dst s)
(expand_moves mv (Lbranch s :: k))
| ebs_store: forall chunk addr args src mv1 args' src' s k,
wf_moves mv1 ->
diff --git a/backend/CSE.v b/backend/CSE.v
index 6d3f6f33..aaaf492c 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -459,7 +459,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
before
| Iop op args res s =>
add_op before res op args
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
add_load before dst chunk addr args
| Istore chunk addr args src s =>
let app := approx!!pc in
@@ -529,14 +529,14 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
let (op', args') := reduce _ combine_op n1 op args vl in
Iop op' args' res s
end
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
let (n1, vl) := valnum_regs n args in
match find_rhs n1 (Load chunk addr vl) with
| Some r =>
Iop Omove (r :: nil) dst s
| None =>
let (addr', args') := reduce _ combine_addr n1 addr args vl in
- Iload chunk addr' args' dst s
+ Iload trap chunk addr' args' dst s
end
| Istore chunk addr args src s =>
let (n1, vl) := valnum_regs n args in
diff --git a/backend/Constprop.v b/backend/Constprop.v
index d8211ffe..b68f4cae 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -157,7 +157,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
let (op', args') := op_strength_reduction op args aargs in
Iop op' args' res s'
end
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
let aargs := aregs ae args in
let a := ValueDomain.loadv chunk rm am (eval_static_addressing addr aargs) in
match const_for_result a with
@@ -165,7 +165,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
Iop cop nil dst s
| None =>
let (addr', args') := addr_strength_reduction addr args aargs in
- Iload chunk addr' args' dst s
+ Iload trap chunk addr' args' dst s
end
| Istore chunk addr args src s =>
let aargs := aregs ae args in
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 2286876e..1f208a91 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -123,7 +123,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t)
if is_dead nres then after
else if is_int_zero nres then (kill res ne, nm)
else (add_needs args (needs_of_operation op nres) (kill res ne), nm)
- | Some (Iload chunk addr args dst s) =>
+ | Some (Iload trap chunk addr args dst s) =>
let ndst := nreg ne dst in
if is_dead ndst then after
else if is_int_zero ndst then (kill dst ne, nm)
@@ -175,7 +175,7 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t)
end
else
instr
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
let ndst := nreg (fst an!!pc) dst in
if is_dead ndst then
Inop s
diff --git a/backend/Inlining.v b/backend/Inlining.v
index f7ee4166..9cf535b9 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -364,9 +364,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit :=
| Iop op args res s =>
set_instr (spc ctx pc)
(Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s))
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
set_instr (spc ctx pc)
- (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s))
+ (Iload trap chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s))
| Istore chunk addr args src s =>
set_instr (spc ctx pc)
(Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s))
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index c345c942..e20fb373 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -270,10 +270,10 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop :=
Ple res ctx.(mreg) ->
c!(spc ctx pc) = Some (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
tr_instr ctx pc (Iop op args res s) c
- | tr_load: forall ctx pc c chunk addr args res s,
+ | tr_load: forall ctx pc c trap chunk addr args res s,
Ple res ctx.(mreg) ->
- c!(spc ctx pc) = Some (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
- tr_instr ctx pc (Iload chunk addr args res s) c
+ c!(spc ctx pc) = Some (Iload trap chunk (saddr ctx addr) (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
+ tr_instr ctx pc (Iload trap chunk addr args res s) c
| tr_store: forall ctx pc c chunk addr args src s,
c!(spc ctx pc) = Some (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s)) ->
tr_instr ctx pc (Istore chunk addr args src s) c
diff --git a/backend/Liveness.v b/backend/Liveness.v
index 16533158..afe11ae6 100644
--- a/backend/Liveness.v
+++ b/backend/Liveness.v
@@ -79,7 +79,7 @@ Definition transfer
reg_list_live args (reg_dead res after)
else
after
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
if Regset.mem dst after then
reg_list_live args (reg_dead dst after)
else
diff --git a/backend/RTL.v b/backend/RTL.v
index 9599a24a..d09cca77 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -36,6 +36,8 @@ Require Import Op Registers.
Definition node := positive.
+Inductive trapping_mode : Type := TRAP | NOTRAP.
+
Inductive instruction: Type :=
| Inop: node -> instruction
(** No operation -- just branch to the successor. *)
@@ -43,11 +45,12 @@ Inductive instruction: Type :=
(** [Iop op args dest succ] performs the arithmetic operation [op]
over the values of registers [args], stores the result in [dest],
and branches to [succ]. *)
- | Iload: memory_chunk -> addressing -> list reg -> reg -> node -> instruction
- (** [Iload chunk addr args dest succ] loads a [chunk] quantity from
+ | Iload: trapping_mode -> memory_chunk -> addressing -> list reg -> reg -> node -> instruction
+ (** [Iload trap chunk addr args dest succ] loads a [chunk] quantity from
the address determined by the addressing mode [addr] and the
values of the [args] registers, stores the quantity just read
- into [dest], and branches to [succ]. *)
+ into [dest], and branches to [succ].
+ If trap=NOTRAP, then failures lead to a default value written to [dest]. *)
| Istore: memory_chunk -> addressing -> list reg -> reg -> node -> instruction
(** [Istore chunk addr args src succ] stores the value of register
[src] in the [chunk] quantity at the
@@ -194,6 +197,8 @@ Definition find_function
end
end.
+Definition default_notrap_load_value (chunk : memory_chunk) := Vundef.
+
(** The transitions are presented as an inductive predicate
[step ge st1 t st2], where [ge] is the global environment,
[st1] the initial state, [st2] the final state, and [t] the trace
@@ -212,12 +217,25 @@ Inductive step: state -> trace -> state -> Prop :=
step (State s f sp pc rs m)
E0 (State s f sp pc' (rs#res <- v) m)
| exec_Iload:
- forall s f sp pc rs m chunk addr args dst pc' a v,
- (fn_code f)!pc = Some(Iload chunk addr args dst pc') ->
+ forall s f sp pc rs m trap chunk addr args dst pc' a v,
+ (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') ->
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = Some v ->
step (State s f sp pc rs m)
E0 (State s f sp pc' (rs#dst <- v) m)
+ | exec_Iload_notrap1:
+ forall s f sp pc rs m chunk addr args dst pc',
+ (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') ->
+ eval_addressing ge sp addr rs##args = None ->
+ step (State s f sp pc rs m)
+ E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m)
+ | exec_Iload_notrap2:
+ forall s f sp pc rs m chunk addr args dst pc' a,
+ (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') ->
+ eval_addressing ge sp addr rs##args = Some a ->
+ Mem.loadv chunk m a = None->
+ step (State s f sp pc rs m)
+ E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m)
| exec_Istore:
forall s f sp pc rs m chunk addr args src pc' a m',
(fn_code f)!pc = Some(Istore chunk addr args src pc') ->
@@ -299,8 +317,8 @@ Proof.
Qed.
Lemma exec_Iload':
- forall s f sp pc rs m chunk addr args dst pc' rs' a v,
- (fn_code f)!pc = Some(Iload chunk addr args dst pc') ->
+ forall s f sp pc rs m trap chunk addr args dst pc' rs' a v,
+ (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') ->
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = Some v ->
rs' = (rs#dst <- v) ->
@@ -384,7 +402,7 @@ Definition successors_instr (i: instruction) : list node :=
match i with
| Inop s => s :: nil
| Iop op args res s => s :: nil
- | Iload chunk addr args dst s => s :: nil
+ | Iload trap chunk addr args dst s => s :: nil
| Istore chunk addr args src s => s :: nil
| Icall sig ros args res s => s :: nil
| Itailcall sig ros args => nil
@@ -403,7 +421,7 @@ Definition instr_uses (i: instruction) : list reg :=
match i with
| Inop s => nil
| Iop op args res s => args
- | Iload chunk addr args dst s => args
+ | Iload trap chunk addr args dst s => args
| Istore chunk addr args src s => src :: args
| Icall sig (inl r) args res s => r :: args
| Icall sig (inr id) args res s => args
@@ -422,7 +440,7 @@ Definition instr_defs (i: instruction) : option reg :=
match i with
| Inop s => None
| Iop op args res s => Some res
- | Iload chunk addr args dst s => Some dst
+ | Iload trap chunk addr args dst s => Some dst
| Istore chunk addr args src s => None
| Icall sig ros args res s => Some res
| Itailcall sig ros args => None
@@ -462,7 +480,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) :=
match i with
| Inop s => m
| Iop op args res s => fold_left Pos.max args (Pos.max res m)
- | Iload chunk addr args dst s => fold_left Pos.max args (Pos.max dst m)
+ | Iload trap chunk addr args dst s => fold_left Pos.max args (Pos.max dst m)
| Istore chunk addr args src s => fold_left Pos.max args (Pos.max src m)
| Icall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m))
| Icall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m)
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 9d7a8506..a0ca0f17 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -436,7 +436,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
transl_exprlist map al rl no
| Eload chunk addr al =>
do rl <- alloc_regs map al;
- do no <- add_instr (Iload chunk addr rl rd nd);
+ do no <- add_instr (Iload TRAP chunk addr rl rd nd);
transl_exprlist map al rl no
| Econdition a b c =>
do nfalse <- transl_expr map c rd nd;
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 17022a7d..aa83da6d 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -707,7 +707,7 @@ Inductive tr_expr (c: code):
tr_expr c map pr (Eop op al) ns nd rd dst
| tr_Eload: forall map pr chunk addr al ns nd rd n1 rl dst,
tr_exprlist c map pr al ns n1 rl ->
- c!n1 = Some (Iload chunk addr rl rd nd) ->
+ c!n1 = Some (Iload TRAP chunk addr rl rd nd) ->
reg_map_ok map rd dst -> ~In rd pr ->
tr_expr c map pr (Eload chunk addr al) ns nd rd dst
| tr_Econdition: forall map pr a ifso ifnot ns nd rd ntrue nfalse dst,
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 8336d1bf..6d27df28 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -104,11 +104,11 @@ Inductive wt_instr : instruction -> Prop :=
valid_successor s ->
wt_instr (Iop op args res s)
| wt_Iload:
- forall chunk addr args dst s,
+ forall trap chunk addr args dst s,
map env args = type_of_addressing addr ->
env dst = type_of_chunk chunk ->
valid_successor s ->
- wt_instr (Iload chunk addr args dst s)
+ wt_instr (Iload trap chunk addr args dst s)
| wt_Istore:
forall chunk addr args src s,
map env args = type_of_addressing addr ->
@@ -282,7 +282,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
else
(let (targs, tres) := type_of_operation op in
do e1 <- S.set_list e args targs; S.set e1 res tres)
- | Iload chunk addr args dst s =>
+ | Iload trap chunk addr args dst s =>
do x <- check_successor s;
do e1 <- S.set_list e args (type_of_addressing addr);
S.set e1 dst (type_of_chunk chunk)
@@ -841,14 +841,14 @@ Proof.
Qed.
Lemma wt_exec_Iload:
- forall env f chunk addr args dst s m a v rs,
- wt_instr f env (Iload chunk addr args dst s) ->
+ forall env f trap chunk addr args dst s m a v rs,
+ wt_instr f env (Iload trap chunk addr args dst s) ->
Mem.loadv chunk m a = Some v ->
wt_regset env rs ->
wt_regset env (rs#dst <- v).
Proof.
intros. destruct a; simpl in H0; try discriminate. inv H.
- eapply wt_regset_assign; eauto. rewrite H8; eapply Mem.load_type; eauto.
+ eapply wt_regset_assign; eauto. rewrite H9; eapply Mem.load_type; eauto.
Qed.
Lemma wt_exec_Ibuiltin:
diff --git a/backend/Renumber.v b/backend/Renumber.v
index 10f58251..7ba16658 100644
--- a/backend/Renumber.v
+++ b/backend/Renumber.v
@@ -43,7 +43,7 @@ Definition renum_instr (i: instruction) : instruction :=
match i with
| Inop s => Inop (renum_pc s)
| Iop op args res s => Iop op args res (renum_pc s)
- | Iload chunk addr args res s => Iload chunk addr args res (renum_pc s)
+ | Iload trap chunk addr args res s => Iload trap chunk addr args res (renum_pc s)
| Istore chunk addr args src s => Istore chunk addr args src (renum_pc s)
| Icall sg ros args res s => Icall sg ros args res (renum_pc s)
| Itailcall sg ros args => i
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index 7cda9425..2e161965 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -175,6 +175,18 @@ Proof.
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
eapply exec_Iload; eauto.
constructor; auto. eapply reach_succ; eauto. simpl; auto.
+ (* load notrap1 *)
+ econstructor; split.
+ assert (eval_addressing tge sp addr rs ## args = None).
+ rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+ eapply exec_Iload_notrap1; eauto.
+ constructor; auto. eapply reach_succ; eauto. simpl; auto.
+ (* load notrap2 *)
+ econstructor; split.
+ assert (eval_addressing tge sp addr rs ## args = Some a).
+ rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+ eapply exec_Iload_notrap2; eauto.
+ constructor; auto. eapply reach_succ; eauto. simpl; auto.
(* store *)
econstructor; split.
assert (eval_addressing tge sp addr rs ## args = Some a).
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 06e314f3..4a5e83a1 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -438,6 +438,19 @@ Proof.
apply eval_addressing_preserved. exact symbols_preserved. eauto.
econstructor; eauto. apply set_reg_lessdef; auto.
+ (* TODO *)
+- (* load notrap1 *)
+ TransfInstr.
+ assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
+
+ intros [a' [ADDR' ALD]].
+ exploit Mem.loadv_extends; eauto.
+ intros [v' [LOAD' VLD]].
+ left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split.
+ eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'.
+ apply eval_addressing_preserved. exact symbols_preserved. eauto.
+ econstructor; eauto. apply set_reg_lessdef; auto.
+
- (* store *)
TransfInstr.
assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v
index 8ac7c4ce..1b5f2547 100644
--- a/backend/Unusedglob.v
+++ b/backend/Unusedglob.v
@@ -46,7 +46,7 @@ Definition ref_instruction (i: instruction) : list ident :=
match i with
| Inop _ => nil
| Iop op _ _ _ => globals_operation op
- | Iload _ addr _ _ _ => globals_addressing addr
+ | Iload _ _ addr _ _ _ => globals_addressing addr
| Istore _ addr _ _ _ => globals_addressing addr
| Icall _ (inl r) _ _ _ => nil
| Icall _ (inr id) _ _ _ => id :: nil
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 680daba7..fa120b6d 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -915,7 +915,7 @@ Proof.
/\ Val.inject j a ta).
{ apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args).
intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
- apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto.
+ apply KEPT. red. exists pc, (Iload trap chunk addr args dst pc'); auto.
econstructor; eauto.
apply regs_inject; auto.
assumption. }
@@ -924,6 +924,36 @@ Proof.
econstructor; split. eapply exec_Iload; eauto.
econstructor; eauto. apply set_reg_inject; auto.
+- (* load notrap1 *)
+ assert (eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = None).
+ { eapply eval_addressing_inj_none.
+ intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+ apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto.
+ econstructor; eauto.
+ rewrite Ptrofs.add_zero; reflexivity.
+ apply regs_inject; auto.
+ eassumption.
+ assumption. }
+
+ econstructor; split. eapply exec_Iload_notrap1; eauto.
+ econstructor; eauto. apply set_reg_inject; auto.
+
+- (* load notrap2 *)
+ assert (A: exists ta,
+ eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta
+ /\ Val.inject j a ta).
+ { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args).
+ intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+ apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto.
+ econstructor; eauto.
+ apply regs_inject; auto.
+ assumption. }
+ destruct A as (ta & B & C).
+ destruct (Mem.loadv chunk tm ta) eqn:Echunk2.
+ + econstructor; split. eapply exec_Iload; eauto.
+ econstructor; eauto. apply set_reg_inject; auto.
+ + econstructor; split. eapply exec_Iload_notrap2; eauto.
+ econstructor; eauto. apply set_reg_inject; auto.
- (* store *)
assert (A: exists ta,
eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 1f80c293..605d7e90 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -121,7 +121,7 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) :
| Some(Iop op args res s) =>
let a := eval_static_operation op (aregs ae args) in
VA.State (AE.set res a ae) am
- | Some(Iload chunk addr args dst s) =>
+ | Some(Iload trap chunk addr args dst s) =>
let a := loadv chunk rm am (eval_static_addressing addr (aregs ae args)) in
VA.State (AE.set dst a ae) am
| Some(Istore chunk addr args src s) =>
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 815d3958..f3ee0577 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -1649,6 +1649,27 @@ Proof.
- apply Val.offset_ptr_inject; auto.
Qed.
+Lemma eval_addressing_inj_none:
+ forall addr sp1 vl1 sp2 vl2,
+ (forall id ofs,
+ In id (globals_addressing addr) ->
+ Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+ Val.inject f sp1 sp2 ->
+ Val.inject_list f vl1 vl2 ->
+ eval_addressing ge1 sp1 addr vl1 = None ->
+ eval_addressing ge2 sp2 addr vl2 = None.
+Proof.
+ intros until vl2. intros Hglobal Hinjsp Hinjvl.
+ destruct addr; simpl in *.
+ 1,2: inv Hinjvl; trivial;
+ inv H0; trivial;
+ inv H2; trivial;
+ discriminate.
+ 2,3: inv Hinjvl; trivial; discriminate.
+ inv Hinjvl; trivial; inv H0; trivial;
+ inv H; trivial; discriminate.
+Qed.
+
End EVAL_COMPAT.
(** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *)
@@ -1755,6 +1776,24 @@ Proof.
destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
Qed.
+
+Lemma eval_addressing_lessdef_none:
+ forall sp addr vl1 vl2,
+ Val.lessdef_list vl1 vl2 ->
+ eval_addressing genv sp addr vl1 = None ->
+ eval_addressing genv sp addr vl2 = None.
+Proof.
+ intros until vl2. intros Hlessdef Heval1.
+ destruct addr; simpl in *.
+ 1, 2, 4, 5: inv Hlessdef; trivial;
+ inv H0; trivial;
+ inv H2; trivial;
+ discriminate.
+ inv Hlessdef; trivial.
+ inv H0; trivial.
+ discriminate.
+Qed.
+
End EVAL_LESSDEF.
(** Compatibility of the evaluation functions with memory injections. *)
generated by cgit (git 2.34.1) at 2024-06-11 21:58:28 +0000