From 71c58a8d494eafd847776446b0c246229b2bc9cf Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Sep 2019 18:30:25 +0200
Subject: avancement (il faut utiliser Vundef visiblement)

---
 backend/Allocation.v      |  2 +-
 backend/Allocproof.v      |  8 ++++----
 backend/CSE.v             |  6 +++---
 backend/Constprop.v       |  4 ++--
 backend/Deadcode.v        |  4 ++--
 backend/Inlining.v        |  4 ++--
 backend/Inliningspec.v    |  6 +++---
 backend/Liveness.v        |  2 +-
 backend/RTL.v             | 40 +++++++++++++++++++++++++++++-----------
 backend/RTLgen.v          |  2 +-
 backend/RTLgenspec.v      |  2 +-
 backend/RTLtyping.v       | 12 ++++++------
 backend/Renumber.v        |  2 +-
 backend/Renumberproof.v   | 12 ++++++++++++
 backend/Tailcallproof.v   | 13 +++++++++++++
 backend/Unusedglob.v      |  2 +-
 backend/Unusedglobproof.v | 32 +++++++++++++++++++++++++++++++-
 backend/ValueAnalysis.v   |  2 +-
 18 files changed, 114 insertions(+), 41 deletions(-)

(limited to 'backend')

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) =>
-- 
cgit 


From 5710342ba44a451639a6c28aeb61d0fc24d7ee58 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Sep 2019 20:23:29 +0200
Subject: progress on non trapping loads

---
 backend/Tailcallproof.v | 40 ++++++++++++++++++++++++++++++++--------
 1 file changed, 32 insertions(+), 8 deletions(-)

(limited to 'backend')

diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 4a5e83a1..5cb1b980 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -438,19 +438,43 @@ 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.
+  left.
+  exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split.
+  eapply exec_Iload_notrap1.
+  eassumption.
+  eapply eval_addressing_lessdef_none. eassumption.
+  erewrite eval_addressing_preserved.
+  eassumption. exact symbols_preserved.
+
   econstructor; eauto. apply set_reg_lessdef; auto.
 
