diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
commit | 265fa07b34a813ba9d8249ddad82d71e6002c10d (patch) | |
tree | 45831b1793c7920b10969fc7cf6316c202d78e91 /backend/Linear.v | |
parent | 94470fb6a652cb993982269fcb7a0e8319b54488 (diff) | |
download | compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.tar.gz compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.zip |
Merge of the reuse-temps branch:
- Reload temporaries are marked as destroyed (set to Vundef) across
operations in the semantics of LTL, LTLin, Linear and Mach,
allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Linear.v')
-rw-r--r-- | backend/Linear.v | 30 |
1 files changed, 22 insertions, 8 deletions
diff --git a/backend/Linear.v b/backend/Linear.v index 0f44206d..40f7e416 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -163,6 +163,20 @@ Definition return_regs (caller callee: locset) : locset := | S s => caller (S s) end. +(** Temporaries destroyed across operations *) + +Definition undef_op (op: operation) (rs: locset) := + match op with + | Omove => rs + | _ => undef_temps rs + end. + +Definition undef_getstack (s: slot) (rs: locset) := + match s with + | Incoming _ _ => Locmap.set (R IT1) Vundef rs + | _ => rs + end. + (** Linear execution states. *) Inductive stackframe: Type := @@ -241,7 +255,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lgetstack: forall s f sp sl r b rs m, step (State s f sp (Lgetstack sl r :: b) rs m) - E0 (State s f sp b (Locmap.set (R r) (rs (S sl)) rs) m) + E0 (State s f sp b (Locmap.set (R r) (rs (S sl)) (undef_getstack sl rs)) m) | exec_Lsetstack: forall s f sp r sl b rs m, step (State s f sp (Lsetstack r sl :: b) rs m) @@ -250,19 +264,19 @@ Inductive step: state -> trace -> state -> Prop := forall s f sp op args res b rs m v, eval_operation ge sp op (reglist rs args) = Some v -> step (State s f sp (Lop op args res :: b) rs m) - E0 (State s f sp b (Locmap.set (R res) v rs) m) + E0 (State s f sp b (Locmap.set (R res) v (undef_op op rs)) m) | exec_Lload: forall s f sp chunk addr args dst b rs m a v, eval_addressing ge sp addr (reglist rs args) = Some a -> Mem.loadv chunk m a = Some v -> step (State s f sp (Lload chunk addr args dst :: b) rs m) - E0 (State s f sp b (Locmap.set (R dst) v rs) m) + E0 (State s f sp b (Locmap.set (R dst) v (undef_temps rs)) m) | exec_Lstore: forall s f sp chunk addr args src b rs m m' a, eval_addressing ge sp addr (reglist rs args) = Some a -> Mem.storev chunk m a (rs (R src)) = Some m' -> step (State s f sp (Lstore chunk addr args src :: b) rs m) - E0 (State s f sp b rs m') + E0 (State s f sp b (undef_temps rs) m') | exec_Lcall: forall s f sp sig ros b rs m f', find_function ros rs = Some f' -> @@ -280,7 +294,7 @@ Inductive step: state -> trace -> state -> Prop := forall s f sp rs m ef args res b t v m', external_call ef ge (reglist rs args) m t v m' -> step (State s f sp (Lbuiltin ef args res :: b) rs m) - t (State s f sp b (Locmap.set (R res) v rs) m') + t (State s f sp b (Locmap.set (R res) v (undef_temps rs)) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -295,19 +309,19 @@ Inductive step: state -> trace -> state -> Prop := eval_condition cond (reglist rs args) = Some true -> find_label lbl f.(fn_code) = Some b' -> step (State s f sp (Lcond cond args lbl :: b) rs m) - E0 (State s f sp b' rs m) + E0 (State s f sp b' (undef_temps rs) m) | exec_Lcond_false: forall s f sp cond args lbl b rs m, eval_condition cond (reglist rs args) = Some false -> step (State s f sp (Lcond cond args lbl :: b) rs m) - E0 (State s f sp b rs m) + E0 (State s f sp b (undef_temps rs) m) | exec_Ljumptable: forall s f sp arg tbl b rs m n lbl b', rs (R arg) = Vint n -> list_nth_z tbl (Int.signed n) = Some lbl -> find_label lbl f.(fn_code) = Some b' -> step (State s f sp (Ljumptable arg tbl :: b) rs m) - E0 (State s f sp b' rs m) + E0 (State s f sp b' (undef_temps rs) m) | exec_Lreturn: forall s f stk b rs m m', Mem.free m stk 0 f.(fn_stacksize) = Some m' -> |