diff options
| author | Alasdair Armstrong | 2018-05-15 17:02:23 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-05-31 16:50:43 +0100 |
| commit | 3babc5a0c35a2774904d2ee44f3c69e79c54876f (patch) | |
| tree | a02618d81b6e6db365109c1670faefa55c86dffb /src | |
| parent | 2a66ef3b242af924099d38cda38c2e5c771616fd (diff) | |
Some tweaks to ocaml compilation and sail_lib for ARM with system registers
Diffstat (limited to 'src')
| -rw-r--r-- | src/ocaml_backend.ml | 4 | ||||
| -rw-r--r-- | src/sail_lib.ml | 14 |
2 files changed, 15 insertions, 3 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 60a34273..a13d7b4b 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -177,9 +177,9 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) = | P_id id -> begin match Env.lookup_id id (pat_env_of pat) with - | Local (Immutable, _) | Unbound -> zencode ctx id + | Local (_, _) | Unbound -> zencode ctx id | Enum _ -> zencode_upper ctx id - | _ -> failwith ("Ocaml: Cannot pattern match on mutable variable or register:" ^ string_of_pat pat) + | _ -> failwith ("Ocaml: Cannot pattern match on register: " ^ string_of_pat pat) end | P_lit lit -> ocaml_lit lit | P_typ (_, pat) -> ocaml_pat ctx pat diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 08de6d69..28784ce1 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -49,7 +49,7 @@ let trace_call str = type bit = B0 | B1 let eq_bit (a, b) = a = b - + let and_bit = function | B1, B1 -> B1 | _, _ -> B0 @@ -629,3 +629,15 @@ let speculate_conditional_success () = true (* Return nanoseconds since epoch. Truncates to ocaml int but will be OK for next 100 years or so... *) let get_time_ns () = Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())) +let string_of_bool = function + | true -> "true" + | false -> "false" + +let dec_str x = Big_int.to_string x + +let hex_str x = Big_int.to_string x + +let trace_memory_write (_, _, _) = () +let trace_memory_read (_, _, _) = () + +let sleep_request () = () |