From 5798f56b8a8630e43dbed84a824811a5626a1503 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 18 Jun 2021 18:35:50 +0200
Subject: Replacing default notrap load value by Vundef everywhere

---
 backend/CSE2proof.v         | 4 ++--
 backend/CSE3analysisproof.v | 2 +-
 backend/CSEdomain.v         | 4 ++--
 backend/CSEproof.v          | 5 ++---
 backend/Deadcodeproof.v     | 2 --
 backend/LTL.v               | 4 ++--
 backend/Linear.v            | 4 ++--
 backend/Lineartyping.v      | 2 --
 backend/Mach.v              | 4 ++--
 backend/RTL.v               | 4 ++--
 backend/RTLtyping.v         | 2 +-
 backend/Tailcallproof.v     | 4 ++--
 backend/ValueAnalysis.v     | 2 --
 13 files changed, 18 insertions(+), 25 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 49dbd409..252240c9 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1399,7 +1399,7 @@ Proof.
     2: discriminate.
     econstructor; split.
     {
-      eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto.
+      eapply exec_Iop with (v := Vundef); eauto.
       simpl.
       rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
       {
@@ -1472,7 +1472,7 @@ Proof.
     2: discriminate.
     econstructor; split.
     {
-      eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto.
+      eapply exec_Iop with (v := Vundef); eauto.
       simpl.
       rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
       {
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index d53cf604..382c9f4c 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -502,7 +502,7 @@ Section SOUNDNESS.
         end
       with
       | Some dat => v' = dat
-      | None => v' = default_notrap_load_value chunk
+      | None => v' = Vundef
       end
     end.
     
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index f78e1d25..9641d012 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -113,12 +113,12 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem):
 (*  | load_notrap1_eval_to: forall chunk addr vl,
       eval_addressing ge sp addr (map valu vl) = None ->
       rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl)
-                  (default_notrap_load_value chunk)
+                  Vundef
   | load_notrap2_eval_to: forall chunk addr vl a,
       eval_addressing ge sp addr (map valu vl) = Some a ->
       Mem.loadv chunk m a = None ->
       rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl)
-                  (default_notrap_load_value chunk) *).
+                  Vundef *).
 
 Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem):
                                                       equation -> Prop :=
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index cf51f5a2..556b44b3 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -402,7 +402,7 @@ Lemma add_load_holds_none1:
   forall valu1 ge sp rs m n addr (args: list reg) chunk dst,
   numbering_holds valu1 ge sp rs m n ->
   eval_addressing ge sp addr rs##args = None ->
-  exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst chunk addr args).
+  exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst chunk addr args).
 Proof.
   unfold add_load; intros.
   destruct (valnum_regs n args) as [n1 vl] eqn:VN.
@@ -418,7 +418,7 @@ Lemma add_load_holds_none2:
   numbering_holds valu1 ge sp rs m n ->
   eval_addressing ge sp addr rs##args = Some a ->
   Mem.loadv chunk m a = None ->
-  exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst NOTRAP chunk addr args).
+  exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst NOTRAP chunk addr args).
 Proof.
   unfold add_load; intros.
   destruct (valnum_regs n args) as [n1 vl] eqn:VN.
@@ -1210,7 +1210,6 @@ Proof.
       exists valu1.
       apply set_unknown_holds.
       assumption.