+- (* load notrap2 *)
+  TransfInstr.
+  assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
+  left.
+
+  exploit eval_addressing_lessdef; eauto.
+  intros [a' [ADDR' ALD]].
+  
+  destruct (Mem.loadv chunk m' a') eqn:Echunk2.
+  + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v) m'); split.
+    eapply exec_Iload with (a:=a'). eassumption.
+    erewrite eval_addressing_preserved.
+    eassumption.
+    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.
+    eapply exec_Iload_notrap2. eassumption.
+    erewrite eval_addressing_preserved.
+    eassumption.
+    exact symbols_preserved.
+    assumption.
+    econstructor; eauto. apply set_reg_lessdef; auto.
+    
 - (* store *)
   TransfInstr.
   assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
-- 
cgit 


From b70d80e7259873ac941830e02b022ca8e92541a6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 10:05:26 +0200
Subject: progress on non trapping loads

---
 backend/Inliningproof.v | 54 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

(limited to 'backend')

diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 181f40bf..588d7165 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -929,6 +929,15 @@ Proof.
   intros. inv H. eauto.
 Qed.
 
+Lemma eval_addressing_none:
+  forall sp' ctx addr rs,
+  eval_addressing ge (Vptr sp' (Ptrofs.repr (dstk ctx))) addr rs = None ->
+  eval_addressing ge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs = None.
+Proof.
+  intros until rs; intro Heval.
+  destruct addr; destruct rs as [| r0 rs1]; simpl in *; trivial; discriminate.
+Qed.
+
 Theorem step_simulation:
   forall S1 t S2,
   step ge S1 t S2 ->
@@ -976,6 +985,51 @@ Proof.
   apply match_stacks_inside_set_reg; auto.
   apply agree_set_reg; auto.
 
+- (* load notrap1 *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Iload_notrap1. eassumption.
+  rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge).
+  exploit eval_addressing_inj_none.
+  4: eassumption.
+  intros. eapply symbol_address_inject.
+  eapply match_stacks_inside_globals; eauto.
+  eauto.
+  instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
+  rewrite Ptrofs.add_zero_l.
+  apply eval_addressing_none.
+  exact symbols_preserved.
+  econstructor; eauto.
+  apply match_stacks_inside_set_reg; auto.
+  apply agree_set_reg; auto.
+
+- (* load notrap2 *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+
+  exploit eval_addressing_inject.
+    eapply match_stacks_inside_globals; eauto.
+    eexact SP.
+    instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
+    eauto.
+  fold (saddr ctx addr). intros [a' [P Q]].
+
+  destruct (Mem.loadv chunk m' a') eqn:Hload'.
+  + left; econstructor; split.
+    eapply plus_one.
+    eapply exec_Iload; eauto.
+    rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
+    econstructor; eauto.
+  apply match_stacks_inside_set_reg; auto.
+  apply agree_set_reg; auto.
+    
+  + left; econstructor; split.
+    eapply plus_one.
+    eapply exec_Iload_notrap2; eauto.
+    rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
+    econstructor; eauto.
+  apply match_stacks_inside_set_reg; auto.
+  apply agree_set_reg; auto.
+  
 - (* store *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
   exploit eval_addressing_inject.
-- 
cgit 


From 5177f34535a70e4335dbab3a66c916c976405df7 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 18:27:40 +0200
Subject: Value analysis for non trapping loads

---
 backend/RTLtyping.v     | 14 ++++++++++++++
 backend/ValueAnalysis.v | 28 ++++++++++++++++++++++++----
 2 files changed, 38 insertions(+), 4 deletions(-)

(limited to 'backend')

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 6d27df28..74bfa582 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -851,6 +851,16 @@ Proof.
   eapply wt_regset_assign; eauto. rewrite H9; eapply Mem.load_type; eauto.
 Qed.
 
+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)).
+Proof.
+  intros. 
+  eapply wt_regset_assign; eauto. simpl. trivial.
+Qed.
+
 Lemma wt_exec_Ibuiltin:
   forall env f ef (ge: genv) args res s vargs m t vres m' rs,
   wt_instr f env (Ibuiltin ef args res s) ->
@@ -930,6 +940,10 @@ Proof.
   econstructor; eauto. eapply wt_exec_Iop; eauto.
   (* Iload *)
   econstructor; eauto. eapply wt_exec_Iload; eauto.
+  (* Iload notrap1*)
+  econstructor; eauto. eapply wt_exec_Iload_notrap; eauto.
+  (* Iload notrap2*)
+  econstructor; eauto. eapply wt_exec_Iload_notrap; eauto.
   (* Istore *)
   econstructor; eauto.
   (* Icall *)
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 5072448a..21dd2c35 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -139,9 +139,11 @@ 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 trap 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(Iload NOTRAP chunk addr args dst s) =>
+      VA.State (AE.set dst Vtop ae) am
   | Some(Istore chunk addr args src s) =>
       let am' := storev chunk am (eval_static_addressing addr (aregs ae args)) (areg ae src) in
       VA.State ae am'
@@ -1268,11 +1270,29 @@ Proof.
   apply ematch_update; auto. eapply eval_static_operation_sound; eauto with va.
 
 - (* load *)
+  destruct trap.
+  + eapply sound_succ_state; eauto. simpl; auto.
+    unfold transfer; rewrite H. eauto.
+    apply ematch_update; auto. eapply loadv_sound; eauto with va.
+    eapply eval_static_addressing_sound; eauto with va.
+  + eapply sound_succ_state; eauto. simpl; auto.
+    unfold transfer; rewrite H. eauto.
+    apply ematch_update; auto.
+    eapply vmatch_top.
+    eapply loadv_sound; try eassumption.
+    eapply eval_static_addressing_sound; eauto with va.
+- (* load notrap1 *)
   eapply sound_succ_state; eauto. simpl; auto.
   unfold transfer; rewrite H. eauto.
-  apply ematch_update; auto. eapply loadv_sound; eauto with va.
-  eapply eval_static_addressing_sound; eauto with va.
-
+  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.
   eapply sound_succ_state; eauto. simpl; auto.
-- 
cgit 


From dbdc40aede7a71596ee2412289df0169215d26d1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 20:12:42 +0200
Subject: advancing in constant propagation

---
 backend/Constprop.v      |  4 ++--
 backend/Constpropproof.v | 20 ++++++++++++++++++++
 2 files changed, 22 insertions(+), 2 deletions(-)

(limited to 'backend')

diff --git a/backend/Constprop.v b/backend/Constprop.v
index cf1a9171..eda41b39 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -181,7 +181,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 trap 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
@@ -189,7 +189,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 trap 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/Constpropproof.v b/backend/Constpropproof.v
index a5d08a0f..eb1faa2d 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -406,6 +406,8 @@ Proof.
   assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va).
   set (av := loadv chunk (romem_for cu) am aa).
   assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto).
+  destruct trap.
+  {
   destruct (const_for_result av) as [cop|] eqn:?; intros.
 + (* constant-propagated *)
   exploit const_for_result_correct; eauto. intros (v' & A & B).
@@ -431,7 +433,25 @@ Proof.
   left; econstructor; econstructor; split.
   eapply exec_Iload; eauto.
   eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+  }
+  {
+    assert (exists v2 : val,
+         eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2.
+    apply eval_addressing_lessdef with (vl1 := rs ## args).
+    apply regs_lessdef_regs; assumption.
+    assumption.
+    destruct Hexist2 as [v2 [Heval2 Hlessdef2]].
+    destruct (Mem.loadv_extends chunk m m' a v2 v MEM H1 Hlessdef2) as [vX [Hvx1 Hvx2]].
+    left; econstructor; econstructor; split.
+    eapply exec_Iload with (a := v2); eauto.
+    erewrite eval_addressing_preserved with (ge1:=ge); auto.
+    exact symbols_preserved.
+  eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+    
+  }
 
+- (* Iload notrap2 *)
+  (* TODO *)
 - (* Istore *)
   rename pc'0 into pc. TransfInstr.
   assert (ADDR:
-- 
cgit 


From 11fbb6994667de03623640842d08f1b5ee02aac1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 21:19:07 +0200
Subject: finished Constopproof for non trapping loads

---
 backend/Constpropproof.v | 42 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 41 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index eb1faa2d..eb4b6f17 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -450,8 +450,48 @@ Proof.
     
   }
 
+- (* Iload notrap1 *)
+  rename pc'0 into pc. TransfInstr.
+  assert (eval_static_addressing addr (aregs ae args) = Vbot) as Hbot by (eapply eval_static_addressing_sound_none; eauto with va).
+  assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr rs' ## args = None) as Hnone.
+  rewrite eval_addressing_preserved with (ge1 := ge).
+  apply eval_addressing_lessdef_none with (vl1 := rs ## args).
+  apply regs_lessdef_regs; assumption.
+  assumption.
+  exact symbols_preserved.
+  
+  left; econstructor; econstructor; split.
+  eapply exec_Iload_notrap1; eauto.
+  eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+
 - (* Iload notrap2 *)
-  (* TODO *)
+  rename pc'0 into pc. TransfInstr.
+    assert (exists v2 : val,
+         eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2.
+    apply eval_addressing_lessdef with (vl1 := rs ## args).
+    apply regs_lessdef_regs; assumption.
+    assumption.
+    destruct Hexist2 as [a' [Heval' Hlessdef']].
+    destruct (Mem.loadv chunk m' a') eqn:Hload'.
+    {
+    left; econstructor; econstructor; split.
+    eapply exec_Iload; eauto.
+   
+    rewrite eval_addressing_preserved with (ge1 := ge).
+    exact Heval'.
+    exact symbols_preserved.
+    eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+    }
+    {
+      left; econstructor; econstructor; split.
+      eapply exec_Iload_notrap2; eauto.
+   
+    rewrite eval_addressing_preserved with (ge1 := ge).
+    exact Heval'.
+    exact symbols_preserved.
+    eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+    }
+
 - (* Istore *)
   rename pc'0 into pc. TransfInstr.
   assert (ADDR:
-- 
cgit 


From 2fe044ba1dbaa3fce00a221d988e06c6907cfaf2 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 22:02:38 +0200
Subject: Dead code proof for non trapping loads

---
 backend/Deadcodeproof.v | 77 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

(limited to 'backend')

diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 2edc0395..6919fe78 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -829,6 +829,83 @@ Ltac UseTransfer :=
   apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
 
+- (* load notrap1 *)
+  TransfInstr; UseTransfer.
+  destruct (is_dead (nreg ne dst)) eqn:DEAD;
+  [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO];
+  simpl in *.
++ (* dead instruction, turned into a nop *)
+  econstructor; split.
+  eapply exec_Inop; eauto.
+  eapply match_succ_states; eauto. simpl; auto.
+  apply eagree_update_dead; auto with na.
++ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
+  econstructor; split.
+  eapply exec_Iop with (v := Vint Int.zero); eauto.
+  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.
+  intro Hnone'.
+  assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'.
+  erewrite eval_addressing_preserved with (ge1 := ge).
+  assumption.
+  exact symbols_preserved.
+  
+  econstructor; split.
+  eapply exec_Iload_notrap1; eauto.
+  eapply match_succ_states; eauto. simpl; auto.
+  apply eagree_update; eauto 2 with na.
+  eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
+
+- (* load notrap2 *)
+  TransfInstr; UseTransfer.
+  
+  destruct (is_dead (nreg ne dst)) eqn:DEAD;
+  [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO];
+  simpl in *.
++ (* dead instruction, turned into a nop *)
+  econstructor; split.
+  eapply exec_Inop; eauto.
+  eapply match_succ_states; eauto. simpl; auto.
+  apply eagree_update_dead; auto with na.
++ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
+  econstructor; split.
+  eapply exec_Iop with (v := Vint Int.zero); eauto.
+  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.
+  intros (ta & U & V).
+  destruct (Mem.loadv chunk tm ta) eqn:Hchunk2.
+  {
+  econstructor; split.
+  eapply exec_Iload. eauto.
+  erewrite eval_addressing_preserved with (ge1 := ge).
+  eassumption.
+  exact symbols_preserved.
+  eassumption.
+  eapply match_succ_states; eauto. simpl; auto.
+  apply eagree_update; eauto 2 with na.
+  eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
+  }
+  {
+  econstructor; split.
+  eapply exec_Iload_notrap2. eauto.
+  erewrite eval_addressing_preserved with (ge1 := ge).
+  eassumption.
+  exact symbols_preserved.
+  eassumption.
+  eapply match_succ_states; eauto. simpl; auto.
+  apply eagree_update; eauto 2 with na.
+  eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
+  }
 - (* store *)
   TransfInstr; UseTransfer.
   destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args)
-- 
cgit 


From 1d90fa730df7d1cb2ee726d3b41b9915ae4e4e2e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 23:02:06 +0200
Subject: moved trapping_mode to a more appropriate place

---
 backend/RTL.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'backend')

diff --git a/backend/RTL.v b/backend/RTL.v
index d09cca77..95fa1f82 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -36,8 +36,6 @@ 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. *)
-- 
cgit 


From 686f0aaff7a4c37e13bfbe823b4dd2a879556f0a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 4 Sep 2019 06:55:27 +0200
Subject: begin CSE

---
 backend/CSE.v           | 18 +++++++++---------
 backend/CSEdomain.v     | 10 +++++-----
 backend/CSEproof.v      | 10 ++++++----
 backend/ValueAnalysis.v |  3 +++
 4 files changed, 23 insertions(+), 18 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE.v b/backend/CSE.v
index 9da30f50..1c884cf0 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -202,10 +202,10 @@ Definition add_op (n: numbering) (rd: reg) (op: operation) (rs: list reg) :=
   and added to [n] as described in [add_rhs]. *)
 
 Definition add_load (n: numbering) (rd: reg)
-                    (chunk: memory_chunk) (addr: addressing)
+                    (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
                     (rs: list reg) :=
   let (n1, vs) := valnum_regs n rs in
-  add_rhs n1 rd (Load chunk addr vs).
+  add_rhs n1 rd (Load trap chunk addr vs).
 
 (** [set_unknown n rd] returns a numbering where [rd] is mapped to
   no value number, and no equations are added.  This is useful
@@ -246,7 +246,7 @@ Definition kill_equations (pred: rhs -> bool) (n: numbering) : numbering :=
 Definition filter_loads (r: rhs) : bool :=
   match r with
   | Op op _ => op_depends_on_memory op
-  | Load _ _ _ => true
+  | Load _ _ _ _ => true
   end.
 
 Definition kill_all_loads (n: numbering) : numbering :=
@@ -262,7 +262,7 @@ Definition filter_after_store (app: VA.t) (n: numbering) (p: aptr) (sz: Z) (r: r
   match r with
   | Op op vl =>
       op_depends_on_memory op
-  | Load chunk addr vl =>
+  | Load trap chunk addr vl =>
       match regs_valnums n vl with
       | None => true
       | Some rl =>
@@ -297,7 +297,7 @@ Definition add_store_result (app: VA.t) (n: numbering) (chunk: memory_chunk) (ad
     let (n1, vsrc) := valnum_reg n rsrc in
     let (n2, vargs) := valnum_regs n1 rargs in
     {| num_next := n2.(num_next);
-       num_eqs  := Eq vsrc false (Load chunk addr vargs) :: n2.(num_eqs);
+       num_eqs  := Eq vsrc false (Load TRAP chunk addr vargs) :: n2.(num_eqs);
        num_reg  := n2.(num_reg);
        num_val  := n2.(num_val) |}
   else n.
@@ -326,7 +326,7 @@ Definition kill_loads_after_storebytes
 
 Definition shift_memcpy_eq (src sz delta: Z) (e: equation) :=
   match e with
-  | Eq l strict (Load chunk (Ainstack i) _) =>
+  | Eq l strict (Load trap chunk (Ainstack i) _) =>
       let i := Ptrofs.unsigned i in
       let j := i + delta in
       if zle src i
@@ -334,7 +334,7 @@ Definition shift_memcpy_eq (src sz delta: Z) (e: equation) :=
       && zeq (Z.modulo delta (align_chunk chunk)) 0
       && zle 0 j
       && zle j Ptrofs.max_unsigned
-      then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil))
+      then Some(Eq l strict (Load trap chunk (Ainstack (Ptrofs.repr j)) nil))
       else None
   | _ => None
   end.
@@ -460,7 +460,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
       | Iop op args res s =>
           add_op before res op args
       | Iload trap chunk addr args dst s =>
-          add_load before dst chunk addr args
+          add_load before dst trap chunk addr args
       | Istore chunk addr args src s =>
           let app := approx!!pc in
           let n := kill_loads_after_store app before chunk addr args in
@@ -536,7 +536,7 @@ Definition transf_instr (n: numbering) (instr: instruction) :=
         end
   | Iload trap chunk addr args dst s =>
       let (n1, vl) := valnum_regs n args in
-      match find_rhs n1 (Load chunk addr vl) with
+      match find_rhs n1 (Load trap chunk addr vl) with
       | Some r =>
           Iop Omove (r :: nil) dst s
       | None =>
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index 9b1243c8..aa0b9fb1 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -32,7 +32,7 @@ Definition valnum := positive.
 
 Inductive rhs : Type :=
   | Op: operation -> list valnum -> rhs
-  | Load: memory_chunk -> addressing -> list valnum -> rhs.
+  | Load: trapping_mode -> memory_chunk -> addressing -> list valnum -> rhs.
 
 Inductive equation : Type :=
   | Eq (v: valnum) (strict: bool) (r: rhs).
@@ -43,7 +43,7 @@ Definition eq_list_valnum: forall (x y: list valnum), {x=y}+{x<>y} := list_eq_de
 
 Definition eq_rhs (x y: rhs) : {x=y}+{x<>y}.
 Proof.
-  generalize chunk_eq eq_operation eq_addressing eq_valnum eq_list_valnum.
+  generalize trapping_mode_eq chunk_eq eq_operation eq_addressing eq_valnum eq_list_valnum.
   decide equality.
 Defined.
 
@@ -74,7 +74,7 @@ Definition empty_numbering :=
 Definition valnums_rhs (r: rhs): list valnum :=
   match r with
   | Op op vl => vl
-  | Load chunk addr vl => vl
+  | Load trap chunk addr vl => vl
   end.
 
 Definition wf_rhs (next: valnum) (r: rhs) : Prop :=
@@ -106,10 +106,10 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem):
   | op_eval_to: forall op vl v,
       eval_operation ge sp op (map valu vl) m = Some v ->
       rhs_eval_to valu ge sp m (Op op vl) v
-  | load_eval_to: forall chunk addr vl a v,
+  | load_eval_to: forall trap chunk addr vl a v,
       eval_addressing ge sp addr (map valu vl) = Some a ->
       Mem.loadv chunk m a = Some v ->
-      rhs_eval_to valu ge sp m (Load chunk addr vl) v.
+      rhs_eval_to valu ge sp m (Load trap chunk addr vl) v.
 
 Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem):
                                                       equation -> Prop :=
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 03c7ecfc..c0464ab8 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -378,11 +378,11 @@ Proof.
 Qed.
 
 Lemma add_load_holds:
-  forall valu1 ge sp rs m n addr (args: list reg) a chunk v dst,
+  forall valu1 ge sp rs m n addr (args: list reg) a trap chunk v dst,
   numbering_holds valu1 ge sp rs m n ->
   eval_addressing ge sp addr rs##args = Some a ->
   Mem.loadv chunk m a = Some v ->
-  exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst chunk addr args).
+  exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst trap chunk addr args).
 Proof.
   unfold add_load; intros.
   destruct (valnum_regs n args) as [n1 vl] eqn:VN.
@@ -641,7 +641,7 @@ Lemma shift_memcpy_eq_holds:
 Proof with (try discriminate).
   intros. set (delta := dst - src) in *. unfold shift_memcpy_eq in H.
   destruct e as [l strict rhs] eqn:E.
-  destruct rhs as [op vl | chunk addr vl]...
+  destruct rhs as [op vl | trap chunk addr vl]...
   destruct addr...
   try (rename i into ofs).
   set (i1 := Ptrofs.unsigned ofs) in *. set (j := i1 + delta) in *.
@@ -1034,7 +1034,7 @@ Proof.
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].
   exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
-  destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?.
+  destruct (find_rhs n1 (Load trap chunk addr vl)) as [r|] eqn:?.
 + (* replaced by move *)
   exploit find_rhs_sound; eauto. intros (v' & EV & LD).
   assert (v' = v) by (inv EV; congruence). subst v'.
@@ -1064,6 +1064,8 @@ Proof.
   eapply add_load_holds; eauto.
   apply set_reg_lessdef; auto.
 
+  (* TODO *)
+
 - (* Istore *)
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 21dd2c35..084a4548 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -142,6 +142,9 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) :
   | 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
+
+  (* TODO: maybe a case analysis on the results of loadv? *)
+               
   | Some(Iload NOTRAP chunk addr args dst s) =>
       VA.State (AE.set dst Vtop ae) am
   | Some(Istore chunk addr args src s) =>
-- 
cgit 


From 44f4bea5d16273b834b1bcc8624c8f00aefaf018 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 4 Sep 2019 10:23:03 +0200
Subject: begin CSE proof for notrap load

---
 backend/CSEproof.v | 88 ++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 85 insertions(+), 3 deletions(-)

(limited to 'backend')

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index c0464ab8..def8003c 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -71,7 +71,9 @@ Lemma rhs_eval_to_exten:
 Proof.
   intros. inv H; simpl in *.
 - constructor. rewrite valnums_val_exten by assumption. auto.
-- econstructor; eauto. rewrite valnums_val_exten by assumption. auto.
+- eapply load_eval_to; eauto. rewrite valnums_val_exten by assumption. auto.
+- apply load_notrap1_eval_to; auto. rewrite valnums_val_exten by assumption. assumption.
+- eapply load_notrap2_eval_to; eauto. rewrite valnums_val_exten by assumption. assumption.
 Qed.
 
 Lemma equation_holds_exten:
@@ -393,6 +395,38 @@ Proof.
 + intros. apply Regmap.gso; auto.
 Qed.
 
+
+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 NOTRAP chunk addr args).
+Proof.
+  unfold add_load; intros.
+  destruct (valnum_regs n args) as [n1 vl] eqn:VN.
+  exploit valnum_regs_holds; eauto.
+  intros (valu2 & A & B & C & D & E).
+  eapply add_rhs_holds; eauto.
++ rewrite Regmap.gss; auto. eapply load_notrap1_eval_to. rewrite <- B; eauto.
++ intros. apply Regmap.gso; auto.
+Qed.
+
+Lemma add_load_holds_none2:
+  forall valu1 ge sp rs m n addr (args: list reg) a chunk dst,
+  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).
+Proof.
+  unfold add_load; intros.
+  destruct (valnum_regs n args) as [n1 vl] eqn:VN.
+  exploit valnum_regs_holds; eauto.
+  intros (valu2 & A & B & C & D & E).
+  eapply add_rhs_holds; eauto.
++ rewrite Regmap.gss; auto. eapply load_notrap2_eval_to. rewrite <- B; eauto. assumption. 
++ intros. apply Regmap.gso; auto.
+Qed.
+
 Lemma set_unknown_holds:
   forall valu ge sp rs m n r v,
   numbering_holds valu ge sp rs m n ->
@@ -456,8 +490,8 @@ Lemma kill_all_loads_hold:
 Proof.
   intros. eapply kill_equations_hold; eauto.
   unfold filter_loads; intros. inv H1.
-  constructor. rewrite <- H2. apply op_depends_on_memory_correct; auto.
-  discriminate.
+  1: constructor; rewrite <- H2; apply op_depends_on_memory_correct; auto.
+  all: discriminate.
 Qed.
 
 Lemma kill_loads_after_store_holds:
@@ -486,6 +520,18 @@ Proof.
   apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va.
+- eapply load_notrap1_eval_to; assumption.
+- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
+  eapply load_notrap2_eval_to; eauto.
+  rewrite <- H9.
+  destruct a; simpl in H1; try discriminate.
+  destruct a0; simpl in H9; try discriminate; simpl; trivial.
+  rewrite negb_false_iff in H6. unfold aaddressing in H6.
+  eapply Mem.load_store_other. eauto.
+  eapply pdisjoint_sound; eauto.
+  apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
+  erewrite <- regs_valnums_sound by eauto. eauto with va.
+  apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va.
 Qed.
 
 Lemma store_normalized_range_sound:
@@ -562,6 +608,8 @@ Proof.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   auto.
+
+(* TODO *)
 Qed.
 
 Lemma load_memcpy:
@@ -1064,6 +1112,40 @@ Proof.
   eapply add_load_holds; eauto.
   apply set_reg_lessdef; auto.
 
+- (* Iload notrap1 *)
+  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
+  destruct (find_rhs n1 (Load NOTRAP chunk addr vl)) as [r|] eqn:?.
++ (* replaced by move *)
+  exploit find_rhs_sound; eauto. intros (v' & EV & LD).
+  assert (v' = Vundef) by (inv EV; congruence). subst v'.
+  econstructor; split.
+  eapply exec_Iop; eauto. simpl; eauto.
+  econstructor; eauto.
+  eapply analysis_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H.
+  eapply add_load_holds; eauto.
+  apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
++ (* load is preserved, but addressing is possibly simplified *)
+  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
+  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
+  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
+    intros; eapply combine_addr_sound; eauto. }
+  exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
+  intros [a' [A B]].
+  assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a').
+  { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
+  exploit Mem.loadv_extends; eauto.
+  intros [v' [X Y]].
+  econstructor; split.
+  eapply exec_Iload; eauto.
+  econstructor; eauto.
+  eapply analysis_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H.
+  eapply add_load_holds; eauto.
+  apply set_reg_lessdef; auto.
+
   (* TODO *)
 
 - (* Istore *)
-- 
cgit 


From 55a90812e9f6f65b4abe7a124e933875f212238c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 4 Sep 2019 18:44:23 +0200
Subject: ca avance

---
 backend/CSEproof.v | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'backend')

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index def8003c..108aef31 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -608,8 +608,17 @@ Proof.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   auto.
-
-(* TODO *)
+- eapply load_notrap1_eval_to; assumption.
+- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
+  eapply load_notrap2_eval_to; eauto. rewrite <- H11.
+  destruct a; simpl in H10; try discriminate; simpl; trivial.
+  rewrite negb_false_iff in H8.
+  eapply Mem.load_storebytes_other. eauto.
+  rewrite H6. rewrite Z2Nat.id by omega.
+  eapply pdisjoint_sound. eauto.
+  unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
+  erewrite <- regs_valnums_sound by eauto. eauto with va.
+  auto.
 Qed.
 
 Lemma load_memcpy:
-- 
cgit 


From fcb50cc5284a006bde4eda21431dc811412cf819 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 4 Sep 2019 19:46:40 +0200
Subject: stuck in CSEproof

---
 backend/CSEdomain.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index aa0b9fb1..26d9c481 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -109,7 +109,16 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem):
   | load_eval_to: forall trap chunk addr vl a v,
       eval_addressing ge sp addr (map valu vl) = Some a ->
       Mem.loadv chunk m a = Some v ->
-      rhs_eval_to valu ge sp m (Load trap chunk addr vl) v.
+      rhs_eval_to valu ge sp m (Load trap chunk addr vl) v
+  | 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)
+  | 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).
 
 Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem):
                                                       equation -> Prop :=
-- 
cgit 


From e188b6c4a1c43fb83157670e1c28db5798f50f0b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 4 Sep 2019 22:58:55 +0200
Subject: going forward

---
 backend/CSEproof.v | 91 ++++++++++++++++++++++++++++++------------------------
 1 file changed, 50 insertions(+), 41 deletions(-)

(limited to 'backend')

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 108aef31..50eb4637 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -72,8 +72,10 @@ Proof.
   intros. inv H; simpl in *.
 - constructor. rewrite valnums_val_exten by assumption. auto.
 - eapply load_eval_to; eauto. rewrite valnums_val_exten by assumption. auto.
+(*
 - apply load_notrap1_eval_to; auto. rewrite valnums_val_exten by assumption. assumption.
 - eapply load_notrap2_eval_to; eauto. rewrite valnums_val_exten by assumption. assumption.
+*)
 Qed.
 
 Lemma equation_holds_exten:
@@ -380,11 +382,11 @@ Proof.
 Qed.
 
 Lemma add_load_holds:
-  forall valu1 ge sp rs m n addr (args: list reg) a trap chunk v dst,
+  forall valu1 ge sp rs m n addr (args: list reg) a chunk v dst,
   numbering_holds valu1 ge sp rs m n ->
   eval_addressing ge sp addr rs##args = Some a ->
   Mem.loadv chunk m a = Some v ->
-  exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst trap chunk addr args).
+  exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst chunk addr args).
 Proof.
   unfold add_load; intros.
   destruct (valnum_regs n args) as [n1 vl] eqn:VN.
