diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/interpreter.ml | 4 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 3 | ||||
| -rw-r--r-- | src/sail_lib.ml | 21 | ||||
| -rw-r--r-- | src/value.ml | 10 |
4 files changed, 37 insertions, 1 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 1a8cad90..599a83bf 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -105,6 +105,10 @@ let value_of_lit (L_aux (l_aux, _)) = |> List.map (fun c -> List.map (fun b -> V_bit b) (Sail_lib.hex_char c)) |> List.concat |> (fun v -> V_vector v) + | L_bin str -> + Util.string_to_list str + |> List.map (fun c -> V_bit (Sail_lib.bin_char c)) + |> (fun v -> V_vector v) | _ -> failwith "Unimplemented value_of_lit" (* TODO *) let is_value = function diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 2a6206d4..970dea83 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -195,7 +195,8 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) = match Env.lookup_id id (pat_env_of pat) with | Local (Immutable, _) | Unbound -> zencode ctx id | Enum _ -> zencode_upper ctx id - | _ -> failwith "Ocaml: Cannot pattern match on mutable variable or register" + | Union _ -> zencode_upper ctx id + | _ -> failwith ("Ocaml: Cannot pattern match on mutable variable or 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 08b8ac1a..86c12aae 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -255,6 +255,11 @@ let get_slice_int (n, m, o) = assert (Big_int.equal (Big_int.of_int (List.length slice)) n); slice +let bin_char = function + | '0' -> B0 + | '1' -> B1 + | _ -> failwith "Invalid binary character" + let hex_char = function | '0' -> [B0; B0; B0; B0] | '1' -> [B0; B0; B0; B1] @@ -479,8 +484,24 @@ 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 skip () = () + let zero_extend (vec, n) = let m = Big_int.to_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 + + +let sign_extend (vec, n) = + let m = Big_int.to_int n in + match vec with + | B0 :: _ as vec -> replicate_bits ([B0], Big_int.of_int (m - List.length vec)) @ vec + | [] -> replicate_bits ([B0], Big_int.of_int (m - List.length vec)) @ vec + | B1 :: _ as vec -> replicate_bits ([B1], Big_int.of_int (m - List.length vec)) @ vec + +(* FIXME *) +let shift_bits_right (x, y) = x +let shift_bits_left (x, y) = x + +let speculate_conditional_success () = true diff --git a/src/value.ml b/src/value.ml index b1f6f80b..0b50ee1f 100644 --- a/src/value.ml +++ b/src/value.ml @@ -328,6 +328,14 @@ let rec string_of_value = function | V_record record -> "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" +let value_sign_extend = function + | [v1; v2] -> mk_vector (Sail_lib.sign_extend (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value sign_extend" + +let value_zero_extend = function + | [v1; v2] -> mk_vector (Sail_lib.zero_extend (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value zero_extend" + let eq_value v1 v2 = string_of_value v1 = string_of_value v2 let value_eq_anything = function @@ -407,6 +415,8 @@ let primops = ("set_slice_int", value_set_slice_int); ("set_slice", value_set_slice); ("hex_slice", value_hex_slice); + ("zero_extend", value_zero_extend); + ("sign_extend", value_sign_extend); ("add_int", value_add_int); ("sub_int", value_sub_int); ("mult", value_mult); |