From f6ad93e7cbbb3e43b045ae3313e556ea70e54c8f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 3 May 2019 17:28:30 +0100
Subject: 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.
---
 language/jib.ott | 42 +++++++++++++++++++++++++-----------------
 1 file changed, 25 insertions(+), 17 deletions(-)

(limited to 'language')

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
-- 
cgit v1.2.3