diff options
| author | Alasdair Armstrong | 2019-05-03 17:28:30 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-03 17:28:30 +0100 |
| commit | f6ad93e7cbbb3e43b045ae3313e556ea70e54c8f (patch) | |
| tree | c6f1bc2e499046cb7e5c22f750e0e63162f6d253 /language | |
| parent | c7a3389c34eebac4fed7764f339f4cd1b2b204f7 (diff) | |
Jib: Fix optimizations for SMT IR changes
Fixes C backend optimizations that were disabled due to changes in the
IR while working on the SMT generation.
Also add a -Oaarch64_fast option that optimizes any integer within a
struct to be an int64_t, which is safe for the ARM v8.5 spec and
improves performance significantly (reduces Linux boot times by 4-5
minutes). Eventually this should probably be a directive that can be
attached to any arbitrary struct/type.
Fixes the -c_specialize option for ARM v8.5. However this only gives a
very small performance improvment for a very large increase in
compilation time however.
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 42 |
1 files changed, 25 insertions, 17 deletions
diff --git a/language/jib.ott b/language/jib.ott index 4ab0e22e..058c50d2 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -57,25 +57,33 @@ name :: '' ::= | return nat :: :: return op :: '' ::= - | not :: :: bnot - | hd :: :: list_hd - | tl :: :: list_tl - | bit_to_bool :: :: bit_to_bool - | eq :: :: eq - | neq :: :: neq + | not :: :: bnot + | hd :: :: list_hd + | tl :: :: list_tl + | bit_to_bool :: :: bit_to_bool + | eq :: :: eq + | neq :: :: neq % Integer ops - | lt :: :: ilt - | lteq :: :: ilteq - | gt :: :: igt - | gteq :: :: igteq - | add :: :: iadd - | sub :: :: isub + | lt :: :: ilt + | lteq :: :: ilteq + | gt :: :: igt + | gteq :: :: igteq + | add :: :: iadd + | sub :: :: isub % Bitvector ops - | bvor :: :: bvor - | bvand :: :: bvand - | concat :: :: concat - | zero_extend nat :: :: zero_extend - | sign_extend nat :: :: sign_extend + | bvnot :: :: bvnot + | bvor :: :: bvor + | bvand :: :: bvand + | bvxor :: :: bvxor + | bvadd :: :: bvadd + | bvsub :: :: bvsub + | bvaccess :: :: bvaccess + | concat :: :: concat + | zero_extend nat :: :: zero_extend + | sign_extend nat :: :: sign_extend + | slice nat :: :: slice + | sslice nat :: :: sslice + | replicate nat :: :: replicate cval :: 'V_' ::= | name : ctyp :: :: id |