diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-29 12:39:03 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-29 12:39:03 +0200 |
| commit | 05273f381d89d86c25d94f1b54b09fd6868db2ec (patch) | |
| tree | 7a60355a68963a76d9dcc09a15e66f1dd35fba2e /aarch64/Asmgen.v | |
| parent | d1d387fefe010c7e397368b09ffaf01b905300c3 (diff) | |
| download | compcert-kvx-05273f381d89d86c25d94f1b54b09fd6868db2ec.tar.gz compcert-kvx-05273f381d89d86c25d94f1b54b09fd6868db2ec.zip | |
Simplify unfold_bblock and complete unfold_body's case in find_instr_bblock
The previous version of unfold_bblock was copied from kvx/Asm.v. kvx's
version is slightly different in that for the (here removed) special
case it does not put a semicolon to separate bundles. Since aarch64 does
not have kvx's bundles the two versions should be equivalent.
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 0124bf63..e1a38c45 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -327,15 +327,8 @@ Definition unfold_bblock (bb: bblock) := * 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) + do bo_is <- unfold_body (body bb); + OK (lbl ++ bo_is ++ unfold_exit (exit bb)) else Error (msg "Asmgen.unfold_bblock: Multiple labels were generated."). |