Add dynamically checked assumption to simplify Asmgenproof

Previously Asmblock.label_pos and Asm.label_pos could point to different
memory location for the same label.

1 files changed, 23 insertions, 9 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index a3b21a88..08ad176a 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -315,15 +315,29 @@ Definition unfold_exit (oc: option control) :=
 
 Definition unfold_bblock (bb: bblock) :=
   let lbl := unfold_label (header bb) in
-  do rest <- (match (body bb), (exit bb) with
-              | (((Asmblock.Pfreeframe _ _
-              | Asmblock.Pallocframe _ _)::nil) as bo), None =>
-                unfold_body bo
-              | bo, ex =>
-                do bo_is <- unfold_body bo;
-                OK (bo_is ++ unfold_exit ex)
-              end)
-  ; OK (lbl ++ rest).
+    (*
+     * With this dynamically checked assumption on a previous optimization we
+     * can show that [Asmblock.label_pos] and [Asm.label_pos] retrieve the same
+     * exact address. Maintaining this property allows us to use the simple
+     * formulation of match_states defined as equality.
+     * Otherwise we would have to deal with the case of a basic block header
+     * that has multiple labels. Asmblock.label_pos will, for all labels, point
+     * to the same location at the beginning of the basic block. Asm.label_pos
+     * on the other hand could return a position pointing into the original
+     * basic block.
+     *)
+  if zle (list_length_z (header bb)) 1 then
+    do rest <- (match (body bb), (exit bb) with
+                | (((Asmblock.Pfreeframe _ _
+                | Asmblock.Pallocframe _ _)::nil) as bo), None =>
+                  unfold_body bo
+                | bo, ex =>
+                  do bo_is <- unfold_body bo;
+                  OK (bo_is ++ unfold_exit ex)
+                end)
+    ; OK (lbl ++ rest)
+  else
+    Error (msg "Asmgen.unfold_bblock: Multiple labels were generated.").
 
 Fixpoint unfold (bbs: Asmblock.bblocks) : res Asm.code :=
   match bbs with