@@ -395,12 +397,12 @@ Proof.
 + intros. apply Regmap.gso; auto.
 Qed.
 
-
+(*
 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 NOTRAP chunk addr args).
+  exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst chunk addr args).
 Proof.
   unfold add_load; intros.
   destruct (valnum_regs n args) as [n1 vl] eqn:VN.
@@ -426,6 +428,7 @@ Proof.
 + rewrite Regmap.gss; auto. eapply load_notrap2_eval_to. rewrite <- B; eauto. assumption. 
 + intros. apply Regmap.gso; auto.
 Qed.
+ *)
 
 Lemma set_unknown_holds:
   forall valu ge sp rs m n r v,
@@ -520,6 +523,7 @@ Proof.
   apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va.
+(*
 - eapply load_notrap1_eval_to; assumption.
 - destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
   eapply load_notrap2_eval_to; eauto.
@@ -532,6 +536,7 @@ Proof.
   apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va.
+*)
 Qed.
 
 Lemma store_normalized_range_sound:
@@ -608,6 +613,7 @@ Proof.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   auto.
+(*
 - eapply load_notrap1_eval_to; assumption.
 - destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
   eapply load_notrap2_eval_to; eauto. rewrite <- H11.
@@ -619,6 +625,7 @@ Proof.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
   auto.
+*)
 Qed.
 
 Lemma load_memcpy:
@@ -698,7 +705,7 @@ Lemma shift_memcpy_eq_holds:
 Proof with (try discriminate).
   intros. set (delta := dst - src) in *. unfold shift_memcpy_eq in H.
   destruct e as [l strict rhs] eqn:E.
-  destruct rhs as [op vl | trap chunk addr vl]...
+  destruct rhs as [op vl | chunk addr vl]...
   destruct addr...
   try (rename i into ofs).
   set (i1 := Ptrofs.unsigned ofs) in *. set (j := i1 + delta) in *.
@@ -1091,44 +1098,14 @@ Proof.
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].
   exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
