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.
---
 src/value.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/value.ml')

diff --git a/src/value.ml b/src/value.ml
index 7a65f6ea..958a1919 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -599,7 +599,7 @@ let value_string_append = function
 let value_decimal_string_of_bits = function
   | [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v))
   | _ -> failwith "value decimal_string_of_bits"
-       
+
 let primops =
   List.fold_left
     (fun r (x, y) -> StringMap.add x y r)
-- 
cgit v1.2.3