From a779d35bad9faf3bbfc5bf898565256bd40edf33 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 30 Mar 2020 22:17:12 +0200
Subject: lemma on stepping through non trapping instructions

---
 backend/Inject.v | 28 ++++++++++++++++++----------
 1 file changed, 18 insertions(+), 10 deletions(-)

(limited to 'backend/Inject.v')

diff --git a/backend/Inject.v b/backend/Inject.v
index 6da10019..6ef32ccb 100644
--- a/backend/Inject.v
+++ b/backend/Inject.v
@@ -81,20 +81,28 @@ Definition inject prog extra_pc injections : code :=
 Section INJECTOR.
   Variable gen_injections : function -> PTree.t (list inj_instr).
 
+  Definition valid_injection_instr (max_reg : reg) (i : inj_instr) :=
+    match i with
+    | INJop op args res => (max_reg <? res) && (negb (is_trapping_op op)
+       && (Datatypes.length args =? args_of_operation op)%nat) 
+    | INJload _ _ _ res => max_reg <? res
+    end.
+  
+  Definition valid_injections1 max_pc max_reg :=
+    List.forallb
+         (fun injection =>
+            ((fst injection) <=? max_pc) &&
+            (List.forallb (valid_injection_instr max_reg) (snd injection))
+         ).
+
+  Definition valid_injections f :=
+    valid_injections1 (max_pc_function f) (max_reg_function f).
+  
   Definition transf_function (f : function) : res function :=
     let injections := PTree.elements (gen_injections f) in
     let max_pc := max_pc_function f in
     let max_reg := max_reg_function f in
-    if List.forallb
-         (fun injection =>
-            ((fst injection) <=? max_pc) &&
-            (List.forallb
-               (fun (i : inj_instr) =>
-                  (match i with
-                   | INJop _ _ res => res
-                   | INJload _ _ _ res => res
-                   end) <=? max_reg) (snd injection))
-         ) injections
+    if valid_injections1 max_pc max_reg injections
     then
       OK {| fn_sig := f.(fn_sig);
             fn_params := f.(fn_params);
-- 
cgit