-      unfold default_notrap_load_value.
       apply set_reg_lessdef; eauto.
     }
     {
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index b51d6cce..be20af0b 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -845,7 +845,6 @@ Ltac UseTransfer :=
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; auto.
   rewrite is_int_zero_sound by auto.
-  unfold default_notrap_load_value.
   constructor.
 + (* preserved *)
   exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption.
@@ -878,7 +877,6 @@ Ltac UseTransfer :=
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; auto.
   rewrite is_int_zero_sound by auto.
-  unfold default_notrap_load_value.
   constructor.
 + (* preserved *)
   exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto.
diff --git a/backend/LTL.v b/backend/LTL.v
index 3edd60a2..a382ef0e 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -217,14 +217,14 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (Block s f sp bb rs' m)
   | exec_Lload_notrap1: forall s f sp chunk addr args dst bb rs m rs',
       eval_addressing ge sp addr (reglist rs args) = None ->
-      rs' = Locmap.set (R dst)  (default_notrap_load_value chunk)
+      rs' = Locmap.set (R dst)  Vundef
                        (undef_regs (destroyed_by_load chunk addr) rs) ->
       step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m)
         E0 (Block s f sp bb rs' m)
   | exec_Lload_notrap2: forall s f sp chunk addr args dst bb rs m a rs',
       eval_addressing ge sp addr (reglist rs args) = Some a ->
       Mem.loadv chunk m a = None ->
-      rs' = Locmap.set (R dst) (default_notrap_load_value chunk)
+      rs' = Locmap.set (R dst) Vundef
                        (undef_regs (destroyed_by_load chunk addr) rs) ->
       step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m)
         E0 (Block s f sp bb rs' m)
diff --git a/backend/Linear.v b/backend/Linear.v
index 1443f795..cb11f7dc 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -170,7 +170,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s f sp chunk addr args dst b rs m rs',
       eval_addressing ge sp addr (reglist rs args) = None ->
       rs' = Locmap.set (R dst)
-                       (default_notrap_load_value chunk)
+                       Vundef
                        (undef_regs (destroyed_by_load chunk addr) rs) ->
       step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m)
         E0 (State s f sp b rs' m)
@@ -179,7 +179,7 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_addressing ge sp addr (reglist rs args) = Some a ->
       Mem.loadv chunk m a = None ->
       rs' = Locmap.set (R dst)
-                       (default_notrap_load_value chunk)
+                       Vundef
                        (undef_regs (destroyed_by_load chunk addr) rs) ->
       step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m)
         E0 (State s f sp b rs' m)
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 22658fb7..cf903aad 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -338,14 +338,12 @@ Local Opaque mreg_type.
   simpl in *; InvBooleans.
   econstructor; eauto.
   apply wt_setreg. eapply Val.has_subtype; eauto.
-  unfold default_notrap_load_value.
   constructor.
   apply wt_undef_regs; auto.
 - (* load notrap2 *)
   simpl in *; InvBooleans.
   econstructor; eauto.
   apply wt_setreg. eapply Val.has_subtype; eauto.
-  unfold default_notrap_load_value.
   constructor.
   apply wt_undef_regs; auto.
 - (* store *)
diff --git a/backend/Mach.v b/backend/Mach.v
index 1c6fdb18..2cfd738d 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -330,14 +330,14 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Mload_notrap1:
       forall s f sp chunk addr args dst c rs m rs',
       eval_addressing ge sp addr rs##args = None ->
-      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
       step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m)
         E0 (State s f sp c rs' m)
   | exec_Mload_notrap2:
       forall s f sp chunk addr args dst c rs m a rs',
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = None ->
-      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
       step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m)
         E0 (State s f sp c rs' m)
   | exec_Mstore:
diff --git a/backend/RTL.v b/backend/RTL.v
index 31b5cf99..fe350adf 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -225,14 +225,14 @@ Inductive step: state -> trace -> state -> Prop :=
       (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)
+        E0 (State s f sp pc' (rs#dst <- Vundef) 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)
+        E0 (State s f sp pc' (rs#dst <- Vundef) 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') ->
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 15ed6d8a..6048f895 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -858,7 +858,7 @@ Lemma wt_exec_Iload_notrap:
   forall env f chunk addr args dst s rs,
   wt_instr f env (Iload NOTRAP chunk addr args dst s) ->
   wt_regset env rs ->
-  wt_regset env (rs#dst <- (default_notrap_load_value chunk)).
+  wt_regset env (rs#dst <- Vundef).
 Proof.
   intros. 
   eapply wt_regset_assign; eauto. simpl. trivial.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 80a68327..39fc10fb 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -440,7 +440,7 @@ Proof.
   TransfInstr.
   assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
   left.
-  exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split.
+  exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
   eapply exec_Iload_notrap1.
   eassumption.
   eapply eval_addressing_lessdef_none. eassumption.
@@ -465,7 +465,7 @@ Proof.
     exact symbols_preserved.
     assumption.
     econstructor; eauto. apply set_reg_lessdef; auto.
-  + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split.
+  + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
     eapply exec_Iload_notrap2. eassumption.
     erewrite eval_addressing_preserved.
     eassumption.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 561e94c9..e20edff7 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1287,13 +1287,11 @@ Proof.
   eapply sound_succ_state; eauto. simpl; auto.
   unfold transfer; rewrite H. eauto.
   apply ematch_update; auto.
-  unfold default_notrap_load_value.
   constructor.
 - (* load notrap2 *)
   eapply sound_succ_state; eauto. simpl; auto.
   unfold transfer; rewrite H. eauto.
   apply ematch_update; auto.
-  unfold default_notrap_load_value.
   constructor.
 - (* store *)
   exploit eval_static_addressing_sound; eauto with va. intros VMADDR.
-- 
cgit