more on notrap

3 files changed, 19 insertions, 4 deletions

diff --git a/mppa_k1c/lib/Machblock.v b/mppa_k1c/lib/Machblock.v
index 2759c49d..5a7f1782 100644
--- a/mppa_k1c/lib/Machblock.v
+++ b/mppa_k1c/lib/Machblock.v
@@ -20,7 +20,7 @@ Inductive basic_inst: Type :=
   | MBsetstack: mreg -> ptrofs -> typ -> basic_inst
   | MBgetparam: ptrofs -> typ -> mreg -> basic_inst
   | MBop: operation -> list mreg -> mreg -> basic_inst
-  | MBload: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
+  | MBload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
   | MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
   .
 
@@ -207,11 +207,22 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:
       rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) ->
       basic_step s fb sp rs m (MBop op args res) rs' m
   | exec_MBload:
-      forall addr args a v rs' chunk dst,
+      forall addr args a v rs' trap chunk dst,
       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) ->
-      basic_step s fb sp rs m (MBload chunk addr args dst) rs' m
+      basic_step s fb sp rs m (MBload trap chunk addr args dst) rs' m
+  | exec_MBload_notrap1:
+      forall addr args rs' chunk dst,
+      eval_addressing ge sp addr rs##args = None ->
+      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+      basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
+  | exec_MBload_notrap2:
+      forall addr args a rs' chunk dst,
+      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)) ->
+      basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
   | exec_MBstore:
       forall chunk addr args src m' a rs',
       eval_addressing ge sp addr rs##args = Some a ->
diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v
index db48934e..a65b218f 100644
--- a/mppa_k1c/lib/Machblockgen.v
+++ b/mppa_k1c/lib/Machblockgen.v
@@ -33,7 +33,7 @@ Definition trans_inst (i:Mach.instruction) : Machblock_inst :=
   | Msetstack src ofs ty          => MB_basic (MBsetstack src ofs ty)
   | Mgetparam ofs ty dst          => MB_basic (MBgetparam ofs ty dst)
   | Mop       op args res         => MB_basic (MBop       op args res)
-  | Mload     chunk addr args dst => MB_basic (MBload     chunk addr args dst)
+  | Mload trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst)
   | Mstore    chunk addr args src => MB_basic (MBstore    chunk addr args src)
   | Mlabel l => MB_label l
   end.
diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v
index 9186e54a..77db094d 100644
--- a/mppa_k1c/lib/Machblockgenproof.v
+++ b/mppa_k1c/lib/Machblockgenproof.v
@@ -483,6 +483,10 @@ Proof.
     unfold Genv.symbol_address; rewrite symbols_preserved; auto.
   - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
     unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+  - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
+    unfold Genv.symbol_address; rewrite symbols_preserved; auto.
   - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
     unfold Genv.symbol_address; rewrite symbols_preserved; auto.
 Qed.