-  destruct (find_rhs n1 (Load trap chunk addr vl)) as [r|] eqn:?.
-+ (* replaced by move *)
-  exploit find_rhs_sound; eauto. intros (v' & EV & LD).
-  assert (v' = v) by (inv EV; congruence). subst v'.
-  econstructor; split.
-  eapply exec_Iop; eauto. simpl; eauto.
-  econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H.
-  eapply add_load_holds; eauto.
-  apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
-+ (* load is preserved, but addressing is possibly simplified *)
-  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
-  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
-  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
-    intros; eapply combine_addr_sound; eauto. }
-  exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
-  intros [a' [A B]].
-  assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a').
-  { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit Mem.loadv_extends; eauto.
-  intros [v' [X Y]].
-  econstructor; split.
-  eapply exec_Iload; eauto.
-  econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H.
-  eapply add_load_holds; eauto.
-  apply set_reg_lessdef; auto.
+  destruct trap.
 
-- (* Iload notrap1 *)
-  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
-  destruct SAT as [valu1 NH1].
-  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
-  destruct (find_rhs n1 (Load NOTRAP chunk addr vl)) as [r|] eqn:?.
+  (* TRAP *)
+  {
+  destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?.
 + (* replaced by move *)
   exploit find_rhs_sound; eauto. intros (v' & EV & LD).
-  assert (v' = Vundef) by (inv EV; congruence). subst v'.
+  assert (v' = v) by (inv EV; congruence). subst v'.
   econstructor; split.
   eapply exec_Iop; eauto. simpl; eauto.
   econstructor; eauto.
@@ -1154,9 +1131,41 @@ Proof.
   unfold transfer; rewrite H.
   eapply add_load_holds; eauto.
   apply set_reg_lessdef; auto.
+  }
 
-  (* TODO *)
+  (* NOTRAP *)
+  {
+    assert (exists a' : val,
+       eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a')
+       as Haa'.    
+    apply eval_addressing_lessdef with (vl1 := rs ## args).
+    apply regs_lessdef_regs; assumption.
+    assumption.
+    destruct Haa' as [a' [Ha'1 Ha'2]].
+
+    assert (
+    exists v' : val,
+        Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by
+    (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption).
+    destruct Hload' as [v' [Hv'1 Hv'2]].
+
+    econstructor. split.
+    eapply exec_Iload; eauto.
+    rewrite eval_addressing_preserved with (ge1 := ge).
+    exact Ha'1.
+    exact symbols_preserved.
+
+    econstructor; eauto.
+    eapply analysis_correct_1; eauto. simpl; eauto.
+    unfold transfer. rewrite H.
+    exists valu1.
+    apply set_unknown_holds.
+    assumption.
+    apply set_reg_lessdef; assumption.
+  }
 
+(* TODO *)
+  
 - (* Istore *)
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].
-- 
cgit 


From 25e3a0643d99248e479b7d18f3dfcbb9bbc35d83 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 09:30:53 +0200
Subject: CSEproof for non trapping loads

---
 backend/CSE.v       | 26 +++++++++++---------
 backend/CSEdomain.v | 12 ++++-----
 backend/CSEproof.v  | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 89 insertions(+), 19 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE.v b/backend/CSE.v
index 1c884cf0..2827161d 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -202,10 +202,10 @@ Definition add_op (n: numbering) (rd: reg) (op: operation) (rs: list reg) :=
   and added to [n] as described in [add_rhs]. *)
 
 Definition add_load (n: numbering) (rd: reg)
-                    (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
+                    (chunk: memory_chunk) (addr: addressing)
                     (rs: list reg) :=
   let (n1, vs) := valnum_regs n rs in
-  add_rhs n1 rd (Load trap chunk addr vs).
+  add_rhs n1 rd (Load chunk addr vs).
 
 (** [set_unknown n rd] returns a numbering where [rd] is mapped to
   no value number, and no equations are added.  This is useful
@@ -246,7 +246,7 @@ Definition kill_equations (pred: rhs -> bool) (n: numbering) : numbering :=
 Definition filter_loads (r: rhs) : bool :=
   match r with
   | Op op _ => op_depends_on_memory op
-  | Load _ _ _ _ => true
+  | Load _ _ _ => true
   end.
 
 Definition kill_all_loads (n: numbering) : numbering :=
@@ -262,7 +262,7 @@ Definition filter_after_store (app: VA.t) (n: numbering) (p: aptr) (sz: Z) (r: r
   match r with
   | Op op vl =>
       op_depends_on_memory op
-  | Load trap chunk addr vl =>
+  | Load chunk addr vl =>
       match regs_valnums n vl with
       | None => true
       | Some rl =>
@@ -297,7 +297,7 @@ Definition add_store_result (app: VA.t) (n: numbering) (chunk: memory_chunk) (ad
     let (n1, vsrc) := valnum_reg n rsrc in
     let (n2, vargs) := valnum_regs n1 rargs in
     {| num_next := n2.(num_next);
-       num_eqs  := Eq vsrc false (Load TRAP chunk addr vargs) :: n2.(num_eqs);
+       num_eqs  := Eq vsrc false (Load chunk addr vargs) :: n2.(num_eqs);
        num_reg  := n2.(num_reg);
        num_val  := n2.(num_val) |}
   else n.
@@ -326,7 +326,7 @@ Definition kill_loads_after_storebytes
 
 Definition shift_memcpy_eq (src sz delta: Z) (e: equation) :=
   match e with
-  | Eq l strict (Load trap chunk (Ainstack i) _) =>
+  | Eq l strict (Load chunk (Ainstack i) _) =>
       let i := Ptrofs.unsigned i in
       let j := i + delta in
       if zle src i
@@ -334,7 +334,7 @@ Definition shift_memcpy_eq (src sz delta: Z) (e: equation) :=
       && zeq (Z.modulo delta (align_chunk chunk)) 0
       && zle 0 j
       && zle j Ptrofs.max_unsigned
-      then Some(Eq l strict (Load trap chunk (Ainstack (Ptrofs.repr j)) nil))
+      then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil))
       else None
   | _ => None
   end.
@@ -459,8 +459,10 @@ 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 trap chunk addr args dst s =>
-          add_load before dst trap chunk addr args
+      | Iload TRAP chunk addr args dst s =>
+        add_load before dst chunk addr args
+      | Iload NOTRAP _ _ _ dst _ =>
+        set_unknown before dst
       | Istore chunk addr args src s =>
           let app := approx!!pc in
           let n := kill_loads_after_store app before chunk addr args in
@@ -534,14 +536,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 trap 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 trap chunk addr vl) with
+      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 trap 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/CSEdomain.v b/backend/CSEdomain.v
index 26d9c481..34ec0118 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -32,7 +32,7 @@ Definition valnum := positive.
 
 Inductive rhs : Type :=
   | Op: operation -> list valnum -> rhs
-  | Load: trapping_mode -> memory_chunk -> addressing -> list valnum -> rhs.
+  | Load: memory_chunk -> addressing -> list valnum -> rhs.
 
 Inductive equation : Type :=
   | Eq (v: valnum) (strict: bool) (r: rhs).
@@ -74,7 +74,7 @@ Definition empty_numbering :=
 Definition valnums_rhs (r: rhs): list valnum :=
   match r with
   | Op op vl => vl
-  | Load trap chunk addr vl => vl
+  | Load chunk addr vl => vl
   end.
 
 Definition wf_rhs (next: valnum) (r: rhs) : Prop :=
@@ -106,11 +106,11 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem):
   | op_eval_to: forall op vl v,
       eval_operation ge sp op (map valu vl) m = Some v ->
       rhs_eval_to valu ge sp m (Op op vl) v
-  | load_eval_to: forall trap chunk addr vl a v,
+  | load_eval_to: forall chunk addr vl a v,
       eval_addressing ge sp addr (map valu vl) = Some a ->
       Mem.loadv chunk m a = Some v ->
-      rhs_eval_to valu ge sp m (Load trap chunk addr vl) v
-  | load_notrap1_eval_to: forall chunk addr vl,
+      rhs_eval_to valu ge sp m (Load chunk addr vl) v
+(*  | 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)
@@ -118,7 +118,7 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem):
       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).
+                  (default_notrap_load_value chunk) *).
 
 Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem):
                                                       equation -> Prop :=
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 50eb4637..684729d4 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1164,8 +1164,76 @@ Proof.
     apply set_reg_lessdef; assumption.
   }
 
-(* TODO *)
+- (* Iload notrap 1*)
+  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
+
+    econstructor. split.
+    eapply exec_Iload_notrap1; eauto.
+    rewrite eval_addressing_preserved with (ge1 := ge).
+    apply eval_addressing_lessdef_none with (vl1 := rs ## args).
+    apply regs_lessdef_regs; assumption.
+    assumption.
+    exact symbols_preserved.
+
+    econstructor; eauto.
+    eapply analysis_correct_1; eauto. simpl; eauto.
+    unfold transfer. rewrite H.
+    exists valu1.
+    apply set_unknown_holds.
+    assumption.
+    apply set_reg_lessdef.
+    constructor. assumption.
   
+- (* Iload notrap 2*)
+  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
+  destruct SAT as [valu1 NH1].
+  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
+
+    assert (exists a' : val,
+       eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a')
+       as Haa'.    
+    apply eval_addressing_lessdef with (vl1 := rs ## args).
+    apply regs_lessdef_regs; assumption.
+    assumption.
+    destruct Haa' as [a' [Ha'1 Ha'2]].
+
+    destruct (Mem.loadv chunk m' a') eqn:Hload'.
+
+    {
+      econstructor. split.
+      eapply exec_Iload; eauto.
+      rewrite eval_addressing_preserved with (ge1 := ge).
+      exact Ha'1.
+      exact symbols_preserved.
+      
+      econstructor; eauto.
+      eapply analysis_correct_1; eauto. simpl; eauto.
+      unfold transfer. rewrite H.
+      exists valu1.
+      apply set_unknown_holds.
+      assumption.
+      unfold default_notrap_load_value.
+      apply set_reg_lessdef; eauto.
+    }
+    {
+      econstructor. split.
+      eapply exec_Iload_notrap2; eauto.
+      rewrite eval_addressing_preserved with (ge1 := ge).
+      exact Ha'1.
+      exact symbols_preserved.
+      
+      econstructor; eauto.
+      eapply analysis_correct_1; eauto. simpl; eauto.
+      unfold transfer. rewrite H.
+      exists valu1.
+      apply set_unknown_holds.
+      assumption.
+      apply set_reg_lessdef.
+      constructor. assumption.
+    }
+    
 - (* Istore *)
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].
-- 
cgit 


From 7042070a3668ae149ec6a490b8e7c1a6aa82d6fe Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 11:07:04 +0200
Subject: LinearizeProof for non trapping loads

---
 backend/Linearizeproof.v | 48 ++++++++++++++++++++++++++++++++----------------
 1 file changed, 32 insertions(+), 16 deletions(-)

(limited to 'backend')

diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 10a3d8b2..18dc52a5 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -585,45 +585,61 @@ Proof.
   intros; eapply reachable_successors; eauto.
   eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto.
 
-  (* Lop *)
+- (* Lop *)
   left; econstructor; split. simpl.
   apply plus_one. econstructor; eauto.
   instantiate (1 := v); rewrite <- H; apply eval_operation_preserved.
   exact symbols_preserved.
   econstructor; eauto.
 
-  (* Lload *)
+- (* Lload *)
   left; econstructor; split. simpl.
-  apply plus_one. econstructor.
+  apply plus_one. eapply exec_Lload.
   instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved.
   exact symbols_preserved. eauto. eauto.
   econstructor; eauto.
 
-  (* Lgetstack *)
+- (* Lload notrap1 *)
+  left; econstructor; split. simpl.
+  apply plus_one. eapply exec_Lload_notrap1.
+  rewrite <- H.
+  apply eval_addressing_preserved.
+  exact symbols_preserved. eauto.
+  econstructor; eauto.
+  
+- (* Lload notrap2 *)
+  left; econstructor; split. simpl.
+  apply plus_one. eapply exec_Lload_notrap2.
+  rewrite <- H.
+  apply eval_addressing_preserved.
+  exact symbols_preserved. eauto. eauto.
+  econstructor; eauto.
+
+- (* Lgetstack *)
   left; econstructor; split. simpl.
   apply plus_one. econstructor; eauto.
   econstructor; eauto.
 
-  (* Lsetstack *)
+- (* Lsetstack *)
   left; econstructor; split. simpl.
   apply plus_one. econstructor; eauto.
   econstructor; eauto.
 
-  (* Lstore *)
+- (* Lstore *)
   left; econstructor; split. simpl.
   apply plus_one. econstructor.
   instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved.
   exact symbols_preserved. eauto. eauto.
   econstructor; eauto.
 
-  (* Lcall *)
+- (* Lcall *)
   exploit find_function_translated; eauto. intros [tfd [A B]].
   left; econstructor; split. simpl.
   apply plus_one. econstructor; eauto.
   symmetry; eapply sig_preserved; eauto.
   econstructor; eauto. constructor; auto. econstructor; eauto.
 
-  (* Ltailcall *)
+- (* Ltailcall *)
   exploit find_function_translated; eauto. intros [tfd [A B]].
   left; econstructor; split. simpl.
   apply plus_one. econstructor; eauto.
@@ -633,18 +649,18 @@ Proof.
   rewrite (match_parent_locset _ _ STACKS).
   econstructor; eauto.
 
-  (* Lbuiltin *)
+- (* Lbuiltin *)
   left; econstructor; split. simpl.
   apply plus_one. eapply exec_Lbuiltin; eauto.
   eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 
-  (* Lbranch *)
+- (* Lbranch *)
   assert ((reachable f)!!pc = true). apply REACH; simpl; auto.
   right; split. simpl; omega. split. auto. simpl. econstructor; eauto.
 
-  (* Lcond *)
+- (* Lcond *)
   assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto).
   assert (REACH2: (reachable f)!!pc2 = true) by (apply REACH; simpl; auto).
   simpl linearize_block.
@@ -670,18 +686,18 @@ Proof.
   apply plus_one. eapply exec_Lcond_false. eauto. eauto.
   econstructor; eauto.
 
-  (* Ljumptable *)
+- (* Ljumptable *)
   assert (REACH': (reachable f)!!pc = true).
     apply REACH. simpl. eapply list_nth_z_in; eauto.
   right; split. simpl; omega. split. auto. econstructor; eauto.
 
-  (* Lreturn *)
+- (* Lreturn *)
   left; econstructor; split.
   simpl. apply plus_one. econstructor; eauto.
   rewrite (stacksize_preserved _ _ TRF). eauto.
   rewrite (match_parent_locset _ _ STACKS). econstructor; eauto.
 
-  (* internal functions *)
+- (* internal functions *)
   assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true).
     apply reachable_entrypoint.
   monadInv H7.
@@ -691,13 +707,13 @@ Proof.
   generalize EQ; intro EQ'; monadInv EQ'. simpl.
   econstructor; eauto. simpl. eapply is_tail_add_branch. constructor.
 
-  (* external function *)
+- (* external function *)
   monadInv H8. left; econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 
-  (* return *)
+- (* return *)
   inv H3. inv H1.
   left; econstructor; split.
   apply plus_one. econstructor.
-- 
cgit 


From c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 11:19:22 +0200
Subject: more proofs going through

---
 backend/Allocation.v     | 24 +++++++++++++-----------
 backend/Bounds.v         |  6 +++---
 backend/Debugvar.v       |  2 +-
 backend/LTL.v            | 19 ++++++++++++++++---
 backend/Linear.v         | 23 ++++++++++++++++++++---
 backend/Linearize.v      |  4 ++--
 backend/Lineartyping.v   | 16 +++++++++++++++-
 backend/RTL.v            |  2 --
 backend/Tunnelingproof.v | 25 +++++++++++++++++++++++++
 9 files changed, 95 insertions(+), 26 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocation.v b/backend/Allocation.v
index c2e80f1c..2fa3fc0b 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -58,19 +58,19 @@ Inductive block_shape: Type :=
          (mv2: moves) (s: node)
   | BSopdead (op: operation) (args: list reg) (res: reg)
          (mv: moves) (s: node)
-  | BSload (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg)
+  | BSload (trap : trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg)
          (mv1: moves) (args': list mreg) (dst': mreg)
          (mv2: moves) (s: node)
   | BSloaddead (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg)
          (mv: moves) (s: node)
-  | BSload2 (addr1 addr2: addressing) (args: list reg) (dst: reg)
+  | BSload2 (trap : trapping_mode) (addr1 addr2: addressing) (args: list reg) (dst: reg)
          (mv1: moves) (args1': list mreg) (dst1': mreg)
          (mv2: moves) (args2': list mreg) (dst2': mreg)
          (mv3: moves) (s: node)
-  | BSload2_1 (addr: addressing) (args: list reg) (dst: reg)
+  | BSload2_1 (trap : trapping_mode) (addr: addressing) (args: list reg) (dst: reg)
          (mv1: moves) (args': list mreg) (dst': mreg)
          (mv2: moves) (s: node)
-  | BSload2_2 (addr addr': addressing) (args: list reg) (dst: reg)
+  | BSload2_2 (trap : trapping_mode) (addr addr': addressing) (args: list reg) (dst: reg)
          (mv1: moves) (args': list mreg) (dst': mreg)
          (mv2: moves) (s: node)
   | BSstore (chunk: memory_chunk) (addr: addressing) (args: list reg) (src: reg)
@@ -229,32 +229,34 @@ Definition pair_instr_block
   | Iload trap chunk addr args dst s =>
       let (mv1, b1) := extract_moves nil b in
       match b1 with
-      | Lload chunk' addr' args' dst' :: b2 =>
+      | Lload trap' chunk' addr' args' dst' :: b2 =>
+        assertion (trapping_mode_eq trap' trap);
           if chunk_eq chunk Mint64 && Archi.splitlong then
             assertion (chunk_eq chunk' Mint32);
             let (mv2, b3) := extract_moves nil b2 in
             match b3 with
-            | Lload chunk'' addr'' args'' dst'' :: b4 =>
+            | Lload trap'' chunk'' addr'' args'' dst'' :: b4 =>
+              assertion (trapping_mode_eq trap'' trap);
                 let (mv3, b5) := extract_moves nil b4 in
                 assertion (chunk_eq chunk'' Mint32);
                 assertion (eq_addressing addr addr');
                 assertion (option_eq eq_addressing (offset_addressing addr 4) (Some addr''));
                 assertion (check_succ s b5);
-                Some(BSload2 addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s)
+                Some(BSload2 trap addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s)
             | _ =>
                 assertion (check_succ s b3);
                 if (eq_addressing addr addr') then
-                  Some(BSload2_1 addr args dst mv1 args' dst' mv2 s)
+                  Some(BSload2_1 trap addr args dst mv1 args' dst' mv2 s)
                 else
                  (assertion (option_eq eq_addressing (offset_addressing addr 4) (Some addr'));
-                  Some(BSload2_2 addr addr' args dst mv1 args' dst' mv2 s))
+                  Some(BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s))
             end
           else (
             let (mv2, b3) := extract_moves nil b2 in
             assertion (chunk_eq chunk chunk');
             assertion (eq_addressing addr addr');
             assertion (check_succ s b3);
-            Some(BSload chunk addr args dst mv1 args' dst' mv2 s))
+            Some(BSload trap chunk addr args dst mv1 args' dst' mv2 s))
       | _ =>
           assertion (check_succ s b1);
           Some(BSloaddead chunk addr args dst mv1 s)
@@ -1023,7 +1025,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
   | BSopdead op args res mv s =>
       assertion (reg_unconstrained res e);
       track_moves env mv e
-  | BSload chunk addr args dst mv1 args' dst' mv2 s =>
+  | BSload trap chunk addr args dst mv1 args' dst' mv2 s =>
       do e1 <- track_moves env mv2 e;
       do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1;
       track_moves env mv1 e2
diff --git a/backend/Bounds.v b/backend/Bounds.v
index fa695234..b8c12166 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -67,7 +67,7 @@ Definition instr_within_bounds (i: instruction) :=
   | Lgetstack sl ofs ty r => slot_within_bounds sl ofs ty /\ mreg_within_bounds r
   | Lsetstack r sl ofs ty => slot_within_bounds sl ofs ty
   | Lop op args res => mreg_within_bounds res
-  | Lload chunk addr args dst => mreg_within_bounds dst
+  | Lload trap chunk addr args dst => mreg_within_bounds dst
   | Lcall sig ros => size_arguments sig <= bound_outgoing b
   | Lbuiltin ef args res =>
        (forall r, In r (params_of_builtin_res res) \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r)
@@ -104,7 +104,7 @@ Definition record_regs_of_instr (u: RegSet.t) (i: instruction) : RegSet.t :=
   | Lgetstack sl ofs ty r => record_reg u r
   | Lsetstack r sl ofs ty => record_reg u r
   | Lop op args res => record_reg u res
-  | Lload chunk addr args dst => record_reg u dst
+  | Lload trap chunk addr args dst => record_reg u dst
   | Lstore chunk addr args src => u
   | Lcall sig ros => u
   | Ltailcall sig ros => u
@@ -280,7 +280,7 @@ Definition defined_by_instr (r': mreg) (i: instruction) :=
   match i with
   | Lgetstack sl ofs ty r => r' = r
   | Lop op args res => r' = res
-  | Lload chunk addr args dst => r' = dst
+  | Lload trap chunk addr args dst => r' = dst
   | Lbuiltin ef args res => In r' (params_of_builtin_res res) \/ In r' (destroyed_by_builtin ef)
   | _ => False
   end.
diff --git a/backend/Debugvar.v b/backend/Debugvar.v
index 1f361030..56908855 100644
--- a/backend/Debugvar.v
+++ b/backend/Debugvar.v
@@ -233,7 +233,7 @@ Definition transfer (lm: labelmap) (before: option avail) (i: instruction):
           (lm, Some (kill (S sl ofs ty) s))
       | Lop op args dst =>
           (lm, Some (kill (R dst) s))
-      | Lload chunk addr args dst =>
+      | Lload trap chunk addr args dst =>
           (lm, Some (kill (R dst) s))
       | Lstore chunk addr args src =>
           (lm, before)
diff --git a/backend/LTL.v b/backend/LTL.v
index 5e7eec8c..ee8b4826 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -29,7 +29,7 @@ Definition node := positive.
 
 Inductive instruction: Type :=
   | Lop (op: operation) (args: list mreg) (res: mreg)
-  | Lload (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg)
+  | Lload (trap : trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg)
   | Lgetstack (sl: slot) (ofs: Z) (ty: typ) (dst: mreg)
   | Lsetstack (src: mreg) (sl: slot) (ofs: Z) (ty: typ)
   | Lstore (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg)
@@ -209,11 +209,24 @@ Inductive step: state -> trace -> state -> Prop :=
       rs' = Locmap.set (R res) v (undef_regs (destroyed_by_op op) rs) ->
       step (Block s f sp (Lop op args res :: bb) rs m)
         E0 (Block s f sp bb rs' m)
-  | exec_Lload: forall s f sp chunk addr args dst bb rs m a v rs',
+  | exec_Lload: forall s f sp trap chunk addr args dst bb rs m a v rs',
       eval_addressing ge sp addr (reglist rs args) = Some a ->
       Mem.loadv chunk m a = Some v ->
       rs' = Locmap.set (R dst) v (undef_regs (destroyed_by_load chunk addr) rs) ->
-      step (Block s f sp (Lload chunk addr args dst :: bb) rs m)
+      step (Block s f sp (Lload trap chunk addr args dst :: bb) rs m)
+        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)
+                       (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)
+                       (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_Lgetstack: forall s f sp sl ofs ty dst bb rs m rs',
       rs' = Locmap.set (R dst) (rs (S sl ofs ty)) (undef_regs (destroyed_by_getstack sl) rs) ->
diff --git a/backend/Linear.v b/backend/Linear.v
index 447c6ba6..1443f795 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -28,7 +28,7 @@ Inductive instruction: Type :=
   | Lgetstack: slot -> Z -> typ -> mreg -> instruction
   | Lsetstack: mreg -> slot -> Z -> typ -> instruction
   | Lop: operation -> list mreg -> mreg -> instruction
-  | Lload: memory_chunk -> addressing -> list mreg -> mreg -> instruction
+  | Lload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Lcall: signature -> mreg + ident -> instruction
   | Ltailcall: signature -> mreg + ident -> instruction
@@ -160,11 +160,28 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Lop op args res :: b) rs m)
         E0 (State s f sp b rs' m)
   | exec_Lload:
-      forall s f sp chunk addr args dst b rs m a v rs',
+      forall s f sp trap chunk addr args dst b rs m a v rs',
       eval_addressing ge sp addr (reglist rs args) = Some a ->
       Mem.loadv chunk m a = Some v ->
       rs' = Locmap.set (R dst) v (undef_regs (destroyed_by_load chunk addr) rs) ->
-      step (State s f sp (Lload chunk addr args dst :: b) rs m)
+      step (State s f sp (Lload trap chunk addr args dst :: b) rs m)
+        E0 (State s f sp b rs' m)
+  | exec_Lload_notrap1:
+      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)
+                       (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)
+  | exec_Lload_notrap2:
+      forall s f sp chunk addr args dst b 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)
+                       (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)
   | exec_Lstore:
       forall s f sp chunk addr args src b rs m m' a rs',
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 2cfa4d3c..4216958c 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -163,8 +163,8 @@ Fixpoint linearize_block (b: LTL.bblock) (k: code) : code :=
   | nil => k
   | LTL.Lop op args res :: b' =>
       Lop op args res :: linearize_block b' k
-  | LTL.Lload chunk addr args dst :: b' =>
-      Lload chunk addr args dst :: linearize_block b' k
+  | LTL.Lload trap chunk addr args dst :: b' =>
+      Lload trap chunk addr args dst :: linearize_block b' k
   | LTL.Lgetstack sl ofs ty dst :: b' =>
       Lgetstack sl ofs ty dst :: linearize_block b' k
   | LTL.Lsetstack src sl ofs ty :: b' =>
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 1fe23a9d..da66b6ff 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -76,7 +76,7 @@ Definition wt_instr (i: instruction) : bool :=
           let (targs, tres) := type_of_operation op in
           subtype tres (mreg_type res)
       end
-  | Lload chunk addr args dst =>
+  | Lload trap chunk addr args dst =>
       subtype (type_of_chunk chunk) (mreg_type dst)
   | Ltailcall sg ros =>
       zeq (size_arguments sg) 0
@@ -332,6 +332,20 @@ Local Opaque mreg_type.
   apply wt_setreg. eapply Val.has_subtype; eauto.
   destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
   apply wt_undef_regs; auto.
+- (* load notrap1 *)
+  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 *)
   simpl in *; InvBooleans.
   econstructor. eauto. eauto. eauto.
diff --git a/backend/RTL.v b/backend/RTL.v
index 95fa1f82..29a49311 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -195,8 +195,6 @@ 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
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 4f95ac9b..d3b8a9f0 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -441,6 +441,31 @@ Proof.
   rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
   eauto. eauto.
   econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
+- (* Lload notrap1 *)
+  exploit eval_addressing_lessdef_none. apply reglist_lessdef; eauto. eassumption.
+  left; simpl; econstructor; split.
+  eapply exec_Lload_notrap1.
+  rewrite <- H0.
+  apply eval_addressing_preserved. exact symbols_preserved. eauto.
+  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
+- (* Lload notrap2 *)
+  exploit eval_addressing_lessdef. apply reglist_lessdef; eauto. eauto. 
+  intros (ta & EV & LD).
+  destruct (Mem.loadv chunk tm ta) eqn:Htload.
+  {
+  left; simpl; econstructor; split.
+  eapply exec_Lload.
+  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
+  exact Htload. eauto.
+  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
+  }
+  {
+  left; simpl; econstructor; split.
+  eapply exec_Lload_notrap2.
+  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
+  exact Htload. eauto.
+  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
+  }
 - (* Lgetstack *)
   left; simpl; econstructor; split.
   econstructor; eauto.
-- 
cgit 


From fb09457f928fd4f19cd89a1fe22246444e3a5f4a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 11:26:52 +0200
Subject: some more proofs on notrap

---
 backend/CleanupLabelsproof.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'backend')

diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index e92be2b4..84ca403e 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -255,6 +255,18 @@ Proof.
   left; econstructor; split.
   econstructor; eauto.
   econstructor; eauto with coqlib.
+(* Lload notrap1 *)
+  assert (eval_addressing tge sp addr (LTL.reglist rs args) = None).
+    rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  left; econstructor; split.
+  eapply exec_Lload_notrap1; eauto.
+  econstructor; eauto with coqlib.
+(* Lload notrap2 *)
+  assert (eval_addressing tge sp addr (LTL.reglist rs args) = Some a).
+    rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  left; econstructor; split.
+  eapply exec_Lload_notrap2; eauto.
+  econstructor; eauto with coqlib.
 (* Lstore *)
   assert (eval_addressing tge sp addr (LTL.reglist rs args) = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
-- 
cgit 


From 42a4bac600c0eaa552b66659f2c67d2f8b44cdf6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 11:49:55 +0200
Subject: more proof

---
 backend/Debugvarproof.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'backend')

diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
index d31c63ec..95020637 100644
--- a/backend/Debugvarproof.v
+++ b/backend/Debugvarproof.v
@@ -449,6 +449,22 @@ Proof.
   eauto. eauto.
   apply eval_add_delta_ranges. traceEq.
   constructor; auto.
+- (* load notrap1 *)
+  econstructor; split.
+  eapply plus_left.
+  eapply exec_Lload_notrap1.
+  rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved.
+  eauto. eauto.
+  apply eval_add_delta_ranges. traceEq.
+  constructor; auto.
+- (* load notrap2 *)
+  econstructor; split.
+  eapply plus_left.
+  eapply exec_Lload_notrap2.
+  rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved.
+  eauto. eauto.
+  apply eval_add_delta_ranges. traceEq.
+  constructor; auto.
 - (* store *)
   econstructor; split.
   eapply plus_left.
-- 
cgit 


From 4284ab56c71cd64ebf6ce22ad13d3cd5533ac7ed Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 12:10:11 +0200
Subject: more on notrap

---
 backend/Mach.v     | 19 ++++++++++++++++---
 backend/Stacking.v |  4 ++--
 2 files changed, 18 insertions(+), 5 deletions(-)

(limited to 'backend')

diff --git a/backend/Mach.v b/backend/Mach.v
index 9fdee9eb..1c6fdb18 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -56,7 +56,7 @@ Inductive instruction: Type :=
   | Msetstack: mreg -> ptrofs -> typ -> instruction
   | Mgetparam: ptrofs -> typ -> mreg -> instruction
   | Mop: operation -> list mreg -> mreg -> instruction
-  | Mload: memory_chunk -> addressing -> list mreg -> mreg -> instruction
+  | Mload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
   | Mcall: signature -> mreg + ident -> instruction
   | Mtailcall: signature -> mreg + ident -> instruction
@@ -321,11 +321,24 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mop op args res :: c) rs m)
         E0 (State s f sp c rs' m)
   | exec_Mload:
-      forall s f sp chunk addr args dst c rs m a v rs',
+      forall s f sp trap chunk addr args dst c rs m a v rs',
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = Some v ->
       rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) ->
-      step (State s f sp (Mload chunk addr args dst :: c) rs m)
+      step (State s f sp (Mload trap chunk addr args dst :: c) rs m)
+        E0 (State s f sp c rs' m)
+  | 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)) ->
+      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)) ->
+      step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m)
         E0 (State s f sp c rs' m)
   | exec_Mstore:
       forall s f sp chunk addr args src c rs m m' a rs',
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 7b382d05..0e3f2832 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -133,8 +133,8 @@ Definition transl_instr
       end
   | Lop op args res =>
       Mop (transl_op fe op) args res :: k
-  | Lload chunk addr args dst =>
-      Mload chunk (transl_addr fe addr) args dst :: k
+  | Lload trap chunk addr args dst =>
+      Mload trap chunk (transl_addr fe addr) args dst :: k
   | Lstore chunk addr args src =>
       Mstore chunk (transl_addr fe addr) args src :: k
   | Lcall sig ros =>
-- 
cgit 


From 339d7e5ff093a2002aa8c939aece10bafe2914d7 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 13:16:05 +0200
Subject: more proofs

---
 backend/Stackingproof.v | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'backend')

diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 326fab61..1d4a93e7 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1918,6 +1918,45 @@ Proof.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
   apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
 
+- (* Lload notrap1*)
+  assert (eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = None) as Haddress.
+  eapply eval_addressing_inject_none; eauto.
+  eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
+  eapply agree_reglist; eauto.
+  econstructor; split.
+  apply plus_one. apply exec_Mload_notrap1.
+  rewrite <- Haddress. apply eval_addressing_preserved. exact symbols_preserved.
+  eauto. econstructor; eauto with coqlib.
+  apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
+  apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
+  
+- (* Lload notrap2 *)
+  assert (exists a',
+          eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
+       /\ Val.inject j a a').
+  eapply eval_addressing_inject; eauto.
+  eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
+  eapply agree_reglist; eauto.
+  destruct H1 as [a' [A B]].
+
+  destruct ( Mem.loadv chunk m' a') as [v'|] eqn:Hloadv.
+  {
+  econstructor; split.
+  apply plus_one. apply exec_Mload with (a:=a') (v:=v'); eauto.
+  rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  econstructor; eauto with coqlib.
+  apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
+  apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
+  }
+  {
+  econstructor; split.
+  apply plus_one. apply exec_Mload_notrap2 with (a:=a'); eauto.
+  rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  econstructor; eauto with coqlib.
+  apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
+  apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
+  }
+
 - (* Lstore *)
   assert (exists a',
           eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
-- 
cgit 


From f9feebf866ec62fc57cb6e7deea9864b65945f16 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 14:08:52 +0200
Subject: moving forward with proofs

---
 backend/Allocation.v | 14 +++++++-------
 backend/Allocproof.v | 44 ++++++++++++++++++++++----------------------
 2 files changed, 29 insertions(+), 29 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 2fa3fc0b..c1fbf90d 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -1029,7 +1029,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       do e1 <- track_moves env mv2 e;
       do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1;
       track_moves env mv1 e2
-  | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s =>
+  | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s =>
       do e1 <- track_moves env mv3 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in
       assertion (loc_unconstrained (R dst2') e2);
@@ -1042,14 +1042,14 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       assertion (reg_unconstrained dst e5);
       do e6 <- add_equations args args1' e5;
       track_moves env mv1 e6
-  | BSload2_1 addr args dst mv1 args' dst' mv2 s =>
+  | BSload2_1 trap addr args dst mv1 args' dst' mv2 s =>
       do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr) e2);
       do e3 <- add_equations args args' e2;
       track_moves env mv1 e3
-  | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s =>
+  | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s =>
       do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
@@ -1265,10 +1265,10 @@ Definition successors_block_shape (bsh: block_shape) : list node :=
   | BShighlong src dst mv s => s :: nil
   | BSop op args res mv1 args' res' mv2 s => s :: nil
   | BSopdead op args res mv s => s :: nil
-  | BSload chunk addr args dst mv1 args' dst' mv2 s => s :: nil
-  | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil
-  | BSload2_1 addr args dst mv1 args' dst' mv2 s => s :: nil
-  | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => s :: nil
+  | BSload trap chunk addr args dst mv1 args' dst' mv2 s => s :: nil
+  | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil
+  | BSload2_1 trap addr args dst mv1 args' dst' mv2 s => s :: nil
+  | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s => s :: nil
   | BSloaddead chunk addr args dst mv s => s :: nil
   | BSstore chunk addr args src mv1 args' src' s => s :: nil
   | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s => s :: nil
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index ac4122bc..428bcc0e 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -98,37 +98,37 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr
                          (expand_moves mv (Lbranch 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)
+      expand_block_shape (BSload trap chunk addr args dst mv1 args' dst' mv2 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,
+                           (Lload trap chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k)))
+  | ebs_load2: forall trap addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k,
       wf_moves mv1 -> wf_moves mv2 -> wf_moves mv3 ->
       Archi.splitlong = true ->
       offset_addressing addr 4 = Some addr2 ->
-      expand_block_shape (BSload2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s)
-                         (Iload Mint64 addr args dst s)
+      expand_block_shape (BSload2 trap addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s)
+                         (Iload trap Mint64 addr args dst s)
                          (expand_moves mv1
-                           (Lload Mint32 addr args1' dst1' ::
+                           (Lload trap Mint32 addr args1' dst1' ::
                            expand_moves mv2
-                             (Lload Mint32 addr2 args2' dst2' ::
+                             (Lload trap Mint32 addr2 args2' dst2' ::
                               expand_moves mv3 (Lbranch s :: k))))
-  | ebs_load2_1: forall addr args dst mv1 args' dst' mv2 s k,
+  | ebs_load2_1: forall trap addr args dst mv1 args' dst' mv2 s k,
       wf_moves mv1 -> wf_moves mv2 ->
       Archi.splitlong = true ->
-      expand_block_shape (BSload2_1 addr args dst mv1 args' dst' mv2 s)
-                         (Iload Mint64 addr args dst s)
+      expand_block_shape (BSload2_1 trap addr args dst mv1 args' dst' mv2 s)
+                         (Iload trap Mint64 addr args dst s)
                          (expand_moves mv1
-                           (Lload Mint32 addr args' dst' ::
+                           (Lload trap Mint32 addr args' dst' ::
                             expand_moves mv2 (Lbranch s :: k)))
-  | ebs_load2_2: forall addr addr2 args dst mv1 args' dst' mv2 s k,
+  | ebs_load2_2: forall trap addr addr2 args dst mv1 args' dst' mv2 s k,
       wf_moves mv1 -> wf_moves mv2 ->
       Archi.splitlong = true ->
       offset_addressing addr 4 = Some addr2 ->
-      expand_block_shape (BSload2_2 addr addr2 args dst mv1 args' dst' mv2 s)
-                         (Iload Mint64 addr args dst s)
+      expand_block_shape (BSload2_2 trap addr addr2 args dst mv1 args' dst' mv2 s)
+                         (Iload trap Mint64 addr args dst s)
                          (expand_moves mv1
-                           (Lload Mint32 addr2 args' dst' ::
+                           (Lload trap Mint32 addr2 args' dst' ::
                             expand_moves mv2 (Lbranch s :: k)))
   | ebs_load_dead: forall trap chunk addr args dst mv s k,
       wf_moves mv ->
@@ -1970,8 +1970,8 @@ Ltac UseShape :=
   end.
 
 Remark addressing_not_long:
-  forall env f addr args dst s r,
-  wt_instr f env (Iload Mint64 addr args dst s) -> Archi.splitlong = true ->
+  forall trap env f addr args dst s r,
+  wt_instr f env (Iload trap Mint64 addr args dst s) -> Archi.splitlong = true ->
   In r args -> r <> dst.
 Proof.
   intros. inv H.
@@ -1981,7 +1981,7 @@ Proof.
   { rewrite <- H5. apply in_map; auto. }
   assert (C: env r = Tint).
   { apply A in B. rewrite B. unfold Tptr. rewrite Archi.splitlong_ptr32 by auto. auto. }
-  red; intros; subst r. rewrite C in H8; discriminate.
+  red; intros; subst r. rewrite C in H9; discriminate.
 Qed.
 
 (** The proof of semantic preservation is a simulation argument of the
@@ -2083,7 +2083,7 @@ Proof.
   eapply wt_exec_Iop; eauto.
 
 (* load regular *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
@@ -2100,7 +2100,7 @@ Proof.
   econstructor; eauto.
 
 (* load pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
@@ -2155,7 +2155,7 @@ Proof.
   econstructor; eauto.
 
 (* load first word of a pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
@@ -2185,7 +2185,7 @@ Proof.
   econstructor; eauto.
 
 (* load second word of a pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
-- 
cgit 


From 3db304d599b7edf4ac77eb74c9b37e765b25bbd3 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 16:51:08 +0200
Subject: BSload notrap1

---
 backend/Allocproof.v | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 428bcc0e..fce54563 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -2082,7 +2082,7 @@ Proof.
   econstructor; eauto.
   eapply wt_exec_Iop; eauto.
 
-(* load regular *)
+(* load regular TRAP *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
   exploit transfer_use_def_satisf; eauto. intros [X Y].
@@ -2229,6 +2229,24 @@ Proof.
   econstructor; eauto.
   eapply wt_exec_Iload; eauto.
 
+- (* BSload notrap1 *)
+  generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS).
+  intro WTRS'.
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit transfer_use_def_satisf; eauto. intros [X Y].
+  exploit eval_addressing_lessdef_none; eauto. intro Haddr.
+  exploit (exec_moves mv2); eauto.  intros [ls2 [A2 B2]].
+  econstructor; split.
+  eapply plus_left. econstructor; eauto.
+  eapply star_trans. eexact A1.
+  eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr.
+  apply eval_addressing_preserved. exact symbols_preserved. eauto.
+  
+  eapply star_right. eexact A2. constructor.
+  eauto. eauto. eauto. traceEq.
+  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
+  econstructor; eauto.
+  
 (* store *)
 - exploit exec_moves; eauto. intros [ls1 [X Y]].
   exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD.
-- 
cgit 


From 8e03466a1a2e7bbc9057ac76ee18deda990dc884 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 23:26:38 +0200
Subject: progress in proof

---
 backend/Allocproof.v | 41 +++++++++++++++++++++++++++--------------
 1 file changed, 27 insertions(+), 14 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index fce54563..44dda4ac 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -102,33 +102,33 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr
                          (Iload trap chunk addr args dst s)
                          (expand_moves mv1
                            (Lload trap chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k)))
-  | ebs_load2: forall trap addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k,
+  | ebs_load2: forall addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k,
       wf_moves mv1 -> wf_moves mv2 -> wf_moves mv3 ->
       Archi.splitlong = true ->
       offset_addressing addr 4 = Some addr2 ->
-      expand_block_shape (BSload2 trap addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s)
-                         (Iload trap Mint64 addr args dst s)
+      expand_block_shape (BSload2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s)
+                         (Iload TRAP Mint64 addr args dst s)
                          (expand_moves mv1
-                           (Lload trap Mint32 addr args1' dst1' ::
+                           (Lload TRAP Mint32 addr args1' dst1' ::
                            expand_moves mv2
-                             (Lload trap Mint32 addr2 args2' dst2' ::
+                             (Lload TRAP Mint32 addr2 args2' dst2' ::
                               expand_moves mv3 (Lbranch s :: k))))
-  | ebs_load2_1: forall trap addr args dst mv1 args' dst' mv2 s k,
+  | ebs_load2_1: forall addr args dst mv1 args' dst' mv2 s k,
       wf_moves mv1 -> wf_moves mv2 ->
       Archi.splitlong = true ->
-      expand_block_shape (BSload2_1 trap addr args dst mv1 args' dst' mv2 s)
-                         (Iload trap Mint64 addr args dst s)
+      expand_block_shape (BSload2_1 addr args dst mv1 args' dst' mv2 s)
+                         (Iload TRAP Mint64 addr args dst s)
                          (expand_moves mv1
-                           (Lload trap Mint32 addr args' dst' ::
+                           (Lload TRAP Mint32 addr args' dst' ::
                             expand_moves mv2 (Lbranch s :: k)))
-  | ebs_load2_2: forall trap addr addr2 args dst mv1 args' dst' mv2 s k,
+  | ebs_load2_2: forall addr addr2 args dst mv1 args' dst' mv2 s k,
       wf_moves mv1 -> wf_moves mv2 ->
       Archi.splitlong = true ->
       offset_addressing addr 4 = Some addr2 ->
-      expand_block_shape (BSload2_2 trap addr addr2 args dst mv1 args' dst' mv2 s)
-                         (Iload trap Mint64 addr args dst s)
+      expand_block_shape (BSload2_2 addr addr2 args dst mv1 args' dst' mv2 s)
+                         (Iload TRAP Mint64 addr args dst s)
                          (expand_moves mv1
-                           (Lload trap Mint32 addr2 args' dst' ::
+                           (Lload TRAP Mint32 addr2 args' dst' ::
                             expand_moves mv2 (Lbranch s :: k)))
   | ebs_load_dead: forall trap chunk addr args dst mv s k,
       wf_moves mv ->
@@ -2246,7 +2246,20 @@ Proof.
   eauto. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
   econstructor; eauto.
-  
+
+(* BSload notrap dead? *)
+- exploit exec_moves; eauto. intros [ls1 [X Y]].
+  econstructor; split.
+  eapply plus_left. econstructor; eauto.
+  eapply star_right. eexact X. econstructor; eauto.
+  eauto. traceEq.
+  exploit satisf_successors. eauto. eauto. simpl; eauto. eauto.
+  eapply reg_unconstrained_satisf; eauto.
+  intros [enext [U V]].
+  econstructor; eauto.
+  eapply wt_exec_Iload_notrap; eauto.
+
+
 (* store *)
 - exploit exec_moves; eauto. intros [ls1 [X Y]].
   exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD.
-- 
cgit 


From e64b9464fb6662bf63ac255eca94d17d572c9d81 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 6 Sep 2019 22:33:46 +0200
Subject: ONE "admitted" and things compile

---
 backend/Allocation.v   | 28 +++++++++++++++-------------
 backend/Allocproof.v   | 37 ++++++++++++++++++++++++++++++++++---
 backend/Inliningaux.ml |  2 +-
 backend/PrintLTL.ml    |  7 ++++---
 backend/PrintMach.ml   |  5 +++--
 backend/PrintRTL.ml    |  7 ++++---
 backend/PrintXTL.ml    |  7 ++++---
 backend/Regalloc.ml    | 26 +++++++++++++-------------
 backend/Splitting.ml   |  4 ++--
 backend/XTL.ml         |  4 ++--
 backend/XTL.mli        |  2 +-
 11 files changed, 83 insertions(+), 46 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocation.v b/backend/Allocation.v
index c1fbf90d..6e4fcc82 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -63,14 +63,14 @@ Inductive block_shape: Type :=
          (mv2: moves) (s: node)
   | BSloaddead (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg)
          (mv: moves) (s: node)
-  | BSload2 (trap : trapping_mode) (addr1 addr2: addressing) (args: list reg) (dst: reg)
+  | BSload2 (addr1 addr2: addressing) (args: list reg) (dst: reg)
          (mv1: moves) (args1': list mreg) (dst1': mreg)
          (mv2: moves) (args2': list mreg) (dst2': mreg)
          (mv3: moves) (s: node)
-  | BSload2_1 (trap : trapping_mode) (addr: addressing) (args: list reg) (dst: reg)
+  | BSload2_1 (addr: addressing) (args: list reg) (dst: reg)
          (mv1: moves) (args': list mreg) (dst': mreg)
          (mv2: moves) (s: node)
-  | BSload2_2 (trap : trapping_mode) (addr addr': addressing) (args: list reg) (dst: reg)
+  | BSload2_2 (addr addr': addressing) (args: list reg) (dst: reg)
          (mv1: moves) (args': list mreg) (dst': mreg)
          (mv2: moves) (s: node)
   | BSstore (chunk: memory_chunk) (addr: addressing) (args: list reg) (src: reg)
@@ -232,24 +232,26 @@ Definition pair_instr_block
       | Lload trap' chunk' addr' args' dst' :: b2 =>
         assertion (trapping_mode_eq trap' trap);
           if chunk_eq chunk Mint64 && Archi.splitlong then
+            (* TODO: do not support non trapping split loads *)
+            assertion (trapping_mode_eq trap TRAP);
             assertion (chunk_eq chunk' Mint32);
             let (mv2, b3) := extract_moves nil b2 in
             match b3 with
             | Lload trap'' chunk'' addr'' args'' dst'' :: b4 =>
-              assertion (trapping_mode_eq trap'' trap);
+              assertion (trapping_mode_eq trap'' TRAP);
                 let (mv3, b5) := extract_moves nil b4 in
                 assertion (chunk_eq chunk'' Mint32);
                 assertion (eq_addressing addr addr');
                 assertion (option_eq eq_addressing (offset_addressing addr 4) (Some addr''));
                 assertion (check_succ s b5);
-                Some(BSload2 trap addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s)
+                Some(BSload2 addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s)
             | _ =>
                 assertion (check_succ s b3);
                 if (eq_addressing addr addr') then
-                  Some(BSload2_1 trap addr args dst mv1 args' dst' mv2 s)
+                  Some(BSload2_1 addr args dst mv1 args' dst' mv2 s)
                 else
                  (assertion (option_eq eq_addressing (offset_addressing addr 4) (Some addr'));
-                  Some(BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s))
+                  Some(BSload2_2 addr addr' args dst mv1 args' dst' mv2 s))
             end
           else (
             let (mv2, b3) := extract_moves nil b2 in
@@ -1029,7 +1031,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       do e1 <- track_moves env mv2 e;
       do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1;
       track_moves env mv1 e2
-  | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s =>
+  | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s =>
       do e1 <- track_moves env mv3 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in
       assertion (loc_unconstrained (R dst2') e2);
@@ -1042,14 +1044,14 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       assertion (reg_unconstrained dst e5);
       do e6 <- add_equations args args1' e5;
       track_moves env mv1 e6
-  | BSload2_1 trap addr args dst mv1 args' dst' mv2 s =>
+  | BSload2_1 addr args dst mv1 args' dst' mv2 s =>
       do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
       assertion (can_undef (destroyed_by_load Mint32 addr) e2);
       do e3 <- add_equations args args' e2;
       track_moves env mv1 e3
-  | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s =>
+  | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s =>
       do e1 <- track_moves env mv2 e;
       let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in
       assertion (reg_loc_unconstrained dst (R dst') e2);
@@ -1266,9 +1268,9 @@ Definition successors_block_shape (bsh: block_shape) : list node :=
   | BSop op args res mv1 args' res' mv2 s => s :: nil
   | BSopdead op args res mv s => s :: nil
   | BSload trap chunk addr args dst mv1 args' dst' mv2 s => s :: nil
-  | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil
-  | BSload2_1 trap addr args dst mv1 args' dst' mv2 s => s :: nil
-  | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s => s :: nil
+  | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil
+  | BSload2_1 addr args dst mv1 args' dst' mv2 s => s :: nil
+  | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => s :: nil
   | BSloaddead chunk addr args dst mv s => s :: nil
   | BSstore chunk addr args src mv1 args' src' s => s :: nil
   | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s => s :: nil
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 44dda4ac..ab6f87b0 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -2229,7 +2229,7 @@ Proof.
   econstructor; eauto.
   eapply wt_exec_Iload; eauto.
 
-- (* BSload notrap1 *)
+- (* load notrap1 *)
   generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS).
   intro WTRS'.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
@@ -2247,7 +2247,7 @@ Proof.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
   econstructor; eauto.
 
-(* BSload notrap dead? *)
+(* load notrap1 dead *)
 - exploit exec_moves; eauto. intros [ls1 [X Y]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
@@ -2259,7 +2259,38 @@ Proof.
   econstructor; eauto.
   eapply wt_exec_Iload_notrap; eauto.
 
+(* load regular notrap2 *)
+- (* exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit transfer_use_def_satisf; eauto. intros [X Y].
+  exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
+
+  econstructor; split.
+  eapply plus_left. econstructor; eauto.
+  eapply star_trans. eexact A1.
+  eapply star_left. eapply exec_Lload_notrap2 with (a := a'). rewrite <- F.
+  apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto.
+  eapply star_right. eexact A2. constructor.
+  eauto. eauto. eauto. traceEq.
+  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
+  econstructor; eauto.
+
+    generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). intro WTRS'.
+   *)
+  
+  admit.
 
+- (* load notrap2 dead *)
+  exploit exec_moves; eauto. intros [ls1 [X Y]].
+  econstructor; split.
+  eapply plus_left. econstructor; eauto.
+  eapply star_right. eexact X. econstructor; eauto.
+  eauto. traceEq.
+  exploit satisf_successors. eauto. eauto. simpl; eauto. eauto.
+  eapply reg_unconstrained_satisf; eauto.
+  intros [enext [U V]].
+  econstructor; eauto.
+  eapply wt_exec_Iload_notrap; eauto.
+  
 (* store *)
 - exploit exec_moves; eauto. intros [ls1 [X Y]].
   exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD.
@@ -2511,7 +2542,7 @@ Proof.
   eapply plus_left. constructor. eexact A. traceEq.
   econstructor; eauto.
   apply wt_regset_assign; auto. rewrite WTRES0; auto.
-Qed.
+Admitted.
 
 Lemma initial_states_simulation:
   forall st1, RTL.initial_state prog st1 ->
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
index 842e0c93..609b2637 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -57,7 +57,7 @@ let used_in_globvar io gv =
 let fun_inline_analysis id io fn =
   let inst io nid = function
     | Iop (op, args, dest, succ) -> used_id io (globals_operation op)
-    | Iload (chunk, addr, args, dest, succ)
+    | Iload (_, chunk, addr, args, dest, succ)
     | Istore (chunk, addr, args, dest, succ) -> used_id io (globals_addressing addr)
     | Ibuiltin (ef, args, dest, succ) -> used_id io (globals_of_builtin_args args)
     | Icall (_, Coq_inr cid, _, _, _)
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 1c449e74..b309a9f2 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -61,9 +61,10 @@ let print_succ pp s dfl =
 let print_instruction pp succ = function
   | Lop(op, args, res) ->
       fprintf pp "%a = %a" mreg res (print_operation mreg) (op, args)
-  | Lload(chunk, addr, args, dst) ->
-      fprintf pp "%a = %s[%a]"
-         mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args)
+  | Lload(trap,chunk, addr, args, dst) ->
+      fprintf pp "%a = %s[%a]%a"
+        mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args)
+        print_trapping_mode trap
   | Lgetstack(sl, ofs, ty, dst) ->
       fprintf pp "%a = %a" mreg dst slot (sl, ofs, ty)
   | Lsetstack(src, sl, ofs, ty) ->
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 517f3037..70e65832 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -48,10 +48,11 @@ let print_instruction pp i =
   | Mop(op, args, res) ->
       fprintf pp "\t%a = %a\n"
          reg res (PrintOp.print_operation reg) (op, args)
-  | Mload(chunk, addr, args, dst) ->
-      fprintf pp "\t%a = %s[%a]\n"
+  | Mload(trap, chunk, addr, args, dst) ->
+      fprintf pp "\t%a = %s[%a]%a\n"
          reg dst (name_of_chunk chunk)
          (PrintOp.print_addressing reg) (addr, args)
+         print_trapping_mode trap
   | Mstore(chunk, addr, args, src) ->
       fprintf pp "\t%s[%a] = %a\n"
          (name_of_chunk chunk)
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 841540b6..c25773e5 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -50,10 +50,11 @@ let print_instruction pp (pc, i) =
       fprintf pp "%a = %a\n"
          reg res (PrintOp.print_operation reg) (op, args);
       print_succ pp s (pc - 1)
-  | Iload(chunk, addr, args, dst, s) ->
-      fprintf pp "%a = %s[%a]\n"
+  | Iload(trap, chunk, addr, args, dst, s) ->
+      fprintf pp "%a = %s[%a]%a\n"
          reg dst (name_of_chunk chunk)
-         (PrintOp.print_addressing reg) (addr, args);
+         (PrintOp.print_addressing reg) (addr, args)
+         print_trapping_mode trap;
       print_succ pp s (pc - 1)
   | Istore(chunk, addr, args, src, s) ->
       fprintf pp "%s[%a] = %a\n"
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 6432682a..1c7655fb 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -86,9 +86,10 @@ let print_instruction pp succ = function
       fprintf pp "(%a) = (%a) using %a, %a" vars dsts vars srcs var t1 var t2
   | Xop(op, args, res) ->
       fprintf pp "%a = %a" var res (print_operation var) (op, args)
-  | Xload(chunk, addr, args, dst) ->
-      fprintf pp "%a = %s[%a]"
-         var dst (name_of_chunk chunk) (print_addressing var) (addr, args)
+  | Xload(trap, chunk, addr, args, dst) ->
+      fprintf pp "%a = %s[%a]%a"
+        var dst (name_of_chunk chunk) (print_addressing var) (addr, args)
+        print_trapping_mode trap
   | Xstore(chunk, addr, args, src) ->
       fprintf pp "%s[%a] = %a"
          (name_of_chunk chunk) (print_addressing var) (addr, args) var src
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 7db8a866..f2658b04 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -249,18 +249,18 @@ let block_of_RTL_instr funsig tyenv = function
             else
               let t = new_temp (tyenv res) in (t :: args2', t) in
       movelist args1 args3 (Xop(op, args3, res3) :: move res3 res1 [Xbranch s])
-  | RTL.Iload(chunk, addr, args, dst, s) ->
+  | RTL.Iload(trap, chunk, addr, args, dst, s) ->
       if Archi.splitlong && chunk = Mint64 then begin
         match offset_addressing addr (coqint_of_camlint 4l) with
         | None -> assert false
         | Some addr' ->
-            [Xload(Mint32, addr, vregs tyenv args,
+            [Xload(trap, Mint32, addr, vregs tyenv args,
                    V((if Archi.big_endian then dst else twin_reg dst), Tint));
-             Xload(Mint32, addr', vregs tyenv args,
+             Xload(trap, Mint32, addr', vregs tyenv args,
                    V((if Archi.big_endian then twin_reg dst else dst), Tint));
              Xbranch s]
       end else
-        [Xload(chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s]
+        [Xload(trap, chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s]
   | RTL.Istore(chunk, addr, args, src, s) ->
       if Archi.splitlong && chunk = Mint64 then begin
         match offset_addressing addr (coqint_of_camlint 4l) with
@@ -364,7 +364,7 @@ let live_before instr after =
       if VSet.mem res after
       then vset_addlist args (VSet.remove res after)
       else after
-  | Xload(chunk, addr, args, dst) ->
+  | Xload(trap, chunk, addr, args, dst) ->
       if VSet.mem dst after
       then vset_addlist args (VSet.remove dst after)
       else after
@@ -459,7 +459,7 @@ let dce_instr instr after k =
       if VSet.mem res after
       then instr :: k
       else k
-  | Xload(chunk, addr, args, dst) ->
+  | Xload(trap, chunk, addr, args, dst) ->
       if VSet.mem dst after
       then instr :: k
       else k
@@ -550,7 +550,7 @@ let spill_costs f =
         (* temps must not be spilled *)
     | Xop(op, args, res) ->
         charge_list 10 1 args; charge 10 1 res
-    | Xload(chunk, addr, args, dst) ->
+    | Xload(trap, chunk, addr, args, dst) ->
         charge_list 10 1 args; charge 10 1 dst
     | Xstore(chunk, addr, args, src) ->
         charge_list 10 1 args; charge 10 1 src
@@ -677,7 +677,7 @@ let add_interfs_instr g instr live =
             (vset_addlist (res :: argl) (VSet.remove res live))
       end;
       add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op)
-  | Xload(chunk, addr, args, dst) ->
+  | Xload(trap, chunk, addr, args, dst) ->
       add_interfs_def g dst live;
       add_interfs_destroyed g (VSet.remove dst live)
                               (destroyed_by_load chunk addr)
@@ -782,7 +782,7 @@ let tospill_instr alloc instr ts =
       ts
   | Xop(op, args, res) ->
       addlist_tospill alloc args (add_tospill alloc res ts)
-  | Xload(chunk, addr, args, dst) ->
+  | Xload(trap, chunk, addr, args, dst) ->
       addlist_tospill alloc args (add_tospill alloc dst ts)
   | Xstore(chunk, addr, args, src) ->
       addlist_tospill alloc args (add_tospill alloc src ts)
@@ -964,10 +964,10 @@ let spill_instr tospill eqs instr =
                add res tmp (kill tmp (kill res eqs2)))
           end
       end
-  | Xload(chunk, addr, args, dst) ->
+  | Xload(trap, chunk, addr, args, dst) ->
       let (args', c1, eqs1) = reload_vars tospill eqs args in
       let (dst', c2, eqs2) = save_var tospill eqs1 dst in
-      (c1 @ Xload(chunk, addr, args', dst') :: c2, eqs2)
+      (c1 @ Xload(trap, chunk, addr, args', dst') :: c2, eqs2)
   | Xstore(chunk, addr, args, src) ->
       let (args', c1, eqs1) = reload_vars tospill eqs args in
       let (src', c2, eqs2) = reload_var tospill eqs1 src in
@@ -1115,8 +1115,8 @@ let transl_instr alloc instr k =
             LTL.Lop(Omove, [rarg1], rres) ::
             LTL.Lop(op, rres :: rargl, rres) :: k
       end
-  | Xload(chunk, addr, args, dst) ->
-      LTL.Lload(chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k
+  | Xload(trap, chunk, addr, args, dst) ->
+      LTL.Lload(trap, chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k
   | Xstore(chunk, addr, args, src) ->
       LTL.Lstore(chunk, addr, mregs_of alloc args, mreg_of alloc src) :: k
   | Xcall(sg, vos, args, res) ->
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 40f09c3d..78eb66a5 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -151,8 +151,8 @@ let ren_instr f maps pc i =
   | Inop s -> Inop s
   | Iop(op, args, res, s) ->
       Iop(op, ren_regs before args, ren_reg after res, s)
-  | Iload(chunk, addr, args, dst, s) ->
-      Iload(chunk, addr, ren_regs before args, ren_reg after dst, s)
+  | Iload(trap, chunk, addr, args, dst, s) ->
+      Iload(trap, chunk, addr, ren_regs before args, ren_reg after dst, s)
   | Istore(chunk, addr, args, src, s) ->
       Istore(chunk, addr, ren_regs before args, ren_reg before src, s)
   | Icall(sg, ros, args, res, s) ->
diff --git a/backend/XTL.ml b/backend/XTL.ml
index f10efeed..c496fafb 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -30,7 +30,7 @@ type instruction =
   | Xspill of var * var
   | Xparmove of var list * var list * var * var
   | Xop of operation * var list * var
-  | Xload of memory_chunk * addressing * var list * var
+  | Xload of trapping_mode * memory_chunk * addressing * var list * var
   | Xstore of memory_chunk * addressing * var list * var
   | Xcall of signature * (var, ident) sum * var list * var list
   | Xtailcall of signature * (var, ident) sum * var list
@@ -159,7 +159,7 @@ let type_instr = function
       let (targs, tres) = type_of_operation op in
       set_vars_type args targs;
       set_var_type res tres
-  | Xload(chunk, addr, args, dst) ->
+  | Xload(trap, chunk, addr, args, dst) ->
       set_vars_type args (type_of_addressing addr);
       set_var_type dst (type_of_chunk chunk)
   | Xstore(chunk, addr, args, src) ->
diff --git a/backend/XTL.mli b/backend/XTL.mli
index 54988d4b..b4b77fab 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -31,7 +31,7 @@ type instruction =
   | Xspill of var * var
   | Xparmove of var list * var list * var * var
   | Xop of operation * var list * var
-  | Xload of memory_chunk * addressing * var list * var
+  | Xload of trapping_mode * memory_chunk * addressing * var list * var
   | Xstore of memory_chunk * addressing * var list * var
   | Xcall of signature * (var, ident) sum * var list * var list
   | Xtailcall of signature * (var, ident) sum * var list
-- 
cgit 


From f2831013b46d0486e5e134f26fde9ece7b78ff93 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 7 Sep 2019 09:49:58 +0200
Subject: more for passing notrap through x86

---
 backend/Constpropproof.v | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'backend')

diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index eb4b6f17..dca36b4e 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -452,7 +452,8 @@ Proof.
 
 - (* Iload notrap1 *)
   rename pc'0 into pc. TransfInstr.
-  assert (eval_static_addressing addr (aregs ae args) = Vbot) as Hbot by (eapply eval_static_addressing_sound_none; eauto with va).
+  destruct (eval_static_addressing addr (aregs ae args)) eqn:Hstatic.
+  {
   assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr rs' ## args = None) as Hnone.
   rewrite eval_addressing_preserved with (ge1 := ge).
   apply eval_addressing_lessdef_none with (vl1 := rs ## args).
@@ -463,7 +464,14 @@ Proof.
   left; econstructor; econstructor; split.
   eapply exec_Iload_notrap1; eauto.
   eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
-
+  }
+  { exploit eval_static_addressing_sound; eauto.
+  rewrite eval_addressing_preserved with (ge1 := ge).
+  apply eval_addressing_lessdef with (vl1 := rs ## args).
+  apply regs_lessdef_regs; assumption.
+  assumption.
+  exact symbols_preserved.
+  }
 - (* Iload notrap2 *)
   rename pc'0 into pc. TransfInstr.
     assert (exists v2 : val,
-- 
cgit 


From 046c24d29796a3bb130c94fe464e54e8a7aa2eb3 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 7 Sep 2019 10:11:56 +0200
Subject: notrap works on x86

---
 backend/Constpropproof.v | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'backend')

diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index dca36b4e..2e43a93f 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -452,10 +452,8 @@ Proof.
 
 - (* Iload notrap1 *)
   rename pc'0 into pc. TransfInstr.
-  destruct (eval_static_addressing addr (aregs ae args)) eqn:Hstatic.
-  {
-  assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr rs' ## args = None) as Hnone.
-  rewrite eval_addressing_preserved with (ge1 := ge).
+  assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) =  None).
+  rewrite eval_addressing_preserved with (ge1 := ge); eauto.
   apply eval_addressing_lessdef_none with (vl1 := rs ## args).
   apply regs_lessdef_regs; assumption.
   assumption.
@@ -464,14 +462,7 @@ Proof.
   left; econstructor; econstructor; split.
   eapply exec_Iload_notrap1; eauto.
   eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
-  }
-  { exploit eval_static_addressing_sound; eauto.
-  rewrite eval_addressing_preserved with (ge1 := ge).
-  apply eval_addressing_lessdef with (vl1 := rs ## args).
-  apply regs_lessdef_regs; assumption.
-  assumption.
-  exact symbols_preserved.
-  }
+
 - (* Iload notrap2 *)
   rename pc'0 into pc. TransfInstr.
     assert (exists v2 : val,
-- 
cgit 


From 35febfa5b231a71234a1b32c128169352e96eaca Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 7 Sep 2019 12:27:43 +0200
Subject: fixes for ARM

---
 backend/CSEproof.v       | 12 +++---------
 backend/Constpropproof.v | 12 ++++--------
 backend/Inliningproof.v  |  4 ++--
 backend/Stackingproof.v  |  5 +++--
 4 files changed, 12 insertions(+), 21 deletions(-)

(limited to 'backend')

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 684729d4..209fa40f 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1151,9 +1151,7 @@ Proof.
 
     econstructor. split.
     eapply exec_Iload; eauto.
-    rewrite eval_addressing_preserved with (ge1 := ge).
-    exact Ha'1.
-    exact symbols_preserved.
+    try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption).
 
     econstructor; eauto.
     eapply analysis_correct_1; eauto. simpl; eauto.
@@ -1204,9 +1202,7 @@ Proof.
     {
       econstructor. split.
       eapply exec_Iload; eauto.
-      rewrite eval_addressing_preserved with (ge1 := ge).
-      exact Ha'1.
-      exact symbols_preserved.
+      try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption).
       
       econstructor; eauto.
       eapply analysis_correct_1; eauto. simpl; eauto.
@@ -1220,9 +1216,7 @@ Proof.
     {
       econstructor. split.
       eapply exec_Iload_notrap2; eauto.
-      rewrite eval_addressing_preserved with (ge1 := ge).
-      exact Ha'1.
-      exact symbols_preserved.
+      try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption).
       
       econstructor; eauto.
       eapply analysis_correct_1; eauto. simpl; eauto.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 2e43a93f..4d104141 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -444,8 +444,8 @@ Proof.
     destruct (Mem.loadv_extends chunk m m' a v2 v MEM H1 Hlessdef2) as [vX [Hvx1 Hvx2]].
     left; econstructor; econstructor; split.
     eapply exec_Iload with (a := v2); eauto.
-    erewrite eval_addressing_preserved with (ge1:=ge); auto.
-    exact symbols_preserved.
+    try (erewrite eval_addressing_preserved with (ge1:=ge); auto;
+    exact symbols_preserved).
   eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
     
   }
@@ -476,18 +476,14 @@ Proof.
     left; econstructor; econstructor; split.
     eapply exec_Iload; eauto.
    
-    rewrite eval_addressing_preserved with (ge1 := ge).
-    exact Heval'.
-    exact symbols_preserved.
+    try (rewrite eval_addressing_preserved with (ge1 := ge); eassumption).
     eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
     }
     {
       left; econstructor; econstructor; split.
       eapply exec_Iload_notrap2; eauto.
    
-    rewrite eval_addressing_preserved with (ge1 := ge).
-    exact Heval'.
-    exact symbols_preserved.
+    try (rewrite eval_addressing_preserved with (ge1 := ge); eassumption).
     eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
     }
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 588d7165..ebc48160 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -1017,7 +1017,7 @@ Proof.
   + left; econstructor; split.
     eapply plus_one.
     eapply exec_Iload; eauto.
-    rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
+    try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved).
     econstructor; eauto.
   apply match_stacks_inside_set_reg; auto.
   apply agree_set_reg; auto.
@@ -1025,7 +1025,7 @@ Proof.
   + left; econstructor; split.
     eapply plus_one.
     eapply exec_Iload_notrap2; eauto.
-    rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
+    try (rewrite <- P; apply eval_addressing_preserved; assumption).
     econstructor; eauto.
   apply match_stacks_inside_set_reg; auto.
   apply agree_set_reg; auto.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 1d4a93e7..19a40e0f 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1943,7 +1943,7 @@ Proof.
   {
   econstructor; split.
   apply plus_one. apply exec_Mload with (a:=a') (v:=v'); eauto.
-  rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  try (rewrite <- A; apply eval_addressing_preserved; assumption).
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
   apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
@@ -1951,7 +1951,8 @@ Proof.
   {
   econstructor; split.
   apply plus_one. apply exec_Mload_notrap2 with (a:=a'); eauto.
-  rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  try (rewrite <- A; apply eval_addressing_preserved; assumption).
+  
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
   apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
-- 
cgit 


From 4cdd085383c5e18989b8636455ddcfc7ceb5843a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 7 Sep 2019 13:12:39 +0200
Subject: fixes for compiling on other platforms

---
 backend/CSEproof.v       | 6 +++---
 backend/Constpropproof.v | 4 ++--
 backend/Inliningproof.v  | 2 +-
 backend/Stackingproof.v  | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'backend')

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 209fa40f..5bbb7508 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1151,7 +1151,7 @@ Proof.
 
     econstructor. split.
     eapply exec_Iload; eauto.
-    try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption).
+    try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
 
     econstructor; eauto.
     eapply analysis_correct_1; eauto. simpl; eauto.
@@ -1202,7 +1202,7 @@ Proof.
     {
       econstructor. split.
       eapply exec_Iload; eauto.
-      try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption).
+      try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
       
       econstructor; eauto.
       eapply analysis_correct_1; eauto. simpl; eauto.
@@ -1216,7 +1216,7 @@ Proof.
     {
       econstructor. split.
       eapply exec_Iload_notrap2; eauto.
-      try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption).
+      try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
       
       econstructor; eauto.
       eapply analysis_correct_1; eauto. simpl; eauto.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 4d104141..63cfee24 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -476,14 +476,14 @@ Proof.
     left; econstructor; econstructor; split.
     eapply exec_Iload; eauto.
    
-    try (rewrite eval_addressing_preserved with (ge1 := ge); eassumption).
+    try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
     eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
     }
     {
       left; econstructor; econstructor; split.
       eapply exec_Iload_notrap2; eauto.
    
-    try (rewrite eval_addressing_preserved with (ge1 := ge); eassumption).
+    try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
     eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
     }
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index ebc48160..b60c1cb7 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -1025,7 +1025,7 @@ Proof.
   + left; econstructor; split.
     eapply plus_one.
     eapply exec_Iload_notrap2; eauto.
-    try (rewrite <- P; apply eval_addressing_preserved; assumption).
+    try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved).
     econstructor; eauto.
   apply match_stacks_inside_set_reg; auto.
   apply agree_set_reg; auto.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 19a40e0f..d3fcdb91 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1943,7 +1943,7 @@ Proof.
   {
   econstructor; split.
   apply plus_one. apply exec_Mload with (a:=a') (v:=v'); eauto.
-  try (rewrite <- A; apply eval_addressing_preserved; assumption).
+  try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved).
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
   apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
@@ -1951,7 +1951,7 @@ Proof.
   {
   econstructor; split.
   apply plus_one. apply exec_Mload_notrap2 with (a:=a'); eauto.
-  try (rewrite <- A; apply eval_addressing_preserved; assumption).
+  try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved).
   
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
-- 
cgit 


From 6fa6e763ba241da7eeb8bd309344a118c6b1ec4a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sun, 8 Sep 2019 18:20:31 +0200
Subject: finished the proofs for non-trapping loads

---
 backend/Allocproof.v | 31 +++++++++++++++++++++----------
 1 file changed, 21 insertions(+), 10 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index ab6f87b0..3d8fb451 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -2260,25 +2260,36 @@ Proof.
   eapply wt_exec_Iload_notrap; eauto.
 
 (* load regular notrap2 *)
-- (* exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+- generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS).
+  intro WTRS'.
+  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
-
-  econstructor; split.
+  destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload.
+  { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto.  intros [ls2 [A2 B2]].
+      econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_trans. eexact A1.
-  eapply star_left. eapply exec_Lload_notrap2 with (a := a'). rewrite <- F.
+  eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F.
   apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto.
   eapply star_right. eexact A2. constructor.
   eauto. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
   econstructor; eauto.
-
-    generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). intro WTRS'.
-   *)
+  }
+  { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto.  intros [ls2 [A2 B2]].
+  econstructor; split.
+  eapply plus_left. econstructor; eauto.
+  eapply star_trans. eexact A1.
+  eapply star_left. eapply exec_Lload_notrap2. rewrite <- F.
+  apply eval_addressing_preserved. exact symbols_preserved. assumption.
+  eauto.
+  eapply star_right. eexact A2. constructor.
+  eauto. eauto. eauto. traceEq.
+  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
+  econstructor; eauto.
+  }
   
-  admit.
-
 - (* load notrap2 dead *)
   exploit exec_moves; eauto. intros [ls1 [X Y]].
   econstructor; split.
@@ -2542,7 +2553,7 @@ Proof.
   eapply plus_left. constructor. eexact A. traceEq.
   econstructor; eauto.
   apply wt_regset_assign; auto. rewrite WTRES0; auto.
-Admitted.
+Qed.
 
 Lemma initial_states_simulation:
   forall st1, RTL.initial_state prog st1 ->
-- 
cgit 


From 3696063f6645297402b7136dba5c4b6d9277d88c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 9 Sep 2019 21:33:21 +0200
Subject: proof for Allnontrap

---
 backend/Allnontrapproof.v | 215 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 215 insertions(+)
 create mode 100644 backend/Allnontrapproof.v

(limited to 'backend')

diff --git a/backend/Allnontrapproof.v b/backend/Allnontrapproof.v
new file mode 100644
index 00000000..92e5a88c
--- /dev/null
+++ b/backend/Allnontrapproof.v
@@ -0,0 +1,215 @@
+Require Import FunInd.
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import Allnontrap.
+
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_transf TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_ptr_transf TRANSL).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_transf TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; reflexivity.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  unfold find_function; intros. destruct ros as [r|id].
+  eapply functions_translated; eauto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+Lemma transf_function_at:
+  forall f pc i,
+  f.(fn_code)!pc = Some i ->
+  (transf_function f).(fn_code)!pc = Some(transf_instr pc i).
+Proof.
+  intros until i. intro Hcode.
+  unfold transf_function; simpl.
+  rewrite PTree.gmap.
+  unfold option_map.
+  rewrite Hcode.
+  reflexivity.
+Qed.
+
+Ltac TR_AT :=
+  match goal with
+  | [ A: (fn_code _)!_ = Some _ |- _ ] =>
+        generalize (transf_function_at _ _ _ A); intros
+  end.
+
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+  | match_frames_intro: forall res f sp pc rs,
+      match_frames (Stackframe res f sp pc rs)
+                   (Stackframe res (transf_function f) sp pc rs).
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp pc rs m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | match_returnstates: forall stk v m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v m).
+
+Lemma step_simulation:
+  forall S1 t S2, RTL.step ge S1 t S2 ->
+  forall S1', match_states S1 S1' ->
+  exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
+Proof.
+  induction 1; intros S1' MS; inv MS; try TR_AT.
+- (* nop *)
+  econstructor; split. eapply exec_Inop; eauto.
+  constructor; auto.
+- (* op *)
+  econstructor; split.
+  eapply exec_Iop with (v := v); eauto.
+  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  constructor; auto.
+(* load *)
+- econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Iload; eauto.
+  constructor; 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.
+- (* 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. 
+- (* store *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs ## args = Some a).
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Istore; eauto.
+  constructor; auto. 
+(* call *)
+- econstructor; split.
+  eapply exec_Icall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. constructor; auto. constructor.
+(* tailcall *)
+- econstructor; split.
+  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+    apply sig_preserved.
+  constructor. auto.
+(* builtin *)
+- econstructor; split.
+  eapply exec_Ibuiltin; eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+(* cond *)
+- econstructor; split.
+  eapply exec_Icond; eauto.
+  constructor; auto.
+(* jumptbl *)
+- econstructor; split.
+  eapply exec_Ijumptable; eauto.
+  constructor; auto.
+(* return *)
+- econstructor; split.
+  eapply exec_Ireturn; eauto.
+  constructor; auto.
+(* internal function *)
+-  simpl. econstructor; split.
+  eapply exec_function_internal; eauto.
+  constructor; auto.
+(* external function *)
+- econstructor; split.
+  eapply exec_function_external; eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+(* return *)
+- inv STACKS. inv H1.
+  econstructor; split.
+  eapply exec_return; eauto.
+  constructor; auto.
+Qed.
+
+Lemma transf_initial_states:
+  forall S1, RTL.initial_state prog S1 ->
+  exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
+Proof.
+  intros. inv H. econstructor; split.
+  econstructor.
+    eapply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
+    eapply function_ptr_translated; eauto.
+    rewrite <- H3; apply sig_preserved.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_step.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
+Qed.
+
+End PRESERVATION.
-- 
cgit 


From 1b44cdee7eef4e31f2fc6b8a2397017c2979f6d9 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 9 Sep 2019 23:02:43 +0200
Subject: missing file

---
 backend/Allnontrap.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 backend/Allnontrap.v

(limited to 'backend')

diff --git a/backend/Allnontrap.v b/backend/Allnontrap.v
new file mode 100644
index 00000000..acf03eca
--- /dev/null
+++ b/backend/Allnontrap.v
@@ -0,0 +1,26 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+
+
+Definition transf_ros (ros: reg + ident) : reg + ident := ros.
+
+Definition transf_instr (pc: node) (instr: instruction) :=
+  match instr with
+  | Iload trap chunk addr args dst s => Iload NOTRAP chunk addr args dst s
+  | _ => instr
+  end.
+
+Definition transf_function (f: function) : function :=
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := PTree.map transf_instr f.(fn_code);
+     fn_entrypoint := f.(fn_entrypoint) |}.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
+
-- 
cgit 


From e2341e779ca6bf734b9ed103156949db588fbbdc Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 26 Nov 2019 07:38:20 +0100
Subject: Duplicateproof: minor edit

---
 backend/Duplicateproof.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'backend')

diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 9d56e86f..39b7a353 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -344,15 +344,16 @@ Proof.
   intros. inv H.
   exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
   eexists. split.
-  - econstructor.
+  - econstructor; eauto.
     + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
     + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
       symmetry. eapply match_program_main. eauto.
-    + exploit function_ptr_translated; eauto.
     + destruct f.
       * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption.
       * monadInv TRANSF. assumption.
-  - constructor; eauto. constructor. apply transf_fundef_correct; auto.
+  - constructor; eauto.
+    + constructor. 
+    + apply transf_fundef_correct; auto.
 Qed.
 
 Theorem transf_final_states:
-- 
cgit 


From 553714035fc08f9b145b89b3dd7c455f06e917df Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Dec 2019 21:39:20 +0100
Subject: finish merge

---
 backend/Duplicate.v      | 24 +++++++++++++-----------
 backend/Duplicateproof.v | 20 ++++++++++++++++++--
 backend/Lineartyping.v   |  2 +-
 3 files changed, 32 insertions(+), 14 deletions(-)

(limited to 'backend')

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 3ad37c83..46f0855d 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -72,17 +72,19 @@ Definition verify_match_inst dupmap inst tinst :=
           else Error(msg "Different operations in Iop")
       | _ => Error(msg "verify_match_inst Inop") end
 
-  | Iload m a lr r n => match tinst with
-      | Iload m' a' lr' r' n' =>
+  | Iload tm m a lr r n => match tinst with
+      | Iload tm' m' a' lr' r' n' =>
           do u <- verify_is_copy dupmap n n';
-          if (chunk_eq m m') then
-            if (eq_addressing a a') then
-              if (list_eq_dec Pos.eq_dec lr lr') then
-                if (Pos.eq_dec r r') then OK tt
-                else Error (msg "Different r in Iload")
-              else Error (msg "Different lr in Iload")
-            else Error (msg "Different addressing in Iload")
-          else Error (msg "Different mchunk in Iload")
+          if (trapping_mode_eq tm tm') then
+            if (chunk_eq m m') then
+              if (eq_addressing a a') then
+                if (list_eq_dec Pos.eq_dec lr lr') then
+                  if (Pos.eq_dec r r') then OK tt
+                  else Error (msg "Different r in Iload")
+                else Error (msg "Different lr in Iload")
+              else Error (msg "Different addressing in Iload")
+            else Error (msg "Different mchunk in Iload")
+          else Error (msg "Different trapping_mode in Iload")
       | _ => Error (msg "verify_match_inst Iload") end
 
   | Istore m a lr r n => match tinst with
@@ -195,4 +197,4 @@ Definition transf_fundef (f: fundef) : res fundef :=
   transf_partial_fundef transf_function f.
 
 Definition transf_program (p: program) : res program :=
-  transform_partial_program transf_fundef p.
\ No newline at end of file
+  transform_partial_program transf_fundef p.
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 39b7a353..e66a1068 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -13,8 +13,8 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop
       dupmap!n' = (Some n) -> match_inst dupmap (Inop n) (Inop n')
   | match_inst_op: forall n n' op lr r,
       dupmap!n' = (Some n) -> match_inst dupmap (Iop op lr r n) (Iop op lr r n')
-  | match_inst_load: forall n n' m a lr r,
-      dupmap!n' = (Some n) -> match_inst dupmap (Iload m a lr r n) (Iload m a lr r n')
+  | match_inst_load: forall n n' tm m a lr r,
+      dupmap!n' = (Some n) -> match_inst dupmap (Iload tm m a lr r n) (Iload tm m a lr r n')
   | match_inst_store: forall n n' m a lr r,
       dupmap!n' = (Some n) -> match_inst dupmap (Istore m a lr r n) (Istore m a lr r n')
   | match_inst_call: forall n n' s ri lr r,
@@ -137,6 +137,7 @@ Proof.
 (* Iload *)
   - destruct i'; try (inversion H; fail). monadInv H.
     destruct x. eapply verify_is_copy_correct in EQ.
+    destruct (trapping_mode_eq _ _); try discriminate.
     destruct (chunk_eq _ _); try discriminate.
     destruct (eq_addressing _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
@@ -393,6 +394,21 @@ Proof.
     eexists. split.
     + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto.
     + econstructor; eauto.
+(* Iload notrap1 *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Iload_notrap1; eauto. erewrite eval_addressing_preserved; eauto.
+    + econstructor; eauto.
+(* Iload notrap2 *)
+  - eapply dupmap_correct in DUPLIC; eauto.
+    destruct DUPLIC as (i' & H2 & H3). inv H3.
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    + eapply exec_Iload_notrap2; eauto. erewrite eval_addressing_preserved; eauto.
+    + econstructor; eauto.
+      
 (* Istore *)
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 994d2652..3fe61470 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -328,7 +328,7 @@ Local Opaque mreg_type.
     change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
     red; intros; subst op. simpl in ISMOVE.
     destruct args; try discriminate. destruct args; discriminate.
-    apply wt_undef_regs; auto.
+    (* no longer needed apply wt_undef_regs; auto. *)
 - (* load *)
   simpl in *; InvBooleans.
   econstructor; eauto.
-- 
cgit 


From e2c64b54bf5df0927c684a70167378c91cba0ff4 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 6 Dec 2019 13:49:48 +0100
Subject: make it compile for ARM

---
 backend/Duplicateproof.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'backend')

diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index e66a1068..ebb17774 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -392,21 +392,21 @@ Proof.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
-    + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto.
+    + eapply exec_Iload; eauto; (* is the follow still needed?*) erewrite eval_addressing_preserved; eauto.
     + econstructor; eauto.
 (* Iload notrap1 *)
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
-    + eapply exec_Iload_notrap1; eauto. erewrite eval_addressing_preserved; eauto.
+    + eapply exec_Iload_notrap1; eauto; erewrite eval_addressing_preserved; eauto. 
     + econstructor; eauto.
 (* Iload notrap2 *)
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
-    + eapply exec_Iload_notrap2; eauto. erewrite eval_addressing_preserved; eauto.
+    + eapply exec_Iload_notrap2; eauto; erewrite eval_addressing_preserved; eauto.
     + econstructor; eauto.
       
 (* Istore *)
@@ -414,7 +414,7 @@ Proof.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES.
     eexists. split.
-    + eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto.
+    + eapply exec_Istore; eauto; erewrite eval_addressing_preserved; eauto.
     + econstructor; eauto.
 (* Icall *)
   - eapply dupmap_correct in DUPLIC; eauto.
-- 
cgit