diff options
-rw-r--r-- | aarch64/Asm.v | 2 | ||||
-rw-r--r-- | aarch64/Asmgen.v | 32 |
2 files changed, 24 insertions, 10 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 369e6f3b..dc1faddd 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -240,7 +240,7 @@ Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z := match c with | nil => None | instr :: c' => - if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c' + if is_label lbl instr then Some pos else label_pos lbl (pos + 1) c' end. Definition nextinstr (rs: regset) := 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 |