From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 2 Sep 2010 12:42:19 +0000
Subject: 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
---
 backend/LTL.v | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'backend/LTL.v')

diff --git a/backend/LTL.v b/backend/LTL.v
index e1222a52..2eff67cd 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -101,6 +101,10 @@ Definition postcall_locs (ls: locset) : locset :=
     | S s => ls (S s)
     end.
 
+(** Temporaries destroyed across instructions *)
+
+Definition undef_temps (ls: locset) := Locmap.undef temporaries ls.
+
 (** LTL execution states. *)
 
 Inductive stackframe : Type :=
@@ -166,21 +170,21 @@ Inductive step: state -> trace -> state -> Prop :=
       (fn_code f)!pc = Some(Lop op args res pc') ->
       eval_operation ge sp op (map rs args) = Some v ->
       step (State s f sp pc rs m)
-        E0 (State s f sp pc' (Locmap.set res v rs) m)
+        E0 (State s f sp pc' (Locmap.set res v (undef_temps rs)) m)
   | exec_Lload:
       forall s f sp pc rs m chunk addr args dst pc' a v,
       (fn_code f)!pc = Some(Lload chunk addr args dst pc') ->
       eval_addressing ge sp addr (map 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' (Locmap.set dst v rs) m)
+        E0 (State s f sp pc' (Locmap.set dst v (undef_temps rs)) m)
   | exec_Lstore:
       forall s f sp pc rs m chunk addr args src pc' a m',
       (fn_code f)!pc = Some(Lstore chunk addr args src pc') ->
       eval_addressing ge sp addr (map rs args) = Some a ->
       Mem.storev chunk m a (rs src) = Some m' ->
       step (State s f sp pc rs m)
-        E0 (State s f sp pc' rs m')
+        E0 (State s f sp pc' (undef_temps rs) m')
   | exec_Lcall:
       forall s f sp pc rs m sig ros args res pc' f',
       (fn_code f)!pc = Some(Lcall sig ros args res pc') ->
@@ -208,20 +212,20 @@ Inductive step: state -> trace -> state -> Prop :=
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
       eval_condition cond (map rs args) = Some true ->
       step (State s f sp pc rs m)
-        E0 (State s f sp ifso rs m)
+        E0 (State s f sp ifso (undef_temps rs) m)
   | exec_Lcond_false:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
       eval_condition cond (map rs args) = Some false ->
       step (State s f sp pc rs m)
-        E0 (State s f sp ifnot rs m)
+        E0 (State s f sp ifnot (undef_temps rs) m)
   | exec_Ljumptable:
       forall s f sp pc rs m arg tbl n pc',
       (fn_code f)!pc = Some(Ljumptable arg tbl) ->
       rs arg = Vint n ->
       list_nth_z tbl (Int.signed n) = Some pc' ->
       step (State s f sp pc rs m)
-        E0 (State s f sp pc' rs m)
+        E0 (State s f sp pc' (undef_temps rs) m)
   | exec_Lreturn:
       forall s f stk pc rs m or m',
       (fn_code f)!pc = Some(Lreturn or) ->
-- 
cgit