From 4e814bba48f8274874010f282c431d7d65e5bb0e Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 27 Nov 2017 16:33:43 +0000
Subject: Compile assertions into OCaml

and_bool and or_bool now are treated specially in the ocaml backend,
so that they have the correct short-circuiting behaviour. This is
required so that assertions don't fail for the ARM spec for predicates
that shouldn't be tested in certain circumstances, for example things like:

IsAArch32() && AArch32_specific_predicate

Also fixed an issue in the sail library for ocaml where greater than
or equal to was being mapped to greater than.
---
 lib/ocaml_rts/sail_lib.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 292f187e..3cf4505d 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -416,7 +416,7 @@ let sub_real (x, y) = Num.sub_num x y
 let lt (x, y) = lt_big_int x y
 let gt (x, y) = gt_big_int x y
 let lteq (x, y) = le_big_int x y
-let gteq (x, y) = gt_big_int x y
+let gteq (x, y) = ge_big_int x y
 
 let pow2 x = power_big_int_positive_int x 2
 
@@ -462,3 +462,9 @@ let rec string_of_list sep string_of = function
   | [] -> ""
   | [x] -> string_of x
   | x::ls -> (string_of x) ^ sep ^ (string_of_list sep string_of ls)
+
+let zero_extend (vec, n) =
+  let m = int_of_big_int n in
+  if m <= List.length vec
+  then take m vec
+  else replicate_bits ([B0], big_int_of_int (m - List.length vec)) @ vec
-- 
cgit v1.2.3