diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 7 | ||||
| -rw-r--r-- | src/_tags | 11 | ||||
| -rw-r--r-- | src/c_backend.ml | 131 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 8 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.ml | 1488 | ||||
| -rw-r--r-- | src/myocamlbuild.ml | 2 | ||||
| -rw-r--r-- | src/util.ml | 7 | ||||
| -rw-r--r-- | src/util.mli | 2 | ||||
| -rw-r--r-- | src/value2.lem | 99 |
9 files changed, 210 insertions, 1545 deletions
diff --git a/src/Makefile b/src/Makefile index 8bf4802a..3e0b9841 100644 --- a/src/Makefile +++ b/src/Makefile @@ -82,7 +82,7 @@ ast.ml: ast.lem sed -i -f ast.sed ast.ml bytecode.ml: bytecode.lem - lem -ocaml bytecode.lem + lem -ocaml bytecode.lem -lib . -lib gen_lib/ sed -i -f ast.sed bytecode.ml lem_interp/interp_ast.lem: ../language/l2.ott @@ -234,8 +234,8 @@ _build/%_trimmed.sail: _build/%_all.sail count: _build/cheri_trimmed.sail _build/mips_trimmed.sail wc -l $^ -%.ml: %.lem - $(LEM) -only_changed_output -ocaml -lib lem_interp/ $< +# %.ml: %.lem +# $(LEM) -only_changed_output -ocaml -lib lem_interp/ $< #run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter # env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native @@ -280,6 +280,7 @@ clean: -rm -rf tex-doc -rm -rf lem lib -rm -rf sail.docdir + -rm -f gen_lib/*.ml -rm -f ast.ml -rm -f ast.lem -rm -f bytecode.ml @@ -1,16 +1,15 @@ true: -traverse, debug, use_menhir <**/*.ml>: bin_annot, annot -# <lem_interp> or <test>: include + <sail.{byte,native}>: package(zarith), package(linksem), package(lem), use_pprint <isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), use_pprint + <isail.ml>: package(linenoise) <elf_loader.ml>: package(linksem) -<pprint> or <pprint/src>: include -<*.m{l,li}>: package(lem) +<**/*.m{l,li}>: package(lem) -# see http://caml.inria.fr/mantis/view.php?id=4943 -<lem_interp/*> and not <lem_interp/*.cmxa>: package(num), package(lem) -<test/*> and not <test/*.cmxa>: package(num), package(lem), package(str) +<gen_lib>: include +<pprint> or <pprint/src>: include # disable partial match and unused variable warnings <**/*.ml>: warn_y diff --git a/src/c_backend.ml b/src/c_backend.ml index dc87cfd9..33f6f127 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -53,6 +53,7 @@ open Ast_util open Bytecode open Type_check open PPrint +open Value2 module Big_int = Nat_big_num let c_verbosity = ref 1 @@ -82,10 +83,23 @@ let lvar_typ = function (* | Union (_, typ) -> typ *) | _ -> assert false +let string_of_value = function + | V_bits bs -> Sail_values.show_bitlist bs ^ "ul" + | V_int i -> Big_int.to_string i ^ "l" + | V_bool true -> "true" + | V_bool false -> "false" + | V_null -> "NULL" + | V_unit -> "UNIT" + | V_bit Sail_values.B0 -> "0ul" + | V_bit Sail_values.B1 -> "1ul" + | V_string str -> "\"" ^ str ^ "\"" + | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str + | _ -> failwith "Cannot convert value to string" + let rec string_of_fragment ?zencode:(zencode=true) = function | F_id id when zencode -> Util.zencode_string (string_of_id id) | F_id id -> string_of_id id - | F_lit str -> str + | F_lit v -> string_of_value v | F_call (str, frags) -> Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags) | F_field (f, field) -> @@ -175,7 +189,7 @@ and aval = let rec frag_rename from_id to_id = function | F_id id when Id.compare id from_id = 0 -> F_id to_id | F_id id -> F_id id - | F_lit str -> F_lit str + | F_lit v -> F_lit v | F_have_exception -> F_have_exception | F_current_exception -> F_current_exception | F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags) @@ -829,16 +843,39 @@ let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp m (* 3. Optimization of primitives and literals *) (**************************************************************************) +let hex_char = + let open Sail_values in + function + | '0' -> [B0; B0; B0; B0] + | '1' -> [B0; B0; B0; B1] + | '2' -> [B0; B0; B1; B0] + | '3' -> [B0; B0; B1; B1] + | '4' -> [B0; B1; B0; B0] + | '5' -> [B0; B1; B0; B1] + | '6' -> [B0; B1; B1; B0] + | '7' -> [B0; B1; B1; B1] + | '8' -> [B1; B0; B0; B0] + | '9' -> [B1; B0; B0; B1] + | 'A' | 'a' -> [B1; B0; B1; B0] + | 'B' | 'b' -> [B1; B0; B1; B1] + | 'C' | 'c' -> [B1; B1; B0; B0] + | 'D' | 'd' -> [B1; B1; B0; B1] + | 'E' | 'e' -> [B1; B1; B1; B0] + | 'F' | 'f' -> [B1; B1; B1; B1] + | _ -> failwith "Invalid hex character" + let literal_to_fragment (L_aux (l_aux, _) as lit) = match l_aux with | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> - Some (F_lit (Big_int.to_string n ^ "L")) + Some (F_lit (V_int n)) | L_hex str when String.length str <= 16 -> let padding = 16 - String.length str in - Some (F_lit ("0x" ^ String.make padding '0' ^ str ^ "ul")) - | L_unit -> Some (F_lit "UNIT") - | L_true -> Some (F_lit "true") - | L_false -> Some (F_lit "false") + let padding = Util.list_init padding (fun _ -> Sail_values.B0) in + let content = Util.string_to_list str |> List.map hex_char |> List.concat in + Some (F_lit (V_bits (padding @ content))) + | L_unit -> Some (F_lit V_unit) + | L_true -> Some (F_lit (V_bool true)) + | L_false -> Some (F_lit (V_bool false)) | _ -> None let c_literals ctx = @@ -869,9 +906,9 @@ let rec is_bitvector = function | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals | _ :: _ -> false -let rec string_of_aval_bit = function - | AV_lit (L_aux (L_zero, _), _) -> "0" - | AV_lit (L_aux (L_one, _), _) -> "1" +let rec value_of_aval_bit = function + | AV_lit (L_aux (L_zero, _), _) -> Sail_values.B0 + | AV_lit (L_aux (L_one, _), _) -> Sail_values.B1 | _ -> assert false let rec c_aval ctx = function @@ -893,7 +930,7 @@ let rec c_aval ctx = function | _ -> v end | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 -> - let bitstring = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit v) ^ "ul") in + let bitstring = F_lit (V_bits (List.map value_of_aval_bit v)) in AV_C_fragment (bitstring, typ) | AV_tuple avals -> AV_tuple (List.map (c_aval ctx) avals) | aval -> aval @@ -912,31 +949,33 @@ let analyze_primop' ctx id args typ = let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in (* prerr_endline ("Analysing: " ^ string_of_typ typ ^ " " ^ extern ^ Pretty_print_sail.to_string (separate_map (string ", ") pp_aval args)); *) + let v_one = F_lit (V_int (Big_int.of_int 1)) in + match extern, args with | "eq_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "==", v2), typ)) | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> - let len = F_op (f, "-", F_op (t, "-", F_lit "1L")) in - AE_val (AV_C_fragment (F_op (F_op (F_op (F_lit "1L", "<<", len), "-", F_lit "1L"), "&", F_op (vec, ">>", t)), typ)) + let len = F_op (f, "-", F_op (t, "-", v_one)) in + AE_val (AV_C_fragment (F_op (F_op (F_op (v_one, "<<", len), "-", v_one), "&", F_op (vec, ">>", t)), typ)) | "vector_access", [AV_C_fragment (vec, _); AV_C_fragment (n, _)] -> - AE_val (AV_C_fragment (F_op (F_lit "1L", "&", F_op (vec, ">>", n)), typ)) + AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ)) | "eq_bit", [AV_C_fragment (a, _); AV_C_fragment (b, _)] -> AE_val (AV_C_fragment (F_op (a, "==", b), typ)) | "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] -> - AE_val (AV_C_fragment (F_op (F_op (F_op (F_lit "1L", "<<", len), "-", F_lit "1L"), "&", F_op (vec, ">>", start)), typ)) + AE_val (AV_C_fragment (F_op (F_op (F_op (v_one, "<<", len), "-", v_one), "&", F_op (vec, ">>", start)), typ)) | "undefined_bit", _ -> - AE_val (AV_C_fragment (F_lit "0ul", typ)) + AE_val (AV_C_fragment (F_lit (V_bit Sail_values.B0), typ)) | "undefined_vector", [AV_C_fragment (len, _); _] -> begin match destruct_vector ctx.tc_env typ with | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> - AE_val (AV_C_fragment (F_lit "0ul", typ)) + AE_val (AV_C_fragment (F_lit (V_bit Sail_values.B0), typ)) | _ -> no_change end @@ -953,12 +992,12 @@ let analyze_primop' ctx id args typ = begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _) when Big_int.less_equal n (Big_int.of_int 64) -> - AE_val (AV_C_fragment (F_call ("fast_replicate_bits", [F_lit (Big_int.to_string m); vec; times]), typ)) + AE_val (AV_C_fragment (F_call ("fast_replicate_bits", [F_lit (V_int m); vec; times]), typ)) | _ -> no_change end | "undefined_bool", _ -> - AE_val (AV_C_fragment (F_lit "false", typ)) + AE_val (AV_C_fragment (F_lit (V_bool false), typ)) | _, _ -> no_change @@ -1261,32 +1300,32 @@ let rec compile_aval ctx = function [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] | AV_lit (L_aux (L_string str, _), typ) -> - [], (F_lit ("\"" ^ String.escaped str ^ "\""), ctyp_of_typ ctx typ), [] + [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), [] | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> let gs = gensym () in [idecl CT_mpz gs; - iinit CT_mpz gs (F_lit (Big_int.to_string n ^ "l"), CT_int64)], + iinit CT_mpz gs (F_lit (V_int n), CT_int64)], (F_id gs, CT_mpz), [iclear CT_mpz gs] | AV_lit (L_aux (L_num n, _), typ) -> let gs = gensym () in [idecl CT_mpz gs; - iinit CT_mpz gs (F_lit ("\"" ^ Big_int.to_string n ^ "\""), CT_string)], + iinit CT_mpz gs (F_lit (V_string (Big_int.to_string n)), CT_string)], (F_id gs, CT_mpz), [iclear CT_mpz gs] - | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit "0", CT_bit), [] - | AV_lit (L_aux (L_one, _), _) -> [], (F_lit "1", CT_bit), [] + | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail_values.B0), CT_bit), [] + | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail_values.B1), CT_bit), [] - | AV_lit (L_aux (L_true, _), _) -> [], (F_lit "true", CT_bool), [] - | AV_lit (L_aux (L_false, _), _) -> [], (F_lit "false", CT_bool), [] + | AV_lit (L_aux (L_true, _), _) -> [], (F_lit (V_bool true), CT_bool), [] + | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), [] | AV_lit (L_aux (L_real str, _), _) -> let gs = gensym () in [idecl CT_real gs; - iinit CT_real gs (F_lit ("\"" ^ str ^ "\""), CT_string)], + iinit CT_real gs (F_lit (V_string str), CT_string)], (F_id gs, CT_real), [iclear CT_real gs] @@ -1331,7 +1370,7 @@ let rec compile_aval ctx = function (* Convert a small bitvector to a uint64_t literal. *) | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 -> begin - let bitstring = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit avals) ^ "ul") in + let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in let len = List.length avals in match destruct_vector ctx.tc_env typ with | Some (_, Ord_aux (Ord_inc, _), _) -> @@ -1348,7 +1387,7 @@ let rec compile_aval ctx = function variable size bitvector, converting it in 64-bit chunks. *) | AV_vector (avals, typ) when is_bitvector avals -> let len = List.length avals in - let bitstring avals = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit avals) ^ "ul") in + let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in let first_chunk = bitstring (Util.take (len mod 64) avals) in let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in let gs = gensym () in @@ -1372,18 +1411,18 @@ let rec compile_aval ctx = function in let gs = gensym () in let ctyp = CT_uint64 (len, direction) in - let mask i = "0b" ^ String.make (63 - i) '0' ^ "1" ^ String.make i '0' ^ "ul" in + let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail_values.B0) @ [Sail_values.B1] @ Util.list_init i (fun _ -> Sail_values.B0)) in let aval_mask i aval = let setup, cval, cleanup = compile_aval ctx aval in match cval with - | (F_lit "0", _) -> [] - | (F_lit "1", _) -> + | (F_lit (V_bit Sail_values.B0), _) -> [] + | (F_lit (V_bit Sail_values.B1), _) -> [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] | _ -> setup @ [iif cval [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup in [idecl ctyp gs; - icopy (CL_id gs) (F_lit "0ul", ctyp)] + icopy (CL_id gs) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail_values.B0))), ctyp)] @ List.concat (List.mapi aval_mask (List.rev avals)), (F_id gs, ctyp), [] @@ -1471,7 +1510,7 @@ let compile_funcall ctx id args typ = let rec compile_match ctx apat cval case_label = match apat, cval with | AP_id pid, (frag, ctyp) when is_ct_variant ctyp -> - [ijump (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ Util.zencode_string (string_of_id pid))), CT_bool) case_label], + [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], [] | AP_global (pid, _), _ -> [icopy (CL_id pid) cval], [] | AP_id pid, (frag, ctyp) when is_ct_enum ctyp -> @@ -1499,10 +1538,10 @@ let rec compile_match ctx apat cval case_label = | AP_app (ctor, apat), (frag, ctyp) -> begin match ctyp with | CT_variant (_, ctors) -> - let ctor_c_id = Util.zencode_string (string_of_id ctor) in + let ctor_c_id = string_of_id ctor in let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in - let instrs, cleanup = compile_match ctx apat ((F_field (frag, ctor_c_id), ctor_ctyp)) case_label in - [ijump (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ ctor_c_id)), CT_bool) case_label] + let instrs, cleanup = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in + [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label] @ instrs, cleanup | _ -> failwith "AP_app constructor with non-variant type" @@ -1512,12 +1551,12 @@ let rec compile_match ctx apat cval case_label = | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) -> let hd_setup, hd_cleanup = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in let tl_setup, tl_cleanup = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in - [ijump (F_op (frag, "==", F_lit "NULL"), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup + [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup | AP_cons _, (_, _) -> c_error "Tried to pattern match cons on non list type" - | AP_nil, (frag, _) -> [ijump (F_op (frag, "!=", F_lit "NULL"), CT_bool) case_label], [] + | AP_nil, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [] -let unit_fragment = (F_lit "UNIT", CT_unit) +let unit_fragment = (F_lit V_unit, CT_unit) (** GLOBAL: label_counter is used to make sure all labels have unique names. Like gensym_counter it should be safe to reset between @@ -1557,7 +1596,7 @@ let rec compile_aexp ctx = function let compile_case (apat, guard, body) = let trivial_guard = match guard with | AE_val (AV_lit (L_aux (L_true, _), _)) - | AE_val (AV_C_fragment (F_lit "true", _)) -> true + | AE_val (AV_C_fragment (F_lit (V_bool true), _)) -> true | _ -> false in let case_label = label "case_" in @@ -1596,7 +1635,7 @@ let rec compile_aexp ctx = function let compile_case (apat, guard, body) = let trivial_guard = match guard with | AE_val (AV_lit (L_aux (L_true, _), _)) - | AE_val (AV_C_fragment (F_lit "true", _)) -> true + | AE_val (AV_C_fragment (F_lit (V_bool true), _)) -> true | _ -> false in let try_label = label "try_" in @@ -1625,7 +1664,7 @@ let rec compile_aexp ctx = function @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel handled_exception_label] - @ [icopy CL_have_exception (F_lit "false", CT_bool)] + @ [icopy CL_have_exception (F_lit (V_bool false), CT_bool)] | AE_if (aval, then_aexp, else_aexp, if_typ) -> let if_ctyp = ctyp_of_typ ctx if_typ in @@ -1671,7 +1710,7 @@ let rec compile_aexp ctx = function let gs = gensym () in left_setup @ [ idecl CT_bool gs; - iif cval (right_setup @ [call (CL_id gs)] @ right_cleanup) [icopy (CL_id gs) (F_lit "false", CT_bool)] CT_bool ] + iif cval (right_setup @ [call (CL_id gs)] @ right_cleanup) [icopy (CL_id gs) (F_lit (V_bool false), CT_bool)] CT_bool ] @ left_cleanup, CT_bool, (fun clexp -> icopy clexp (F_id gs, CT_bool)), @@ -1682,7 +1721,7 @@ let rec compile_aexp ctx = function let gs = gensym () in left_setup @ [ idecl CT_bool gs; - iif cval [icopy (CL_id gs) (F_lit "true", CT_bool)] (right_setup @ [call (CL_id gs)] @ right_cleanup) CT_bool ] + iif cval [icopy (CL_id gs) (F_lit (V_bool true), CT_bool)] (right_setup @ [call (CL_id gs)] @ right_cleanup) CT_bool ] @ left_cleanup, CT_bool, (fun clexp -> icopy clexp (F_id gs, CT_bool)), @@ -1996,7 +2035,7 @@ let fix_exception_block ctx instrs = | before, I_aux (I_throw cval, _) :: after -> before @ [icopy CL_current_exception cval; - icopy CL_have_exception (F_lit "true", CT_bool)] + icopy CL_have_exception (F_lit (V_bool true), CT_bool)] @ generate_cleanup (historic @ before) @ [igoto end_block_label] @ rewrite_exception (historic @ before) after diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 4d67cbfc..fce595e0 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -108,6 +108,12 @@ let showBitU = function | BU -> "U" end +let bitU_char = function + | B0 -> #'0' + | B1 -> #'1' + | BU -> #'?' +end + instance (Show bitU) let show = showBitU end @@ -307,7 +313,7 @@ declare {isabelle} termination_argument hexstring_of_bits = automatic let show_bitlist bs = match hexstring_of_bits bs with | Just s -> toString (#'0' :: #'x' :: s) - | Nothing -> show bs + | Nothing -> toString (#'0' :: #'b' :: map bitU_char bs) end (*** List operations *) diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml deleted file mode 100644 index 213acea1..00000000 --- a/src/gen_lib/sail_values.ml +++ /dev/null @@ -1,1488 +0,0 @@ -open Big_int_Z -open Printf - -let trace_writes = ref false -let tracef = printf - -(* only expected to be 0, 1, 2; 2 represents undef *) -type vbit = Vone | Vzero | Vundef -type number = Big_int_Z.big_int - -type _bool = vbit -type _string = string -type _nat = number -type _int = number - -let undef_val = ref Vundef - -type value = - | Vvector of vbit array * int * bool - | VvectorR of value array * int * bool - | Vregister of vbit array ref * int * bool * string * (string * (int * int)) list - | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*) - -exception Sail_exit -exception Sail_return - -let _print s = print_string s - -let string_of_bit = function - | Vone -> "1" - | Vzero -> "0" - | Vundef -> "u" - -let bit_of_string = function - | "1" -> Vone - | "0" -> Vzero - | "u" -> Vundef - | _ -> failwith "invalid bit value" - -let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) - -let string_of_value = function - | Vvector(bits, start, inc) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array bits) - | VvectorR(values, start, inc) -> "" - | Vregister(bits, start, inc, name, fields) -> "reg" ^ (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits) - | Vbit(b) -> string_of_bit b - -let to_bool = function - | Vzero -> false - | Vone -> true - | Vundef -> assert false - -let is_one i = - if eq_big_int i unit_big_int - then Vone - else Vzero - - -let exit _ = raise Sail_exit - - -let is_one_int i = - if i = 1 then Vone else Vzero - -let get_barray = function - | Vvector(a,_,_) -> a - | Vregister(a,_,_,_,_) -> !a - | _ -> assert false - -let get_varray = function - | VvectorR(a,_,_) -> a - | _ -> assert false - -let get_ord = function - | Vvector(_,_,o) | Vregister(_,_,o,_,_) | VvectorR(_,_,o) -> o - | _ -> assert false - -let get_start = function - | Vvector(_,s,o) | Vregister(_,s,o,_,_) | VvectorR(_,s,o) -> s - | _ -> assert false - -let set_start i = function - | Vvector(a,start,dir) -> Vvector(a,i,dir) - | Vregister(bits,start,dir,name,regfields) -> Vregister(bits,i,dir,name,regfields) - | VvectorR(a,start,dir) -> VvectorR(a,i,dir) - | _ -> assert false - -let length_int = function - | Vvector(array,_,_) -> Array.length array - | Vregister(array,_,_,_,_) -> Array.length !array - | VvectorR(array,_,_) -> Array.length array - | _ -> assert false - -let set_start_to_length v = set_start ((length_int v)-1) v (* XXX should take account of direction? *) - -let length_big v = big_int_of_int (length_int v) -let length = length_big - -let read_register = function - | Vregister(a,start,inc,_,_) -> Vvector(!a,start,inc) - | v -> v - -let vector_access_int v n = - match v with - | VvectorR(array,start,is_inc) -> - if is_inc - then (array.(n-start)) - else (array.(start-n)) - | _ -> assert false - -let vector_access_big v n = vector_access_int v (int_of_big_int n) - -let vector_access = vector_access_big - -let bit_vector_access_int v n = match v with - | Vvector(array,start,is_inc) -> - if is_inc - then array.(n-start) - else array.(start-n) - | Vregister(array,start,is_inc,_,_) -> - if is_inc - then !array.(n-start) - else !array.(start-n) - | _ -> assert false - -let bit_vector_access_big v n = bit_vector_access_int v (int_of_big_int n) -let bit_vector_access = bit_vector_access_big - -let vector_subrange_int v n m = - (*Printf.printf "vector_subrange %s %d %d\n" (string_of_value v) n m;*) - match v with - | VvectorR(array,start,is_inc) -> - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - VvectorR(Array.sub array offset length,n,is_inc) - | Vvector(array,start,is_inc) -> - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - Vvector(Array.sub array offset length,n,is_inc) - | Vregister(array,start,is_inc,name,fields) -> - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - Vvector(Array.sub !array offset length,n,is_inc) - | _ -> v - -let vector_subrange_big v n m = vector_subrange_int v (int_of_big_int n) (int_of_big_int m) -let vector_subrange = vector_subrange_big - -let get_register_field_vec reg field = - match reg with - | Vregister(_,_,_,name,fields) -> - (match List.assoc field fields with - | (i,j) -> - if i = j - then Vbit Vundef - else vector_subrange_int reg i j) - | _ -> Vbit Vundef - -let get_register_field_bit reg field = - match reg with - | Vregister(_,_,_,name,fields) -> - (match List.assoc field fields with - | (i,j) -> - if i = j - then bit_vector_access_int reg i - else Vundef) - | _ -> Vundef - -let set_register register value = match register,value with - | Vregister(a,_,_,name,_), Vregister(new_v,_,_,_,_) -> - begin - if !trace_writes then - tracef "%s <- %s\n" name (string_of_value value); - a := !new_v - end - | Vregister(a,_,_,name,_), Vvector(new_v,_,_) -> - begin - if !trace_writes then - tracef "%s <- %s\n" name (string_of_value value); - a := new_v - end - | _ -> failwith "set_register of non-register" - -let set_vector_subrange_vec_int v n m new_v = - let walker array length offset new_values = - begin - for x = 0 to length-1 - do array.(x+offset) <- new_values.(x) - done; - end - in - match v, new_v with - | VvectorR(array,start,is_inc),VvectorR(new_v,_,_) -> - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - walker array length offset new_v - | _ -> () - -let set_vector_subrange_vec_big v n m new_v = - set_vector_subrange_vec_int v (int_of_big_int n) (int_of_big_int m) new_v -let set_vector_subrange_vec = set_vector_subrange_vec_big (* or maybe _int *) - -let set_vector_subrange_bit_int v n m new_v = - let walker array length offset new_values = - begin - for x = 0 to length-1 - do array.(x+offset) <- new_values.(x) - done; - end - in - match v,new_v with - | Vvector(array,start,is_inc),Vvector(new_v,_,_) -> - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - walker array length offset new_v - | Vregister(array,start,is_inc,name,fields),Vvector(new_v,_,_) -> - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - walker !array length offset new_v - | _ -> () - -let set_vector_subrange_bit_big v n m new_v = - set_vector_subrange_bit_int v (int_of_big_int n) (int_of_big_int m) new_v -let set_vector_subrange_bit = set_vector_subrange_bit_big - -let set_register_bit_int reg n v = - match reg with - | Vregister(array,start,inc,name,fields) -> - begin - if !trace_writes then - tracef "%s[%d] <- %s\n" name n (string_of_bit v); - (!array).(if inc then (n - start) else (start - n)) <- v - end - | _ -> failwith "set_register_bit of non-register" -let set_register_bit_big reg n v = set_register_bit_int reg (int_of_big_int n) v -let set_register_bit = set_register_bit_big - -let set_register_field_v reg field new_v = - match reg with - | Vregister(array,start,dir,name,fields) -> - begin - if !trace_writes then - tracef "%s[%s] <- %s\n" name field (string_of_value new_v); - (match List.assoc field fields with - | (i,j) -> - if i = j - then () - else set_vector_subrange_bit_int reg i j new_v) - end - | _ -> () - -let set_register_field_bit reg field new_v = - match reg with - | Vregister(array,start,dir,name,fields) -> - begin - if !trace_writes then - tracef "%s.%s <- %s\n" name field (string_of_bit new_v); - (match List.assoc field fields with - | (i,j) -> - if i = j - then !array.(if dir then i - start else start - i) <- new_v - else ()) - end - | _ -> () - -let set_two_reg r1 r2 vec = - let size = length_int r1 in - let dir = get_ord r1 in - let start = get_start vec in - let vsize = length_int vec in - let r1_v = vector_subrange_int vec start ((if dir then size - start else start - size) - 1) in - let r2_v = vector_subrange_int vec (if dir then size - start else start - size) - (if dir then vsize - start else start - vsize) in - begin set_register r1 r1_v; set_register r2 r2_v end - - -let make_indexed_v entries default start size dir = - let default_value = match default with - | None -> Vbit Vundef - | Some v -> v in - let array = Array.make size default_value in - begin - List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries; - VvectorR(array, start, dir) - end - -let make_indexed_v_big entries default start size dir = - make_indexed_v entries default (int_of_big_int start) (int_of_big_int size) dir - -let make_indexed_bitv entries default start size dir = - let default_value = match default with - | None -> Vundef - | Some v -> v in - let array = Array.make size default_value in - begin - List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries; - Vvector(array, start, dir) - end - -let make_indexed_bitv_big entries default start size dir = - make_indexed_bitv entries default (int_of_big_int start) (int_of_big_int size) dir - -let vector_concat l r = - match l,r with - | Vvector(arrayl,start,ord), Vvector(arrayr,_,_) -> - Vvector(Array.append arrayl arrayr, start, ord) - | Vvector(arrayl,start,ord), Vregister(arrayr,_,_,_,_) -> - Vvector(Array.append arrayl !arrayr, start,ord) - | Vregister(arrayl,start,ord,_,_), Vvector(arrayr,_,_) -> - Vvector(Array.append !arrayl arrayr, start, ord) - | Vregister(arrayl,start,ord,_,_), Vregister(arrayr,_,_,_,_) -> - Vvector(Array.append !arrayl !arrayr,start,ord) - | VvectorR(arrayl,start,ord),VvectorR(arrayr,_,_) -> - VvectorR(Array.append arrayl arrayr, start,ord) - | _ -> Vbit Vundef - -let has_undef = function - | Vvector(array,_,_) -> - let rec foreach i = (* XXX ideally would use Array.mem but not in ocaml 4.02.3 *) - if i < Array.length array - then - if array.(i) = Vundef then true - else foreach (i+1) - else false in - foreach 0 - | Vregister(array,_,_,_,_) -> - let array = !array in - let rec foreach i = - if i < Array.length array - then - if array.(i) = Vundef then true - else foreach (i+1) - else false in - foreach 0 - | _ -> false - -let most_significant = function - | Vvector(array,_,_) -> array.(0) - | Vregister(array,_,_,_,_) -> !array.(0) - | _ -> assert false - -let _most_significant = most_significant - -let bitwise_not_bit = function - | Vone -> Vzero - | Vzero -> Vone - | _ -> Vundef - -let bitwise_not = function - | Vvector(array,s,d)-> Vvector( Array.map bitwise_not_bit array,s,d) - | Vregister(array,s,d,_,_) -> Vvector( Array.map bitwise_not_bit !array,s,d) - | _ -> assert false - -let bool_to_bit b = if b then Vone else Vzero - -let bitwise_binop_bit op (l,r) = - match l,r with - | Vundef,_ | _,Vundef -> Vundef (*Do we want to do this or to respect | of One and & of Zero rules?*) - | Vone,Vone -> bool_to_bit (op true true) - | Vone,Vzero -> bool_to_bit (op true false) - | Vzero,Vone -> bool_to_bit (op false true) - | Vzero,Vzero -> bool_to_bit (op false false) - -let bitwise_and_bit = bitwise_binop_bit (&&) -let bitwise_or_bit = bitwise_binop_bit (||) -let bitwise_xor_bit = bitwise_binop_bit (<>) - -let bitwise_binop op (l,r) = - let bop l arrayl arrayr = - let array = Array.make l Vzero in - begin - for i = 0 to (l-1) do - array.(i) <- bitwise_binop_bit op (arrayl.(i), arrayr.(i)) - done; - array - end in - match l,r with - | Vvector(arrayl, start, dir), Vvector(arrayr,_,_) -> - Vvector(bop (Array.length arrayl) arrayl arrayr, start,dir) - | Vvector(arrayl, start, dir), Vregister(arrayr,_,_,_,_) -> - Vvector(bop (Array.length arrayl) arrayl !arrayr, start, dir) - | Vregister(arrayl, start,dir,_,_), Vvector(arrayr,_,_) -> - Vvector(bop (Array.length arrayr) !arrayl arrayr, start,dir) - | Vregister(arrayl, start, dir, _, _), Vregister(arrayr,_,_,_,_) -> - Vvector(bop (Array.length !arrayl) !arrayl !arrayr, start,dir) - | _ -> Vbit Vundef - -let bitwise_and = bitwise_binop (&&) -let bitwise_or = bitwise_binop (||) -let bitwise_xor = bitwise_binop (<>) - -let rec power_int base raiseto = - if raiseto = 0 - then 1 - else base * (power_int base (raiseto - 1)) - -let int_of_bit_array array = - let acc = ref 0 in - let len = Array.length array in - begin - for i = 0 to len - 1 do - acc := (!acc) lsl 1; - match array.(i) with - | Vone -> acc := succ (!acc) - | _ -> () - done; - !acc - end - -let unsigned_int = function - | (Vvector(array,_,_) as v) -> - if has_undef v - then assert false - else int_of_bit_array array - | (Vregister(array,_,_,_,_) as v)-> - let array = !array in - if has_undef v - then assert false - else int_of_bit_array array - | _ -> assert false - -let big_int_of_bit_array array = - let acc = ref zero_big_int in - let len = Array.length array in - begin - for i = 0 to len - 1 do - acc := shift_left_big_int !acc 1; - match array.(i) with - | Vone -> acc := succ_big_int !acc - | _ -> (); - done; - !acc - end - -let unsigned_big = function - | (Vvector(array,_,_) as v) -> - if has_undef v - then assert false - else - big_int_of_bit_array array - | (Vregister(array,_,_,_,_) as v)-> - let array = !array in - if has_undef v - then assert false - else - big_int_of_bit_array array - | _ -> assert false - -let unsigned = unsigned_big - -let signed_int v = - match most_significant v with - | Vone -> -(1 + (unsigned_int (bitwise_not v))) - | Vzero -> unsigned_int v - | _ -> assert false - -let signed_big v = - match most_significant v with - | Vone -> minus_big_int(add_int_big_int 1 (unsigned_big (bitwise_not v))) - | Vzero -> unsigned_big v - | _ -> assert false - -let signed = signed_big - -let to_num_int sign = if sign then signed_int else unsigned_int -let to_num_big sign = if sign then signed_big else unsigned_big -let to_num = to_num_big - -let two_big_int = big_int_of_int 2 -let max_64u = pred_big_int (power_big two_big_int (big_int_of_int 64)) -let max_64 = pred_big_int (power_big two_big_int (big_int_of_int 63)) -let min_64 = minus_big_int (power_big two_big_int (big_int_of_int 63)) -let max_32u = big_int_of_int 4294967295 -let max_32 = big_int_of_int 2147483647 -let min_32 = big_int_of_int (-2147483648) -let max_8 = big_int_of_int 127 -let min_8 = big_int_of_int (-128) -let max_5 = big_int_of_int 31 - -let get_max_representable_in sign n = - match (sign, n) with - | (true, 64) -> max_64 - | (false, 64) -> max_64u - | (true, 32) -> max_32 - | (false, 32) -> max_32u - | (true, 8) -> max_8 - | (false, 5) -> max_5 - | (true, _) -> pred_big_int (power_big two_big_int (big_int_of_int (n-1))) - | (false, _) -> pred_big_int (power_big two_big_int (big_int_of_int n)) - -let get_min_representable_in sign n = - match (sign, n) with - | (false, _) -> zero_big_int - | (true, 64) -> min_64 - | (true, 32) -> min_32 - | (true, 8) -> min_8 - | (true, _) -> minus_big_int (power_big two_big_int (big_int_of_int (n-1))) - -let to_vec_int ord len n = - let array = Array.make len Vzero in - let start = if ord then 0 else len-1 in - let acc = ref n in - for i = (len - 1) downto 0 do - if ((!acc) land 1) = 1 then - array.(i) <- Vone; - acc := (!acc) asr 1 - done; - Vvector(array, start, ord) - -let to_vec_big ord len n = - let len = int_of_big_int len in - let array = Array.make len Vzero in - let start = if ord then 0 else len-1 in - if eq_big_int n zero_big_int - then Vvector(array, start, ord) - else - begin - for i = 0 to len - 1 do - if ((extract_big_int n (len - 1 - i) 1) == unit_big_int) then - array.(i) <- Vone - done; - Vvector(array, start, ord) - end - -let to_vec_inc_int (len,n) = to_vec_int true len n -let to_vec_dec_int (len,n) = to_vec_int false len n - -let to_vec_inc_big (len,n) = to_vec_big true len n -let to_vec_dec_big (len,n) = to_vec_big false len n - -let to_vec_inc = to_vec_inc_big -let to_vec_dec = to_vec_dec_big - -let to_vec_undef_int ord len = - let array = Array.make len !undef_val in - let start = if ord then 0 else len-1 in - Vvector(array, start, ord) - -let to_vec_undef_big ord len = - let len = int_of_big_int len in - let array = Array.make len !undef_val in - let start = if ord then 0 else len-1 in - Vvector(array, start, ord) - -let to_vec_inc_undef_int len = to_vec_undef_int true len -let to_vec_dec_undef_int len = to_vec_undef_int false len - -let to_vec_inc_undef_big len = to_vec_undef_big true len -let to_vec_dec_undef_big len = to_vec_undef_big false len - -let to_vec_inc_undef = to_vec_inc_undef_big -let to_vec_dec_undef = to_vec_dec_undef_big - -let exts_int (len, vec) = - let barray = get_barray(vec) in - let vlen = Array.length barray in - let arr = - if (vlen < len) then - (* copy most significant bit into new bits *) - Array.append (Array.make (len - vlen) barray.(0)) barray - else - (* truncate to least significant bits *) - Array.sub barray (vlen - len) len in - let inc = get_ord vec in - Vvector(arr, (if inc then 0 else (len - 1)), inc) - -let extz_int (len, vec) = - let barray = get_barray(vec) in - let vlen = Array.length barray in - let arr = - if (vlen < len) then - (* fill new bits with zero *) - Array.append (Array.make (len - vlen) Vzero) barray - else - (* truncate to least significant bits *) - Array.sub barray (vlen - len) len in - let inc = get_ord vec in - Vvector(arr, (if inc then 0 else (len - 1)), inc) - -let exts_big (len,vec) = exts_int (int_of_big_int len, vec) -let extz_big (len,vec) = extz_int (int_of_big_int len, vec) - -let exts = exts_big -let extz = extz_big - -let arith_op op (l,r) = op l r -let add_big = arith_op add_big_int -let add_signed_big = arith_op add_big_int -let minus_big = arith_op sub_big_int -let multiply_big = arith_op mult_big_int -let min_big = arith_op min_big_int -let max_big = arith_op max_big_int -(* NB Z.div is what we want because it does truncation towards zero unlike Big_int_Z.div_big_int == Z.ediv *) -let quot_big = arith_op (Z.div) -let modulo_big = arith_op (Z.rem) - -let power_big = arith_op power_big - -let add_int = arith_op (+) -let add_signed_int = arith_op (+) -let minus_int = arith_op (-) -let multiply_int = arith_op ( * ) -let modulo_int = arith_op (mod) -let quot_int = arith_op (/) - -let power_int = arith_op power_int - -let add = add_big -let add_signed = add_signed_big -let minus = minus_big -let multiply = multiply_big -let modulo = modulo_big -let quot = quot_big -let power = power_big -let min_int = min (* the built-in version *) -let min = min_big (* is overwritten here *) -let max_int = max (* likewise *) -let max = max_big -let abs_int = abs -let abs_big = abs_big_int -let abs = abs_big - -let arith_op_vec_big op sign size (l,r) = - let ord = get_ord l in - let (l',r') = to_num_big sign l, to_num_big sign r in - let n = arith_op op (l',r') in - to_vec_big ord (mult_big_int size (length_big l)) n - -let add_vec_big = arith_op_vec_big add_big_int false unit_big_int -let add_vec_signed_big = arith_op_vec_big add_big_int true unit_big_int -let minus_vec_big = arith_op_vec_big sub_big_int false unit_big_int -let multiply_vec_big = arith_op_vec_big mult_big_int false two_big_int -let multiply_vec_signed_big = arith_op_vec_big mult_big_int true two_big_int - -let arith_op_vec_int op sign size (l,r) = - let ord = get_ord l in - let (l',r') = to_num_int sign l, to_num_int sign r in - let n = arith_op op (l',r') in - to_vec_int ord (size * (length_int l)) n - -let add_vec_int = arith_op_vec_int (+) false 1 -let add_vec_signed_int = arith_op_vec_int (+) true 1 -let minus_vec_int = arith_op_vec_int (-) false 1 -let multiply_vec_int = arith_op_vec_int ( * ) false 2 -let multiply_vec_signed_int = arith_op_vec_int ( * ) true 2 - -let add_vec = add_vec_big -let add_vec_signed = add_vec_signed_big -let minus_vec = minus_vec_big -let multiply_vec = multiply_vec_big -let multiply_vec_signed = multiply_vec_signed_big - - -let arith_op_vec_range_int op sign size (l,r) = - let ord = get_ord l in - arith_op_vec_int op sign size (l, to_vec_int ord (length_int l) r) - -let add_vec_range_int = arith_op_vec_range_int (+) false 1 -let add_vec_range_signed_int = arith_op_vec_range_int (+) true 1 -let minus_vec_range_int = arith_op_vec_range_int (-) false 1 -let mult_vec_range_int = arith_op_vec_range_int ( * ) false 2 -let mult_vec_range_signed_int = arith_op_vec_range_int ( * ) true 2 - -let arith_op_vec_range_big op sign size (l,r) = - let ord = get_ord l in - arith_op_vec_big op sign size (l, to_vec_big ord (length_big l) r) - -let add_vec_range_big = arith_op_vec_range_big add_big_int false unit_big_int -let add_vec_range_signed_big = arith_op_vec_range_big add_big_int true unit_big_int -let minus_vec_range_big = arith_op_vec_range_big sub_big_int false unit_big_int -let mult_vec_range_big = arith_op_vec_range_big mult_big_int false two_big_int -let mult_vec_range_signed_big = arith_op_vec_range_big mult_big_int true two_big_int - -let add_vec_range = add_vec_range_big -let add_vec_range_signed = add_vec_range_signed_big -let minus_vec_range = minus_vec_range_big -let mult_vec_range = mult_vec_range_big -let mult_vec_range_signed = mult_vec_range_signed_big - -let arith_op_range_vec_int op sign size (l,r) = - let ord = get_ord r in - arith_op_vec_int op sign size ((to_vec_int ord (length_int r) l), r) - -let add_range_vec_int = arith_op_range_vec_int (+) false 1 -let add_range_vec_signed_int = arith_op_range_vec_int (+) true 1 -let minus_range_vec_int = arith_op_range_vec_int (-) false 1 -let mult_range_vec_int = arith_op_range_vec_int ( * ) false 2 -let mult_range_vec_signed_int = arith_op_range_vec_int ( * ) true 2 - -let arith_op_range_vec_big op sign size (l,r) = - let ord = get_ord r in - arith_op_vec_big op sign size ((to_vec_big ord (length_big r) l), r) - -let add_range_vec_big = arith_op_range_vec_big add_big_int false unit_big_int -let add_range_vec_signed_big = arith_op_range_vec_big add_big_int true unit_big_int -let minus_range_vec_big = arith_op_range_vec_big sub_big_int false unit_big_int -let mult_range_vec_big = arith_op_range_vec_big mult_big_int false two_big_int -let mult_range_vec_signed_big = arith_op_range_vec_big mult_big_int true two_big_int - -let add_range_vec = add_range_vec_big -let add_range_vec_signed = add_range_vec_signed_big -let minus_range_vec = minus_range_vec_big -let mult_range_vec = mult_range_vec_big -let mult_range_vec_signed = mult_range_vec_signed_big - - -let arith_op_range_vec_range_int op sign (l,r) = arith_op op (l, to_num_int sign r) - -let add_range_vec_range_int = arith_op_range_vec_range_int (+) false -let add_range_vec_range_signed_int = arith_op_range_vec_range_int (+) true -let minus_range_vec_range_int = arith_op_range_vec_range_int (-) false - -let arith_op_range_vec_range_big op sign (l,r) = arith_op op (l, to_num_big sign r) - -let add_range_vec_range_big = arith_op_range_vec_range_big add_big_int false -let add_range_vec_range_signed_big = arith_op_range_vec_range_big add_big_int true -let minus_range_vec_range_big = arith_op_range_vec_range_big sub_big_int false - -let add_range_vec_range = add_range_vec_range_big -let add_range_vec_range_signed = add_range_vec_range_signed_big -let minus_range_vec_range = minus_range_vec_range_big - -let arith_op_vec_range_range_int op sign (l,r) = arith_op op (to_num_int sign l,r) - -let add_vec_range_range_int = arith_op_vec_range_range_int (+) false -let add_vec_range_range_signed_int = arith_op_vec_range_range_int (+) true -let minus_vec_range_range_int = arith_op_vec_range_range_int (-) false - -let arith_op_vec_range_range_big op sign (l,r) = arith_op op (to_num_big sign l,r) - -let add_vec_range_range_big = arith_op_vec_range_range_big add_big_int false -let add_vec_range_range_signed_big = arith_op_vec_range_range_big add_big_int true -let minus_vec_range_range_big = arith_op_vec_range_range_big sub_big_int false - -let add_vec_range_range = add_vec_range_range_big -let add_vec_range_range_signed = add_vec_range_range_signed_big -let minus_vec_range_range = minus_vec_range_range_big - - -let arith_op_vec_vec_range_int op sign (l,r) = - let (l',r') = (to_num_int sign l,to_num_int sign r) in - arith_op op (l',r') - -let add_vec_vec_range_int = arith_op_vec_vec_range_int (+) false -let add_vec_vec_range_signed_int = arith_op_vec_vec_range_int (+) true - -let arith_op_vec_vec_range_big op sign (l,r) = - let (l',r') = (to_num_big sign l,to_num_big sign r) in - arith_op op (l',r') - -let add_vec_vec_range_big = arith_op_vec_vec_range_big add_big_int false -let add_vec_vec_range_signed_big = arith_op_vec_vec_range_big add_big_int true - -let add_vec_vec_range = add_vec_vec_range_big -let add_vec_vec_range_signed = add_vec_vec_range_signed_big - -let arith_op_vec_bit_int op sign (l,r) = - let ord = get_ord l in - let l' = to_num_int sign l in - let n = arith_op op (l', match r with | Vone -> 1 | _ -> 0) in - to_vec_int ord (length_int l) n - -let add_vec_bit_int = arith_op_vec_bit_int (+) false -let add_vec_bit_signed_int = arith_op_vec_bit_int (+) true -let minus_vec_bit_int = arith_op_vec_bit_int (-) true - -let arith_op_vec_bit_big op sign (l,r) = - let ord = get_ord l in - let l' = to_num_big sign l in - let n = arith_op op (l', match r with | Vone -> unit_big_int | _ -> zero_big_int) in - to_vec_big ord (length_big l) n - -let add_vec_bit_big = arith_op_vec_bit_big add_big_int false -let add_vec_bit_signed_big = arith_op_vec_bit_big add_big_int true -let minus_vec_bit_big = arith_op_vec_bit_big sub_big_int true - -let add_vec_bit = add_vec_bit_big -let add_vec_bit_signed = add_vec_bit_signed_big -let minus_vec_bit = minus_vec_bit_big - - -let rec arith_op_overflow_vec_int op sign size (l,r) = - let ord = get_ord l in - let len = length_int l in - let act_size = len * size in - let (l_sign,r_sign) = (to_num_int sign l,to_num_int sign r) in - let (l_unsign,r_unsign) = (to_num_int false l,to_num_int false r) in - let n = arith_op op (l_sign,r_sign) in - let n_unsign = arith_op op (l_unsign,r_unsign) in - let correct_size_num = to_vec_int ord act_size n in - let one_more_size_u = to_vec_int ord (act_size +1) n_unsign in - let overflow = if (n <= (int_of_big_int (get_max_representable_in sign len))) && - (n >= (int_of_big_int (get_min_representable_in sign len))) - then Vzero - else Vone in - let c_out = most_significant one_more_size_u in - (correct_size_num,overflow,c_out) - -let add_overflow_vec_int = arith_op_overflow_vec_int (+) false 1 -let add_overflow_vec_signed_int = arith_op_overflow_vec_int (+) true 1 -let minus_overflow_vec_int = arith_op_overflow_vec_int (-) false 1 -let minus_overflow_vec_signed_int = arith_op_overflow_vec_int (-) true 1 -let mult_overflow_vec_int = arith_op_overflow_vec_int ( * ) false 2 -let mult_overflow_vec_signed_int = arith_op_overflow_vec_int ( * ) true 2 - -let rec arith_op_overflow_vec_big op sign size (l,r) = - let ord = get_ord l in - let len = length_big l in - let act_size = mult_big_int len size in - let (l_sign,r_sign) = (to_num_big sign l,to_num_big sign r) in - let (l_unsign,r_unsign) = (to_num_big false l,to_num_big false r) in - let n = arith_op op (l_sign,r_sign) in - let n_unsign = arith_op op (l_unsign,r_unsign) in - let correct_size_num = to_vec_big ord act_size n in - let one_more_size_u = to_vec_big ord (succ_big_int act_size) n_unsign in - let overflow = if (le_big_int n (get_max_representable_in sign (int_of_big_int len))) && - (ge_big_int n (get_min_representable_in sign (int_of_big_int len))) - then Vzero - else Vone in - let c_out = most_significant one_more_size_u in - (correct_size_num,overflow,c_out) - -let add_overflow_vec_big = arith_op_overflow_vec_big add_big_int false unit_big_int -let add_overflow_vec_signed_big = arith_op_overflow_vec_big add_big_int true unit_big_int -let minus_overflow_vec_big = arith_op_overflow_vec_big sub_big_int false unit_big_int -let minus_overflow_vec_signed_big = arith_op_overflow_vec_big sub_big_int true unit_big_int -let mult_overflow_vec_big = arith_op_overflow_vec_big mult_big_int false two_big_int -let mult_overflow_vec_signed_big = arith_op_overflow_vec_big mult_big_int true two_big_int - -let add_overflow_vec = add_overflow_vec_big -let add_overflow_vec_signed = add_overflow_vec_signed_big -let minus_overflow_vec = minus_overflow_vec_big -let minus_overflow_vec_signed = minus_overflow_vec_signed_big -let mult_overflow_vec = mult_overflow_vec_big -let mult_overflow_vec_signed = mult_overflow_vec_signed_big - -let rec arith_op_overflow_vec_bit_int op sign (l,r_bit) = - let ord = get_ord l in - let act_size = length_int l in - let l' = to_num_int sign l in - let l_u = to_num_int false l in - let (n,nu,changed) = match r_bit with - | Vone -> (arith_op op (l',1), arith_op op (l_u,1), true) - | Vzero -> (l',l_u,false) - | _ -> assert false - in - let correct_size_num = to_vec_int ord act_size n in - let one_larger = to_vec_int ord (1+ act_size) nu in - let overflow = - if changed - then if (n <= (int_of_big_int (get_max_representable_in sign act_size))) && - (n >= (int_of_big_int (get_min_representable_in sign act_size))) - then Vzero - else Vone - else Vone in - (correct_size_num,overflow,most_significant one_larger) - -let add_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (+) true -let minus_overflow_vec_bit_int = arith_op_overflow_vec_bit_int (-) false -let minus_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (-) true - -let rec arith_op_overflow_vec_bit_big op sign (l,r_bit) = - let ord = get_ord l in - let act_size = length_big l in - let l' = to_num_big sign l in - let l_u = to_num_big false l in - let (n,nu,changed) = match r_bit with - | Vone -> (arith_op op (l',unit_big_int), arith_op op (l_u,unit_big_int), true) - | Vzero -> (l',l_u,false) - | _ -> assert false - in - let correct_size_num = to_vec_big ord act_size n in - let one_larger = to_vec_big ord (succ_big_int act_size) nu in - let overflow = - if changed - then if (le_big_int n (get_max_representable_in sign (int_of_big_int act_size))) && - (ge_big_int n (get_min_representable_in sign (int_of_big_int act_size))) - then Vzero - else Vone - else Vone in - (correct_size_num,overflow,most_significant one_larger) - -let add_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big add_big_int true -let minus_overflow_vec_bit_big = arith_op_overflow_vec_bit_big sub_big_int false -let minus_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big sub_big_int true - -let add_overflow_vec_bit_signed = add_overflow_vec_bit_signed_big -let minus_overflow_vec_bit = minus_overflow_vec_bit_big -let minus_overflow_vec_bit_signed = minus_overflow_vec_bit_signed_big - -let shift_op_vec_int op (l,r) = - match l with - | Vvector(_,start,ord) | Vregister(_,start,ord,_,_) -> - let array = match l with | Vvector(array,_,_) -> array | Vregister(array,_,_,_,_) -> !array | _ -> assert false in - let len = Array.length array in - (match op with - | "<<" -> - if (r <= len) then - let left = Array.sub array r (len - r) in - let right = Array.make r Vzero in - let result = Array.append left right in - Vvector(result, start, ord) - else - Vvector(Array.make len Vzero, start, ord) - | ">>" -> - if (r <= len) then - let left = Array.make r Vzero in - let right = Array.sub array 0 (len - r) in - let result = Array.append left right in - Vvector(result, start, ord) - else - Vvector(Array.make len Vzero, start, ord) - | "<<<" -> - let rmod = r mod len in - let left = Array.sub array rmod (len - rmod) in - let right = Array.sub array 0 rmod in - let result = Array.append left right in - Vvector(result, start, ord) - | _ -> assert false) - | _ -> assert false - -let shift_op_vec_big op (l,r) = shift_op_vec_int op (l, int_of_big_int r) -let bitwise_leftshift_big = shift_op_vec_big "<<" -let bitwise_rightshift_big = shift_op_vec_big ">>" -let bitwise_rotate_big = shift_op_vec_big "<<<" - -let bitwise_leftshift = bitwise_leftshift_big -let bitwise_rightshift = bitwise_rightshift_big -let bitwise_rotate = bitwise_rotate_big - -let rec arith_op_no0_big op (l,r) = - if eq_big_int r zero_big_int - then None - else Some (op l r) - -let modulo_no0_big = arith_op_no0_big (Z.rem) -let quot_no0_big = arith_op_no0_big (Z.div) - -let rec arith_op_no0_int op (l,r) = - if r = 0 - then None - else Some (op l r) - -let rec arith_op_vec_no0_int op sign size (l,r) = - let ord = get_ord l in - let act_size = ((length_int l) * size) in - let (l',r') = (to_num_int sign l,to_num_int sign r) in - let n = arith_op_no0_int op (l',r') in - let representable,n' = - match n with - | Some n' -> - ((n' <= (int_of_big_int (get_max_representable_in sign act_size))) && - (n' >= (int_of_big_int (get_min_representable_in sign act_size)))), n' - | _ -> false,0 in - if representable - then to_vec_int ord act_size n' - else - match l with - | Vvector(_, start, _) | Vregister(_, start, _, _, _) -> - Vvector((Array.make act_size Vundef), start, ord) - | _ -> assert false - -let mod_vec_int = arith_op_vec_no0_int (mod) false 1 -let quot_vec_int = arith_op_vec_no0_int (/) false 1 -let quot_vec_signed_int = arith_op_vec_no0_int (/) true 1 - -let rec arith_op_vec_no0_big op sign size (l,r) = - let ord = get_ord l in - let act_size = int_of_big_int (mult_int_big_int (length_int l) size) in - let (l',r') = (to_num_big sign l,to_num_big sign r) in - let n = arith_op_no0_big op (l',r') in - let representable,n' = - match n with - | Some n' -> - ((le_big_int n' (get_max_representable_in sign act_size)) && - (ge_big_int n' (get_min_representable_in sign act_size))), n' - | _ -> false,zero_big_int in - if representable - then to_vec_big ord (big_int_of_int act_size) n' - else - match l with - | Vvector(_, start, _) | Vregister(_, start, _, _, _) -> - Vvector((Array.make act_size Vundef), start, ord) - | _ -> assert false - -let mod_vec_big = arith_op_vec_no0_big (Z.rem) false unit_big_int -let quot_vec_big = arith_op_vec_no0_big (Z.div) false unit_big_int -let quot_vec_signed_big = arith_op_vec_no0_big (Z.div) true unit_big_int - -let mod_vec = mod_vec_big -let quot_vec = quot_vec_big -let quot_vec_signed = quot_vec_signed_big - -let arith_op_overflow_no0_vec_int op sign size (l,r) = - let ord = get_ord l in - let rep_size = (length_int r) * size in - let act_size = (length_int l) * size in - let (l',r') = ((to_num_int sign l),(to_num_int sign r)) in - let (l_u,r_u) = (to_num_int false l,to_num_int false r) in - let n = arith_op_no0_int op (l',r') in - let n_u = arith_op_no0_int op (l_u,r_u) in - let representable,n',n_u' = - match n, n_u with - | Some n',Some n_u' -> - ((n' <= (int_of_big_int (get_max_representable_in sign rep_size))) && - (n' >= (int_of_big_int (get_min_representable_in sign rep_size))), n', n_u') - | _ -> true,0,0 in - let (correct_size_num,one_more) = - if representable then - (to_vec_int ord act_size n',to_vec_int ord (1+act_size) n_u') - else match l with - | Vvector(_, start, _) | Vregister(_, start, _, _, _) -> - Vvector((Array.make act_size Vundef), start, ord), - Vvector((Array.make (act_size + 1) Vundef), start, ord) - | _ -> assert false in - let overflow = if representable then Vzero else Vone in - (correct_size_num,overflow,most_significant one_more) - -let quot_overflow_vec_int = arith_op_overflow_no0_vec_int (/) false 1 -let quot_overflow_vec_signed_int = arith_op_overflow_no0_vec_int (/) true 1 - -let arith_op_overflow_no0_vec_big op sign size (l,r) = - let ord = get_ord l in - let rep_size = mult_big_int (length_big r) size in - let act_size = mult_big_int (length_big l) size in - let (l',r') = ((to_num_big sign l),(to_num_big sign r)) in - let (l_u,r_u) = (to_num_big false l,to_num_big false r) in - let n = arith_op_no0_big op (l',r') in - let n_u = arith_op_no0_big op (l_u,r_u) in - let representable,n',n_u' = - match n, n_u with - | Some n',Some n_u' -> - ((le_big_int n' (get_max_representable_in sign (int_of_big_int rep_size))) && - (ge_big_int n' (get_min_representable_in sign (int_of_big_int rep_size))), n', n_u') - | _ -> true,zero_big_int,zero_big_int in - let (correct_size_num,one_more) = - if representable then - (to_vec_big ord act_size n',to_vec_big ord (succ_big_int act_size) n_u') - else match l with - | Vvector(_, start, _) | Vregister(_, start, _, _, _) -> - Vvector((Array.make (int_of_big_int act_size) Vundef), start, ord), - Vvector((Array.make ((int_of_big_int act_size) + 1) Vundef), start, ord) - | _ -> assert false in - let overflow = if representable then Vzero else Vone in - (correct_size_num,overflow,most_significant one_more) - -let quot_overflow_vec_big = arith_op_overflow_no0_vec_big (Z.div) false unit_big_int -let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big (Z.div) true unit_big_int - -let quot_overflow_vec = quot_overflow_vec_big -let quot_overflow_vec_signed = quot_overflow_vec_signed_big - - -let arith_op_vec_range_no0_int op sign size (l,r) = - let ord = get_ord l in - arith_op_vec_no0_int op sign size (l,(to_vec_int ord (length_int l) r)) - -let mod_vec_range_int = arith_op_vec_range_no0_int (mod) false 1 - -let arith_op_vec_range_no0_big op sign size (l,r) = - let ord = get_ord l in - arith_op_vec_no0_big op sign size (l,(to_vec_big ord (length_big l) r)) - -let mod_vec_range_big = arith_op_vec_range_no0_big (Z.rem) false unit_big_int - -let mod_vec_range = mod_vec_range_big - -(* XXX Need to have a default top level direction reference I think*) -let duplicate_int (bit,length) = - Vvector((Array.make length bit), (length-1), false) - -let duplicate_big (bit,length) = - duplicate_int (bit, int_of_big_int length) - -let duplicate = duplicate_big - -let duplicate_bits_big (bits, x) = - let len = (length_int bits) * (int_of_big_int x) in - let is_inc = get_ord bits in - let bits_arr = get_barray bits in - let arr = Array.concat (Array.to_list(Array.make (int_of_big_int x) bits_arr)) in - Vvector(arr, (if is_inc then 0 else (len - 1)), is_inc) - -let duplicate_bits = duplicate_bits_big - -let compare_op op (l,r) = - if (op l r) - then Vone - else Vzero - -let lt_big = compare_op lt_big_int -let gt_big = compare_op gt_big_int -let lteq_big = compare_op le_big_int -let gteq_big = compare_op ge_big_int -let lt_int : (int* int) -> vbit = compare_op (<) -let gt_int : (int * int) -> vbit = compare_op (>) -let lteq_int : (int * int) -> vbit = compare_op (<=) -let gteq_int : (int*int) -> vbit = compare_op (>=) - -let lt = lt_big -let gt = gt_big -let lteq = lteq_big -let gteq = gteq_big - -let compare_op_vec_int op sign (l,r) = - let (l',r') = (to_num_int sign l, to_num_int sign r) in - compare_op op (l',r') - -let lt_vec_int = compare_op_vec_int (<) true -let gt_vec_int = compare_op_vec_int (>) true -let lteq_vec_int = compare_op_vec_int (<=) true -let gteq_vec_int = compare_op_vec_int (>=) true -let lt_vec_signed_int = compare_op_vec_int (<) true -let gt_vec_signed_int = compare_op_vec_int (>) true -let lteq_vec_signed_int = compare_op_vec_int (<=) true -let gteq_vec_signed_int = compare_op_vec_int (>=) true -let lt_vec_unsigned_int = compare_op_vec_int (<) false -let gt_vec_unsigned_int = compare_op_vec_int (>) false -let lteq_vec_unsigned_int = compare_op_vec_int (<=) false -let gteq_vec_unsigned_int = compare_op_vec_int (>=) false - -let compare_op_vec_big op sign (l,r) = - let (l',r') = (to_num_big sign l, to_num_big sign r) in - compare_op op (l',r') - -let lt_vec_big = compare_op_vec_big lt_big_int true -let gt_vec_big = compare_op_vec_big gt_big_int true -let lteq_vec_big = compare_op_vec_big le_big_int true -let gteq_vec_big = compare_op_vec_big ge_big_int true -let lt_vec_signed_big = compare_op_vec_big lt_big_int true -let gt_vec_signed_big = compare_op_vec_big gt_big_int true -let lteq_vec_signed_big = compare_op_vec_big le_big_int true -let gteq_vec_signed_big = compare_op_vec_big ge_big_int true -let lt_vec_unsigned_big = compare_op_vec_big lt_big_int false -let gt_vec_unsigned_big = compare_op_vec_big gt_big_int false -let lteq_vec_unsigned_big = compare_op_vec_big le_big_int false -let gteq_vec_unsigned_big = compare_op_vec_big ge_big_int false - -let lt_vec = lt_vec_big -let gt_vec = gt_vec_big -let lteq_vec = lteq_vec_big -let gteq_vec = gteq_vec_big -let lt_vec_signed = lt_vec_signed_big -let gt_vec_signed = gt_vec_signed_big -let lteq_vec_signed = lteq_vec_signed_big -let gteq_vec_signed = gteq_vec_signed_big -let lt_vec_unsigned = lt_vec_unsigned_big -let gt_vec_unsigned = gt_vec_unsigned_big -let lteq_vec_unsigned = lteq_vec_unsigned_big -let gteq_vec_unsigned = gteq_vec_unsigned_big - -let compare_op_vec_range_int op sign (l,r) = - compare_op op ((to_num_int sign l),r) - -let lt_vec_range_int = compare_op_vec_range_int (<) true -let gt_vec_range_int = compare_op_vec_range_int (>) true -let lteq_vec_range_int = compare_op_vec_range_int (<=) true -let gteq_vec_range_int = compare_op_vec_range_int (>=) true - -let compare_op_vec_range_big op sign (l,r) = - compare_op op ((to_num_big sign l),r) - -let lt_vec_range_big = compare_op_vec_range_big lt_big_int true -let gt_vec_range_big = compare_op_vec_range_big gt_big_int true -let lteq_vec_range_big = compare_op_vec_range_big le_big_int true -let gteq_vec_range_big = compare_op_vec_range_big ge_big_int true - -let lt_vec_range = lt_vec_range_big -let gt_vec_range = gt_vec_range_big -let lteq_vec_range = lteq_vec_range_big -let gteq_vec_range = gteq_vec_range_big - -let compare_op_range_vec_int op sign (l,r) = - compare_op op (l, (to_num_int sign r)) - -let lt_range_vec_int = compare_op_range_vec_int (<) true -let gt_range_vec_int = compare_op_range_vec_int (>) true -let lteq_range_vec_int = compare_op_range_vec_int (<=) true -let gteq_range_vec_int = compare_op_range_vec_int (>=) true - -let compare_op_range_vec_big op sign (l,r) = - compare_op op (l, (to_num_big sign r)) - -let lt_range_vec_big = compare_op_range_vec_big lt_big_int true -let gt_range_vec_big = compare_op_range_vec_big gt_big_int true -let lteq_range_vec_big = compare_op_range_vec_big le_big_int true -let gteq_range_vec_big = compare_op_range_vec_big ge_big_int true - -let lt_range_vec = lt_range_vec_big -let gt_range_vec = gt_range_vec_big -let lteq_range_vec = lteq_range_vec_big -let gteq_range_vec = gteq_range_vec_big - -let eq (l,r) = if l = r then Vone else Vzero -let eq_vec_vec (l,r) = eq (to_num_big true l, to_num_big true r) -let eq_vec (l,r) = eq_vec_vec(l,r) -let eq_vec_range (l,r) = eq (to_num_big false l,r) -let eq_range_vec (l,r) = eq (l, to_num_big false r) -let eq_range = eq -let eq_bit = bitwise_binop_bit (=) - -let neq (l,r) = bitwise_not_bit (eq (l,r)) -let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r)) -let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) -let neq_bit (l,r) = bitwise_not_bit (eq_bit(l,r)) -let neq_range = neq - -let mask (n,v) = - let n' = int_of_big_int n in - match v with - | Vvector (bits,start,dir) -> - let current_size = Array.length bits in - let to_drop = (current_size - n') in - let bits' = Array.sub bits to_drop n' in - Vvector (bits',(if dir then 0 else n'-1), dir) - | Vregister (bits,start,dir,name,fields) -> - let current_size = Array.length !bits in - let to_drop = (current_size - n') in - let bits' = Array.sub !bits to_drop n' in - Vvector (bits',(if dir then 0 else n'-1), dir) - | VvectorR _ -> failwith "mask not implemented for VregisterR" - | Vbit _ -> failwith "mask called for bit" - -let slice_raw (v, i, j) = - let i' = int_of_big_int i in - let j' = int_of_big_int j in - match v with - | Vvector (bs, start, is_inc) -> - let bits = Array.sub bs i' (j'-i'+1) in - let len = Array.length bits in - Vvector (bits, (if is_inc then 0 else len - 1), is_inc) - | _ -> failwith "slice_raw only implemented for VVector" -let _slice_raw = slice_raw - -(* enough literal big ints to account for most literals found in specs *) -(* for i = 0 to 257 do Printf.printf "let bi%d = big_int_of_int %d\n" i i done;; *) -let bi0 = zero_big_int -let bi1 = unit_big_int -let bi2 = big_int_of_int 2 -let bi3 = big_int_of_int 3 -let bi4 = big_int_of_int 4 -let bi5 = big_int_of_int 5 -let bi6 = big_int_of_int 6 -let bi7 = big_int_of_int 7 -let bi8 = big_int_of_int 8 -let bi9 = big_int_of_int 9 -let bi10 = big_int_of_int 10 -let bi11 = big_int_of_int 11 -let bi12 = big_int_of_int 12 -let bi13 = big_int_of_int 13 -let bi14 = big_int_of_int 14 -let bi15 = big_int_of_int 15 -let bi16 = big_int_of_int 16 -let bi17 = big_int_of_int 17 -let bi18 = big_int_of_int 18 -let bi19 = big_int_of_int 19 -let bi20 = big_int_of_int 20 -let bi21 = big_int_of_int 21 -let bi22 = big_int_of_int 22 -let bi23 = big_int_of_int 23 -let bi24 = big_int_of_int 24 -let bi25 = big_int_of_int 25 -let bi26 = big_int_of_int 26 -let bi27 = big_int_of_int 27 -let bi28 = big_int_of_int 28 -let bi29 = big_int_of_int 29 -let bi30 = big_int_of_int 30 -let bi31 = big_int_of_int 31 -let bi32 = big_int_of_int 32 -let bi33 = big_int_of_int 33 -let bi34 = big_int_of_int 34 -let bi35 = big_int_of_int 35 -let bi36 = big_int_of_int 36 -let bi37 = big_int_of_int 37 -let bi38 = big_int_of_int 38 -let bi39 = big_int_of_int 39 -let bi40 = big_int_of_int 40 -let bi41 = big_int_of_int 41 -let bi42 = big_int_of_int 42 -let bi43 = big_int_of_int 43 -let bi44 = big_int_of_int 44 -let bi45 = big_int_of_int 45 -let bi46 = big_int_of_int 46 -let bi47 = big_int_of_int 47 -let bi48 = big_int_of_int 48 -let bi49 = big_int_of_int 49 -let bi50 = big_int_of_int 50 -let bi51 = big_int_of_int 51 -let bi52 = big_int_of_int 52 -let bi53 = big_int_of_int 53 -let bi54 = big_int_of_int 54 -let bi55 = big_int_of_int 55 -let bi56 = big_int_of_int 56 -let bi57 = big_int_of_int 57 -let bi58 = big_int_of_int 58 -let bi59 = big_int_of_int 59 -let bi60 = big_int_of_int 60 -let bi61 = big_int_of_int 61 -let bi62 = big_int_of_int 62 -let bi63 = big_int_of_int 63 -let bi64 = big_int_of_int 64 -let bi65 = big_int_of_int 65 -let bi66 = big_int_of_int 66 -let bi67 = big_int_of_int 67 -let bi68 = big_int_of_int 68 -let bi69 = big_int_of_int 69 -let bi70 = big_int_of_int 70 -let bi71 = big_int_of_int 71 -let bi72 = big_int_of_int 72 -let bi73 = big_int_of_int 73 -let bi74 = big_int_of_int 74 -let bi75 = big_int_of_int 75 -let bi76 = big_int_of_int 76 -let bi77 = big_int_of_int 77 -let bi78 = big_int_of_int 78 -let bi79 = big_int_of_int 79 -let bi80 = big_int_of_int 80 -let bi81 = big_int_of_int 81 -let bi82 = big_int_of_int 82 -let bi83 = big_int_of_int 83 -let bi84 = big_int_of_int 84 -let bi85 = big_int_of_int 85 -let bi86 = big_int_of_int 86 -let bi87 = big_int_of_int 87 -let bi88 = big_int_of_int 88 -let bi89 = big_int_of_int 89 -let bi90 = big_int_of_int 90 -let bi91 = big_int_of_int 91 -let bi92 = big_int_of_int 92 -let bi93 = big_int_of_int 93 -let bi94 = big_int_of_int 94 -let bi95 = big_int_of_int 95 -let bi96 = big_int_of_int 96 -let bi97 = big_int_of_int 97 -let bi98 = big_int_of_int 98 -let bi99 = big_int_of_int 99 -let bi100 = big_int_of_int 100 -let bi101 = big_int_of_int 101 -let bi102 = big_int_of_int 102 -let bi103 = big_int_of_int 103 -let bi104 = big_int_of_int 104 -let bi105 = big_int_of_int 105 -let bi106 = big_int_of_int 106 -let bi107 = big_int_of_int 107 -let bi108 = big_int_of_int 108 -let bi109 = big_int_of_int 109 -let bi110 = big_int_of_int 110 -let bi111 = big_int_of_int 111 -let bi112 = big_int_of_int 112 -let bi113 = big_int_of_int 113 -let bi114 = big_int_of_int 114 -let bi115 = big_int_of_int 115 -let bi116 = big_int_of_int 116 -let bi117 = big_int_of_int 117 -let bi118 = big_int_of_int 118 -let bi119 = big_int_of_int 119 -let bi120 = big_int_of_int 120 -let bi121 = big_int_of_int 121 -let bi122 = big_int_of_int 122 -let bi123 = big_int_of_int 123 -let bi124 = big_int_of_int 124 -let bi125 = big_int_of_int 125 -let bi126 = big_int_of_int 126 -let bi127 = big_int_of_int 127 -let bi128 = big_int_of_int 128 -let bi129 = big_int_of_int 129 -let bi130 = big_int_of_int 130 -let bi131 = big_int_of_int 131 -let bi132 = big_int_of_int 132 -let bi133 = big_int_of_int 133 -let bi134 = big_int_of_int 134 -let bi135 = big_int_of_int 135 -let bi136 = big_int_of_int 136 -let bi137 = big_int_of_int 137 -let bi138 = big_int_of_int 138 -let bi139 = big_int_of_int 139 -let bi140 = big_int_of_int 140 -let bi141 = big_int_of_int 141 -let bi142 = big_int_of_int 142 -let bi143 = big_int_of_int 143 -let bi144 = big_int_of_int 144 -let bi145 = big_int_of_int 145 -let bi146 = big_int_of_int 146 -let bi147 = big_int_of_int 147 -let bi148 = big_int_of_int 148 -let bi149 = big_int_of_int 149 -let bi150 = big_int_of_int 150 -let bi151 = big_int_of_int 151 -let bi152 = big_int_of_int 152 -let bi153 = big_int_of_int 153 -let bi154 = big_int_of_int 154 -let bi155 = big_int_of_int 155 -let bi156 = big_int_of_int 156 -let bi157 = big_int_of_int 157 -let bi158 = big_int_of_int 158 -let bi159 = big_int_of_int 159 -let bi160 = big_int_of_int 160 -let bi161 = big_int_of_int 161 -let bi162 = big_int_of_int 162 -let bi163 = big_int_of_int 163 -let bi164 = big_int_of_int 164 -let bi165 = big_int_of_int 165 -let bi166 = big_int_of_int 166 -let bi167 = big_int_of_int 167 -let bi168 = big_int_of_int 168 -let bi169 = big_int_of_int 169 -let bi170 = big_int_of_int 170 -let bi171 = big_int_of_int 171 -let bi172 = big_int_of_int 172 -let bi173 = big_int_of_int 173 -let bi174 = big_int_of_int 174 -let bi175 = big_int_of_int 175 -let bi176 = big_int_of_int 176 -let bi177 = big_int_of_int 177 -let bi178 = big_int_of_int 178 -let bi179 = big_int_of_int 179 -let bi180 = big_int_of_int 180 -let bi181 = big_int_of_int 181 -let bi182 = big_int_of_int 182 -let bi183 = big_int_of_int 183 -let bi184 = big_int_of_int 184 -let bi185 = big_int_of_int 185 -let bi186 = big_int_of_int 186 -let bi187 = big_int_of_int 187 -let bi188 = big_int_of_int 188 -let bi189 = big_int_of_int 189 -let bi190 = big_int_of_int 190 -let bi191 = big_int_of_int 191 -let bi192 = big_int_of_int 192 -let bi193 = big_int_of_int 193 -let bi194 = big_int_of_int 194 -let bi195 = big_int_of_int 195 -let bi196 = big_int_of_int 196 -let bi197 = big_int_of_int 197 -let bi198 = big_int_of_int 198 -let bi199 = big_int_of_int 199 -let bi200 = big_int_of_int 200 -let bi201 = big_int_of_int 201 -let bi202 = big_int_of_int 202 -let bi203 = big_int_of_int 203 -let bi204 = big_int_of_int 204 -let bi205 = big_int_of_int 205 -let bi206 = big_int_of_int 206 -let bi207 = big_int_of_int 207 -let bi208 = big_int_of_int 208 -let bi209 = big_int_of_int 209 -let bi210 = big_int_of_int 210 -let bi211 = big_int_of_int 211 -let bi212 = big_int_of_int 212 -let bi213 = big_int_of_int 213 -let bi214 = big_int_of_int 214 -let bi215 = big_int_of_int 215 -let bi216 = big_int_of_int 216 -let bi217 = big_int_of_int 217 -let bi218 = big_int_of_int 218 -let bi219 = big_int_of_int 219 -let bi220 = big_int_of_int 220 -let bi221 = big_int_of_int 221 -let bi222 = big_int_of_int 222 -let bi223 = big_int_of_int 223 -let bi224 = big_int_of_int 224 -let bi225 = big_int_of_int 225 -let bi226 = big_int_of_int 226 -let bi227 = big_int_of_int 227 -let bi228 = big_int_of_int 228 -let bi229 = big_int_of_int 229 -let bi230 = big_int_of_int 230 -let bi231 = big_int_of_int 231 -let bi232 = big_int_of_int 232 -let bi233 = big_int_of_int 233 -let bi234 = big_int_of_int 234 -let bi235 = big_int_of_int 235 -let bi236 = big_int_of_int 236 -let bi237 = big_int_of_int 237 -let bi238 = big_int_of_int 238 -let bi239 = big_int_of_int 239 -let bi240 = big_int_of_int 240 -let bi241 = big_int_of_int 241 -let bi242 = big_int_of_int 242 -let bi243 = big_int_of_int 243 -let bi244 = big_int_of_int 244 -let bi245 = big_int_of_int 245 -let bi246 = big_int_of_int 246 -let bi247 = big_int_of_int 247 -let bi248 = big_int_of_int 248 -let bi249 = big_int_of_int 249 -let bi250 = big_int_of_int 250 -let bi251 = big_int_of_int 251 -let bi252 = big_int_of_int 252 -let bi253 = big_int_of_int 253 -let bi254 = big_int_of_int 254 -let bi255 = big_int_of_int 255 -let bi256 = big_int_of_int 256 -let bi257 = big_int_of_int 257 diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml index ae58f7b2..6ee0e963 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -72,7 +72,7 @@ let lem_dir = let lem = lem_dir / "lem" ;; (* All -wl ignores should be removed if you want to see the pattern compilation, exhaustive, and unused var warnings *) -let lem_opts = [A "-lib"; P "../lem_interp"; +let lem_opts = [A "-lib"; P "../gen_lib"; A "-wl_pat_comp"; P "ign"; A "-wl_pat_exh"; P "ign"; A "-wl_pat_fail"; P "ign"; diff --git a/src/util.ml b/src/util.ml index b44c5dfb..b997005e 100644 --- a/src/util.ml +++ b/src/util.ml @@ -394,6 +394,13 @@ let rec drop n xs = match n, xs with | n, [] -> [] | n, (x :: xs) -> drop (n - 1) xs +let list_init len f = + let rec list_init' len f acc = + if acc >= len then [] + else f acc :: list_init' len f (acc + 1) + in + list_init' len f 0 + let termcode n = if !opt_colors then "\x1B[" ^ string_of_int n ^ "m" diff --git a/src/util.mli b/src/util.mli index b74442a2..596b298d 100644 --- a/src/util.mli +++ b/src/util.mli @@ -219,6 +219,8 @@ module ExtraSet : functor (S : Set.S) -> val list_inter : S.t list -> S.t end +val list_init : int -> (int -> 'a) -> 'a list + (*Formatting functions*) val string_of_list : string -> ('a -> string) -> 'a list -> string diff --git a/src/value2.lem b/src/value2.lem new file mode 100644 index 00000000..09d74520 --- /dev/null +++ b/src/value2.lem @@ -0,0 +1,99 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open import Pervasives +open import Assert_extra +open Map + +open import Sail_values + +type vl = + | V_vector of list vl + | V_list of list vl + | V_bits of list bitU + | V_bit of bitU + | V_tuple of list vl + | V_bool of bool + | V_nondet (* Special nondeterministic boolean *) + | V_unit + | V_int of integer + | V_string of string + | V_ctor of string * list vl + | V_ctor_kind of string + | V_record of list (string * vl) + | V_null (* Used for unitialized values and null pointers in C compilation *) + +let string_of_value = function + | V_bits bs -> show_bitlist bs ^ "ul" + | V_int i -> show i ^ "l" + | V_bool true -> "true" + | V_bool false -> "false" + | V_null -> "NULL" + | V_unit -> "UNIT" + | V_bit B0 -> "0ul" + | V_bit B1 -> "1ul" + | V_string str -> "\"" ^ str ^ "\"" + | _ -> failwith "Cannot convert value to string" +end + +let primops extern args = + match (extern, args) with + | ("and_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 && b2) + | ("and_bool", [V_nondet; V_bool false]) -> V_bool false + | ("and_bool", [V_bool false; V_nondet]) -> V_bool false + | ("and_bool", _) -> V_nondet + + | ("or_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 || b2) + | ("or_bool", [V_nondet; V_bool true]) -> V_bool true + | ("or_bool", [V_bool true; V_nondet]) -> V_bool true + | ("or_bool", _) -> V_nondet + + | _ -> failwith ("Unimplemented primitive operation " ^ extern) + end |