summaryrefslogtreecommitdiff
path: root/src/sail_lib.ml
diff options
context:
space:
mode:
authorjp2020-02-12 17:46:48 +0000
committerjp2020-02-12 17:46:48 +0000
commited8bccd927306551f93d5aab8d0e2a92b9e5d227 (patch)
tree55bf788c8155f0c7d024f2147f5eb3873729b02a /src/sail_lib.ml
parent31a65c9b7383d2a87da0fbcf5c265d533146ac23 (diff)
parent4a72cb8084237161d0bccc66f27d5fb6d24315e0 (diff)
Merge branch 'sail2' of https://github.com/rems-project/sail into sail2
Diffstat (limited to 'src/sail_lib.ml')
-rw-r--r--src/sail_lib.ml15
1 files changed, 10 insertions, 5 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 164bcefa..03994657 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -17,6 +17,14 @@ let opt_trace = ref false
let trace_depth = ref 0
let random = ref false
+
+let opt_cycle_limit = ref 0
+let cycle_count = ref 0
+
+let cycle_limit_reached () =
+ cycle_count := !cycle_count + 1;
+ !opt_cycle_limit != 0 && !cycle_count >= !opt_cycle_limit
+
let sail_call (type t) (f : _ -> t) =
let module M =
struct exception Return of t end
@@ -274,9 +282,7 @@ let rec replicate_bits (bits, n) =
let identity x = x
-
-
-(*
+(*
Returns list of n bits of integer m starting from offset o >= 0 (bits numbered from least significant).
Uses twos-complement representation for m<0 and pads most significant bits in sign-extended way.
Most significant bit is head of returned list.
@@ -529,7 +535,7 @@ let fast_read_ram (data_size, addr) =
!vector
let tag_ram = (ref Mem.empty : (bool Mem.t) ref);;
-
+
let write_tag_bool (addr, tag) =
let addri = uint addr in
tag_ram := Mem.add addri tag !tag_ram
@@ -551,7 +557,6 @@ let lor_int (n, m) = Big_int.bitwise_or n m
let land_int (n, m) = Big_int.bitwise_and n m
let lxor_int (n, m) = Big_int.bitwise_xor n m
-
let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2 ^ string_of_bits v)
let eq_string (str1, str2) = String.compare str1 str2 == 0