diff options
Diffstat (limited to 'aarch64/Asmgen.v')
-rw-r--r-- | aarch64/Asmgen.v | 32 |
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 |