oracle simplification, BTL printer, and error msg spec

1 files changed, 41 insertions, 41 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 9fdf39be..3daa40c4 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -529,13 +529,13 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           do u <- verify_is_copy dupmap pc1 pc;
           if negb isfst then
             OK None
-          else Error (msg "verify_block: isfst is true Bgoto")
+          else Error (msg "BTL.verify_block: isfst is true Bgoto")
       | Breturn or =>
           match cfg!pc with
           | Some (Ireturn or') =>
               if option_eq Pos.eq_dec or or' then OK None
-              else Error (msg "verify_block: different opt reg in Breturn")
-          | _ => Error (msg "verify_block: incorrect cfg Breturn")
+              else Error (msg "BTL.verify_block: different opt reg in Breturn")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn")
           end
       | Bcall s ri lr r pc1 =>
           match cfg!pc with
@@ -545,11 +545,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
                 if (product_eq Pos.eq_dec ident_eq ri ri') then
                   if (list_eq_dec Pos.eq_dec lr lr') then
                     if (Pos.eq_dec r r') then OK None
-                    else Error (msg "verify_block: different r r' in Bcall")
-                  else Error (msg "verify_block: different lr in Bcall")
-                else Error (msg "verify_block: different ri in Bcall")
-              else Error (msg "verify_block: different signatures in Bcall")
-          | _ => Error (msg "verify_block: incorrect cfg Bcall")
+                    else Error (msg "BTL.verify_block: different r r' in Bcall")
+                  else Error (msg "BTL.verify_block: different lr in Bcall")
+                else Error (msg "BTL.verify_block: different ri in Bcall")
+              else Error (msg "BTL.verify_block: different signatures in Bcall")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall")
           end
       | Btailcall s ri lr =>
           match cfg!pc with
@@ -557,10 +557,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               if (signature_eq s s') then
                 if (product_eq Pos.eq_dec ident_eq ri ri') then
                   if (list_eq_dec Pos.eq_dec lr lr') then OK None
-                  else Error (msg "verify_block: different lr in Btailcall")
-                else Error (msg "verify_block: different ri in Btailcall")
-              else Error (msg "verify_block: different signatures in Btailcall")
-          | _ => Error (msg "verify_block: incorrect cfg Btailcall")
+                  else Error (msg "BTL.verify_block: different lr in Btailcall")
+                else Error (msg "BTL.verify_block: different ri in Btailcall")
+              else Error (msg "BTL.verify_block: different signatures in Btailcall")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall")
           end
       | Bbuiltin ef la br pc1 =>
           match cfg!pc with
@@ -569,24 +569,24 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               if (external_function_eq ef ef') then
                 if (list_eq_dec builtin_arg_eq_pos la la') then
                   if (builtin_res_eq_pos br br') then OK None
-                  else Error (msg "verify_block: different brr in Bbuiltin")
-                else Error (msg "verify_block: different lbar in Bbuiltin")
-              else Error (msg "verify_block: different ef in Bbuiltin")
-          | _ => Error (msg "verify_block: incorrect cfg Bbuiltin")
+                  else Error (msg "BTL.verify_block: different brr in Bbuiltin")
+                else Error (msg "BTL.verify_block: different lbar in Bbuiltin")
+              else Error (msg "BTL.verify_block: different ef in Bbuiltin")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin")
           end
       | Bjumptable r ln =>
           match cfg!pc with
           | Some (Ijumptable r' ln') =>
               do u <- verify_is_copy_list dupmap ln ln';
               if (Pos.eq_dec r r') then OK None
-              else Error (msg "verify_block: different r in Bjumptable")
-          | _ => Error (msg "verify_block: incorrect cfg Bjumptable")
+              else Error (msg "BTL.verify_block: different r in Bjumptable")
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable")
           end
       end
   | Bnop =>
       match cfg!pc with
       | Some (Inop pc') => OK (Some pc')
-      | _ => Error (msg "verify_block: incorrect cfg Bnop")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop")
       end
   | Bop op lr r =>
       match cfg!pc with
@@ -595,10 +595,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
             if (list_eq_dec Pos.eq_dec lr lr') then
               if (Pos.eq_dec r r') then
                 OK (Some pc')
-              else Error (msg "verify_block: different r in Bop")
-            else Error (msg "verify_block: different lr in Bop")
-          else Error (msg "verify_block: different operations in Bop")
-      | _ => Error (msg "verify_block: incorrect cfg Bop")
+              else Error (msg "BTL.verify_block: different r in Bop")
+            else Error (msg "BTL.verify_block: different lr in Bop")
+          else Error (msg "BTL.verify_block: different operations in Bop")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bop")
       end
   | Bload tm m a lr r =>
       match cfg!pc with
@@ -609,12 +609,12 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
                 if (list_eq_dec Pos.eq_dec lr lr') then
                   if (Pos.eq_dec r r') then
                     OK (Some pc')
-                  else Error (msg "verify_block: different r in Bload")
-                else Error (msg "verify_block: different lr in Bload")
-              else Error (msg "verify_block: different addressing in Bload")
-            else Error (msg "verify_block: different mchunk in Bload")
-          else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload")
-      | _ => Error (msg "verify_block: incorrect cfg Bload")
+                  else Error (msg "BTL.verify_block: different r in Bload")
+                else Error (msg "BTL.verify_block: different lr in Bload")
+              else Error (msg "BTL.verify_block: different addressing in Bload")
+            else Error (msg "BTL.verify_block: different mchunk in Bload")
+          else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bload")
       end
   | Bstore m a lr r =>
       match cfg!pc with
@@ -623,18 +623,18 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
             if (eq_addressing a a') then
               if (list_eq_dec Pos.eq_dec lr lr') then
                 if (Pos.eq_dec r r') then OK (Some pc')
-                else Error (msg "verify_block: different r in Bstore")
-              else Error (msg "verify_block: different lr in Bstore")
-            else Error (msg "verify_block: different addressing in Bstore")
-          else Error (msg "verify_block: different mchunk in Bstore")
-      | _ => Error (msg "verify_block: incorrect cfg Bstore")
+                else Error (msg "BTL.verify_block: different r in Bstore")
+              else Error (msg "BTL.verify_block: different lr in Bstore")
+            else Error (msg "BTL.verify_block: different addressing in Bstore")
+          else Error (msg "BTL.verify_block: different mchunk in Bstore")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore")
       end
   | Bseq b1 b2 =>
       do opc <- verify_block dupmap cfg isfst pc b1;
       match opc with
       | Some pc' =>
           verify_block dupmap cfg false pc' b2
-      | None => Error (msg "verify_block: None next pc in Bseq (deadcode)")
+      | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)")
       end
   | Bcond c lr bso bnot i =>
       match cfg!pc with
@@ -648,11 +648,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               | o, None => OK o
               | Some x, Some x' =>
                   if Pos.eq_dec x x' then OK (Some x)
-                  else Error (msg "verify_block: is_join_opt incorrect for Bcond")
+                  else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond")
               end
-            else Error (msg "verify_block: incompatible conditions in Bcond")
-          else Error (msg "verify_block: different lr in Bcond")
-      | _ => Error (msg "verify_block: incorrect cfg Bcond")
+            else Error (msg "BTL.verify_block: incompatible conditions in Bcond")
+          else Error (msg "BTL.verify_block: different lr in Bcond")
+      | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond")
       end
   end.
 
@@ -753,9 +753,9 @@ Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit :=
     | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry);
                  match o with
                  | None => verify_blocks dupmap cfg cfg' l
-                 | _ => Error(msg "verify_blocks.end")
+                 | _ => Error(msg "BTL.verify_blocks.end")
                  end
-    | _ => Error(msg "verify_blocks.entry")
+    | _ => Error(msg "BTL.verify_blocks.entry")
     end
   end.