Builtin mem spec in scheduler and some needed proof in Postpasssch.v

3 files changed, 6 insertions, 5 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 25b9c5c5..4297cfd8 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -1088,7 +1088,7 @@ Definition trans_control (ctl: control) : inst :=
                     (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil));
                     (#X16, Op (Constant Vundef) Enil);
                     (#X17, Op (Constant Vundef) Enil)]
-  | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
+  | Pbuiltin ef args res => []
   end.
 
 Definition trans_exit (ex: option control) : L.inst :=
@@ -2637,7 +2637,7 @@ End SECT_BBLOCK_EQUIV.
 (** REWRITE RULES *)
 
 Definition is_constant (o: op): bool :=
-  match o with
+  match o with (* TODO *)
   | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ => true
   | _ => false
   end.
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v
index c84b327b..a9473789 100644
--- a/aarch64/PostpassScheduling.v
+++ b/aarch64/PostpassScheduling.v
@@ -336,8 +336,9 @@ Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : re
   | Some c => OK {| header := nil; body := lb; exit := Some c |}
   end.
 Next Obligation.
-  (* TODO *)
-Admitted.
+  unfold Is_true, AB.non_empty_bblockb.
+  unfold AB.non_empty_exit. rewrite orb_true_r. reflexivity.
+Qed.
 
 Definition do_schedule (bb: bblock) : res bblock :=
   if (Z.eqb (size bb) 1) then OK (bb) 
diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml
index 886519b2..821a1d53 100644
--- a/aarch64/PostpassSchedulingOracle.ml
+++ b/aarch64/PostpassSchedulingOracle.ml
@@ -462,7 +462,7 @@ let builtin_rec ef args res =
   (* XXX verify this *)
   {
     inst = builtin_real;
-    write_locs = [];
+    write_locs = [ Mem ];
     read_locs = [ Mem ];
     is_control = true;
   }