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 /src/value.ml | |
| 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 'src/value.ml')
| -rw-r--r-- | src/value.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |