summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/_tags11
-rw-r--r--src/bitfield.ml51
-rw-r--r--src/initial_check.ml7
-rw-r--r--src/interpreter.ml222
-rw-r--r--src/isail.ml113
-rw-r--r--src/myocamlbuild.ml5
-rw-r--r--src/ocaml_backend.ml2
-rw-r--r--src/rewrites.ml3
-rw-r--r--src/sail.ml8
-rw-r--r--src/sail_lib.ml4
-rw-r--r--src/type_check.ml16
-rw-r--r--src/type_check.mli2
-rw-r--r--src/value.ml104
13 files changed, 451 insertions, 97 deletions
diff --git a/src/_tags b/src/_tags
index efe34d17..f1d54db1 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,15 +1,16 @@
true: -traverse, debug, use_menhir
<**/*.ml>: bin_annot, annot
# <lem_interp> or <test>: include
-<sail.{byte,native}>: package(zarith), use_pprint, use_nums, use_unix, use_str, use_lem
-<isail.{byte,native}>: package(zarith), package(linenoise), use_pprint, use_nums, use_unix, use_str, use_lem
+<sail.{byte,native}>: package(zarith), use_pprint, use_unix, use_str, package(lem)
+<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}>: use_lem
+<*.m{l,li}>: package(lem)
# see http://caml.inria.fr/mantis/view.php?id=4943
-<lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, use_lem
-<test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str
+<lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, package(lem)
+<test/*> and not <test/*.cmxa>: use_nums, package(lem), use_str
# disable partial match and unused variable warnings
<**/*.ml>: warn_y
diff --git a/src/bitfield.ml b/src/bitfield.ml
index 0a32654d..db3411b1 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -1,3 +1,52 @@
+(**************************************************************************)
+(* 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. *)
+(**************************************************************************)
module Big_int = Nat_big_num
@@ -18,6 +67,7 @@ let newtype name size order =
let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in
ast_of_def_string order nt
+(* These functions define the getter and setter for all the bits in the field. *)
let full_getter name size order =
let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in
let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in
@@ -41,6 +91,7 @@ let full_overload name order =
let full_accessor name size order =
combine [full_getter name size order; full_setter name size order; full_overload name order]
+(* For every index range, create a getter and setter *)
let index_range_getter' name field order start stop =
let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
let irg_val = Printf.sprintf "val _get_%s : %s -> %s" field name (bitvec size order) in
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4e466596..28579291 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -964,7 +964,8 @@ let typschm_of_string order str =
let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
typschm
-let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false))
+let extern_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> Some (string_of_id id)), false))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, (fun _ -> None), false))
let val_spec_ids (Defs defs) =
let val_spec_id (VS_aux (vs_aux, _)) =
@@ -1003,7 +1004,7 @@ let have_undefined_builtins = ref false
let generate_undefineds vs_ids (Defs defs) =
let gen_vs id str =
- if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
+ if (IdSet.mem id vs_ids) then [] else [extern_of_string dec_ord id str]
in
let undefined_builtins =
if !have_undefined_builtins then
@@ -1022,7 +1023,7 @@ let generate_undefineds vs_ids (Defs defs) =
gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
(* FIXME: How to handle inc/dec order correctly? *)
- gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type). (atom('n), 'a) -> vector('n, dec,'a) effect {undef}";
+ gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
(* Only used with lem_mwords *)
gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 7a4b6b33..59b20a17 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -54,7 +54,7 @@ open Value
type gstate =
{ registers : value Bindings.t;
- letbinds : (Type_check.tannot letbind) list
+ letbinds : (Type_check.tannot letbind) list;
}
type lstate =
@@ -70,7 +70,7 @@ let rec ast_letbinds (Defs defs) =
let initial_gstate ast =
{ registers = Bindings.empty;
- letbinds = ast_letbinds ast
+ letbinds = ast_letbinds ast;
}
let initial_lstate =
@@ -179,6 +179,22 @@ let assertion_failed msg = Yield (Assertion_failed msg)
let liftM2 f m1 m2 = m1 >>= fun x -> m2 >>= fun y -> return (f x y)
+let rec pat_ids (P_aux (pat_aux, _)) =
+ match pat_aux with
+ | P_lit _ | P_wild -> IdSet.empty
+ | P_id id -> IdSet.singleton id
+ | P_as (pat, id) -> IdSet.add id (pat_ids pat)
+ | P_var (pat, _) | P_typ (_, pat) -> pat_ids pat
+ | P_app (_, pats) | P_tup pats | P_vector pats | P_vector_concat pats | P_list pats ->
+ List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty
+ | P_cons (pat1, pat2) ->
+ IdSet.union (pat_ids pat1) (pat_ids pat2)
+ | P_record (fpats, _) ->
+ List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty
+and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat
+
+let letbind_pat_ids (LB_aux (LB_val (pat, _), _)) = pat_ids pat
+
let rec subst id value (E_aux (e_aux, annot) as exp) =
let wrap e_aux = E_aux (e_aux, annot) in
let e_aux = match e_aux with
@@ -187,34 +203,96 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
| E_id id' -> if Id.compare id id' = 0 then unaux_exp (exp_of_value value) else E_id id'
| E_lit lit -> E_lit lit
| E_cast (typ, exp) -> E_cast (typ, subst id value exp)
+
| E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps)
| E_app_infix (exp1, op, exp2) -> E_app_infix (subst id value exp1, op, subst id value exp2)
+
| E_tuple exps -> E_tuple (List.map (subst id value) exps)
- | E_assign (lexp, exp) -> E_assign (subst_lexp id value lexp, subst id value exp) (* Shadowing... *)
- | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
- (* TODO: Fix shadowing *)
- E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot), subst id value body)
+
| E_if (cond, then_exp, else_exp) ->
E_if (subst id value cond, subst id value then_exp, subst id value else_exp)
+
+ | E_loop (loop, cond, body) ->
+ E_loop (loop, subst id value cond, subst id value body)
+ | E_for (id', exp1, exp2, exp3, order, body) when Id.compare id id' = 0 ->
+ E_for (id', exp1, exp2, exp3, order, body)
+ | E_for (id', exp1, exp2, exp3, order, body) ->
+ E_for (id', subst id value exp1, subst id value exp2, subst id value exp3, order, subst id value body)
+
| E_vector exps -> E_vector (List.map (subst id value) exps)
+ | E_vector_access (exp1, exp2) -> E_vector_access (subst id value exp1, subst id value exp2)
+ | E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (subst id value exp1, subst id value exp2, subst id value exp3)
+ | E_vector_update (exp1, exp2, exp3) -> E_vector_update (subst id value exp1, subst id value exp2, subst id value exp3)
+ | E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
+ E_vector_update_subrange (subst id value exp1, subst id value exp2, subst id value exp3, subst id value exp4)
+ | E_vector_append (exp1, exp2) -> E_vector_append (subst id value exp1, subst id value exp2)
+
+ | E_list exps -> E_list (List.map (subst id value) exps)
+ | E_cons (exp1, exp2) -> E_cons (subst id value exp1, subst id value exp2)
+
+ | E_record fexps -> E_record (subst_fexps id value fexps)
+ | E_record_update (exp, fexps) -> E_record_update (subst id value exp, subst_fexps id value fexps)
+ | E_field (exp, id') -> E_field (subst id value exp, id')
+
+ | E_case (exp, pexps) ->
+ E_case (subst id value exp, List.map (subst_pexp id value) pexps)
+
+ | E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
+ E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot),
+ if IdSet.mem id (pat_ids pat) then body else subst id value body)
+
+ | E_assign (lexp, exp) -> E_assign (subst_lexp id value lexp, subst id value exp) (* Shadowing... *)
+
+ (* Should be re-written *)
+ | E_sizeof nexp -> E_sizeof nexp
+ | E_constraint nc -> E_constraint nc
+
| E_return exp -> E_return (subst id value exp)
+ | E_exit exp -> E_exit (subst id value exp)
+ (* Not sure about this, but id should always be immutable while id' must be mutable so should be ok. *)
+ | E_ref id' -> E_ref id'
+ | E_throw exp -> E_throw (subst id value exp)
+
+ | E_try (exp, pexps) ->
+ E_try (subst id value exp, List.map (subst_pexp id value) pexps)
+
| E_assert (exp1, exp2) -> E_assert (subst id value exp1, subst id value exp2)
+
| E_internal_value v -> E_internal_value v
| _ -> failwith ("subst " ^ string_of_exp exp)
in
wrap e_aux
+and subst_pexp id value (Pat_aux (pexp_aux, annot)) =
+ let pexp_aux = match pexp_aux with
+ | Pat_exp (pat, exp) when IdSet.mem id (pat_ids pat) -> Pat_exp (pat, exp)
+ | Pat_exp (pat, exp) -> Pat_exp (pat, subst id value exp)
+ | Pat_when (pat, guard, exp) when IdSet.mem id (pat_ids pat) -> Pat_when (pat, guard, exp)
+ | Pat_when (pat, guard, exp) -> Pat_when (pat, subst id value guard, subst id value exp)
+ in
+ Pat_aux (pexp_aux, annot)
+
+
+and subst_fexps id value (FES_aux (FES_Fexps (fexps, flag), annot)) =
+ FES_aux (FES_Fexps (List.map (subst_fexp id value) fexps, flag), annot)
+
+and subst_fexp id value (FE_aux (FE_Fexp (id', exp), annot)) =
+ FE_aux (FE_Fexp (id', subst id value exp), annot)
+
and subst_lexp id value (LEXP_aux (lexp_aux, annot) as lexp) =
let wrap lexp_aux = LEXP_aux (lexp_aux, annot) in
let lexp_aux = match lexp_aux with
| LEXP_deref exp -> LEXP_deref (subst id value exp)
| LEXP_id id' -> LEXP_id id'
| LEXP_memory (f, exps) -> LEXP_memory (f, List.map (subst id value) exps)
- | _ -> failwith ("subst lexp")
+ | LEXP_cast (typ, id') -> LEXP_cast (typ, id')
+ | LEXP_tup lexps -> LEXP_tup (List.map (subst_lexp id value) lexps)
+ | LEXP_vector (lexp, exp) -> LEXP_vector (subst_lexp id value lexp, subst id value exp)
+ | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (subst_lexp id value lexp, subst id value exp1, subst id value exp2)
+ | LEXP_field (lexp, id') -> LEXP_field (subst_lexp id value lexp, id')
in
wrap lexp_aux
-
(**************************************************************************)
(* 2. Expression Evaluation *)
(**************************************************************************)
@@ -224,13 +302,14 @@ let unit_exp = E_lit (L_aux (L_unit, Parse_ast.Unknown))
let is_value_fexp (FE_aux (FE_Fexp (id, exp), _)) = is_value exp
let value_of_fexp (FE_aux (FE_Fexp (id, exp), _)) = (string_of_id id, value_of_exp exp)
-let rec build_letchain lbs (E_aux (_, annot) as exp) =
- print_endline ("LETCHAIN " ^ string_of_exp exp);
+let rec build_letchain id lbs (E_aux (_, annot) as exp) =
+ (* print_endline ("LETCHAIN " ^ string_of_exp exp); *)
match lbs with
| [] -> exp
- | lb :: lbs ->
+ | lb :: lbs when IdSet.mem id (letbind_pat_ids lb)->
let exp = E_aux (E_let (lb, exp), annot) in
- build_letchain lbs exp
+ build_letchain id lbs exp
+ | _ :: lbs -> build_letchain id lbs exp
let rec step (E_aux (e_aux, annot) as orig_exp) =
let wrap e_aux' = return (E_aux (e_aux', annot)) in
@@ -248,6 +327,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_if (exp, then_exp, else_exp) ->
step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp))
+ | E_loop (While, exp, body) when not (is_value exp) ->
+ step exp >>= fun exp' -> wrap (E_loop (While, exp', body))
+ | E_loop (While, exp, body) when is_true exp -> wrap (E_block [body; orig_exp])
+ | E_loop (While, exp, body) when is_false exp -> wrap unit_exp
+ | E_loop _ -> assert false (* Impossible *)
+
| E_assert (exp, msg) when is_true exp -> wrap unit_exp
| E_assert (exp, msg) when is_false exp -> assertion_failed "FIXME"
| E_assert (exp, msg) ->
@@ -262,6 +347,15 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| [] -> return (exp_of_value (V_vector (List.map value_of_exp evaluated)))
end
+ | E_list exps ->
+ let evaluated, unevaluated = Util.take_drop is_value exps in
+ begin
+ match unevaluated with
+ | exp :: exps ->
+ step exp >>= fun exp' -> wrap (E_list (evaluated @ exp' :: exps))
+ | [] -> return (exp_of_value (V_list (List.map value_of_exp evaluated)))
+ end
+
(* Special rules for short circuting boolean operators *)
| E_app (id, [x; y]) when (string_of_id id = "and_bool" || string_of_id id = "or_bool") && not (is_value x) ->
step x >>= fun x' -> wrap (E_app (id, [x'; y]))
@@ -273,7 +367,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_let (LB_aux (LB_val (pat, bind), lb_annot), body) when not (is_value bind) ->
step bind >>= fun bind' -> wrap (E_let (LB_aux (LB_val (pat, bind'), lb_annot), body))
| E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
- let matched, bindings = pattern_match pat (value_of_exp bind) in
+ let matched, bindings = pattern_match (Type_check.env_of orig_exp) pat (value_of_exp bind) in
if matched then
return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
else
@@ -323,16 +417,29 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
step exp >>= fun exp' -> wrap (E_case (exp', pexps))
| E_case (_, []) -> failwith "Pattern matching failed"
| E_case (exp, Pat_aux (Pat_exp (pat, body), _) :: pexps) ->
- let matched, bindings = pattern_match pat (value_of_exp exp) in
+ let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
if matched then
return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
else
wrap (E_case (exp, pexps))
+ | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when not (is_value guard) ->
+ let matched, bindings = pattern_match (Type_check.env_of body) pat (value_of_exp exp) in
+ if matched then
+ let guard = List.fold_left (fun guard (id, v) -> subst id v guard) guard (Bindings.bindings bindings) in
+ let body = List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings) in
+ step guard >>= fun guard' ->
+ wrap (E_case (exp, Pat_aux (Pat_when (pat, guard', body), pat_annot) :: pexps))
+ else
+ wrap (E_case (exp, pexps))
+ | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_true guard -> return body
+ | E_case (exp, Pat_aux (Pat_when (pat, guard, body), pat_annot) :: pexps) when is_false guard -> wrap (E_case (exp, pexps))
| E_cast (typ, exp) -> return exp
| E_throw exp when is_value exp -> throw (value_of_exp exp)
| E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp')
+ | E_exit exp when is_value exp -> throw (V_ctor ("Exit", [value_of_exp exp]))
+ | E_exit exp -> step exp >>= fun exp' -> wrap (E_exit exp')
| E_ref id -> return (exp_of_value (V_ref (string_of_id id)))
| E_id id ->
@@ -350,9 +457,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
return exp
| Local (Mutable, _) -> return (exp_of_value (Bindings.find id lstate.locals))
| Local (Immutable, _) ->
- let chain = build_letchain gstate.letbinds orig_exp in
- print_endline "CHAINED";
+ let chain = build_letchain id gstate.letbinds orig_exp in
return chain
+ | Enum _ ->
+ return (exp_of_value (V_ctor (string_of_id id, [])))
| _ -> failwith "id"
end
@@ -388,19 +496,23 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
|> return
end
+ | E_field (exp, id) when not (is_value exp) ->
+ step exp >>= fun exp' -> wrap (E_field (exp', id))
+ | E_field (exp, id) ->
+ let record = coerce_record (value_of_exp exp) in
+ return (exp_of_value (StringMap.find (string_of_id id) record))
+
| E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp'))
| E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp]))
- | E_assign (LEXP_aux (LEXP_field (lexp, id), _), exp) ->
+ | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) ->
let open Type_check in
let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in
- let ul = (Parse_ast.Unknown, None) in
let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in
wrap (E_assign (lexp, exp'))
- | E_assign (LEXP_aux (LEXP_vector (vec, n), _), exp) ->
+ | E_assign (LEXP_aux (LEXP_vector (vec, n), lexp_annot), exp) ->
let open Type_check in
let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
- let ul = (Parse_ast.Unknown, None) in
- let exp' = E_aux (E_vector_update (vec_exp, n, exp), ul) in
+ let exp' = E_aux (E_vector_update (vec_exp, n, exp), lexp_annot) in
wrap (E_assign (vec, exp'))
| E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) ->
begin
@@ -419,7 +531,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
let id = Id_aux (Id (coerce_ref (value_of_exp reference)), Parse_ast.Unknown) in
gets >>= fun (lstate, gstate) ->
puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp
- | E_assign _ -> assert false
+ | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment"
+ (*
+ let values = coerce_tuple (value_of_exp exp) in
+ wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values))
+ *)
+ | E_assign _ -> failwith (string_of_exp orig_exp);
| E_try (exp, pexps) when is_value exp -> return exp
| E_try (exp, pexps) ->
@@ -452,40 +569,51 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
| LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id))
and lexp_assign (LEXP_aux (lexp_aux, _) as lexp) value =
- print_endline ("Assigning: " ^ string_of_lexp lexp ^ " to " ^ string_of_value value |> Util.yellow |> Util.clear);
+ (* print_endline ("Assigning: " ^ string_of_lexp lexp ^ " to " ^ string_of_value value |> Util.yellow |> Util.clear); *)
match lexp_aux with
| LEXP_id id -> Bindings.singleton id value
| _ -> failwith "Unhandled lexp_assign"
-and pattern_match (P_aux (p_aux, _) as pat) value =
- print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear);
+and pattern_match env (P_aux (p_aux, _) as pat) value =
+ (* print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear); *)
match p_aux with
| P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty
| P_wild -> true, Bindings.empty
| P_as (pat, id) ->
- let matched, bindings = pattern_match pat value in
+ let matched, bindings = pattern_match env pat value in
matched, Bindings.add id value bindings
- | P_typ (_, pat) -> pattern_match pat value
- | P_id id -> true, Bindings.singleton id value
- | P_var (pat, _) -> pattern_match pat value
+ | P_typ (_, pat) -> pattern_match env pat value
+ | P_id id ->
+ let open Type_check in
+ begin
+ match Env.lookup_id id env with
+ | Enum _ | Union _ ->
+ if is_ctor value && string_of_id id = fst (coerce_ctor value)
+ then true, Bindings.empty
+ else false, Bindings.empty
+ | _ -> true, Bindings.singleton id value
+ end
+ | P_var (pat, _) -> pattern_match env pat value
| P_app (id, pats) ->
let (ctor, vals) = coerce_ctor value in
if Id.compare id (mk_id ctor) = 0 then
- let matches = List.map2 pattern_match pats vals in
+ let matches = List.map2 (pattern_match env) pats vals in
List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
else
false, Bindings.empty
| P_record _ -> assert false (* TODO *)
- | P_vector _ -> assert false (* TODO *)
+ | P_vector pats ->
+ let matches = List.map2 (pattern_match env) pats (coerce_gv value) in
+ List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
| P_vector_concat _ -> assert false (* TODO *)
| P_tup pats | P_list pats ->
- let matches = List.map2 pattern_match pats (coerce_listlike value) in
+ let matches = List.map2 (pattern_match env) pats (coerce_listlike value) in
List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
| P_cons _ -> assert false (* TODO *)
-let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), _)) value =
+let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) value =
let pexp_of_funcl (FCL_aux (FCL_Funcl (_, pexp), _)) = pexp in
- E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), (Parse_ast.Unknown, None))
+ E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), annot)
let rec get_fundef id (Defs defs) =
match defs with
@@ -500,31 +628,45 @@ let stack_state (_, lstate, _) = lstate
type frame =
| Done of state * value
| Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list
+ | Break of frame
-let rec eval_frame ast = function
+let rec eval_frame' ast = function
| Done (state, v) -> Done (state, v)
+ | Break frame -> Break frame
| Step (out, state, m, stack) ->
match (m, stack) with
| Pure v, [] when is_value v -> Done (state, value_of_exp v)
| Pure v, (head :: stack') when is_value v ->
- print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear);
+ (* print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear); *)
Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack')
| Pure exp', _ ->
let out' = Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp') in
Step (out', state, step exp', stack)
+ | Yield (Call(id, vals, cont)), _ when string_of_id id = "break" ->
+ let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
+ let body = exp_of_fundef (get_fundef id ast) arg in
+ Break (Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack))
| Yield (Call(id, vals, cont)), _ ->
- print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear);
+ (* print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); *)
let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
let body = exp_of_fundef (get_fundef id ast) arg in
Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)
| Yield (Gets cont), _ ->
- eval_frame ast (Step (out, state, cont state, stack))
+ eval_frame' ast (Step (out, state, cont state, stack))
| Yield (Puts (state', cont)), _ ->
- eval_frame ast (Step (out, state', cont (), stack))
+ eval_frame' ast (Step (out, state', cont (), stack))
| Yield (Early_return v), [] -> Done (state, v)
| Yield (Early_return v), (head :: stack') ->
- print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear);
+ (* print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear); *)
Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack')
| Yield (Assertion_failed msg), _ ->
failwith msg
+ | Yield (Exception v), _ ->
+ print_endline ("Uncaught Exception" |> Util.cyan |> Util.clear);
+ Done (state, v)
| _ -> assert false
+
+let eval_frame ast frame =
+ try eval_frame' ast frame with
+ | Type_check.Type_error (l, err) ->
+ raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
diff --git a/src/isail.ml b/src/isail.ml
index 5452b7a9..6b60581b 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -76,7 +76,10 @@ let rec user_input callback =
| None -> ()
| Some v ->
mode_clear ();
- callback v;
+ begin
+ try callback v with
+ | Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
+ end;
user_input callback
let termcode n = "\x1B[" ^ string_of_int n ^ "m"
@@ -86,25 +89,72 @@ let clear str = str ^ termcode 0
let sail_logo =
let banner str = str |> bold |> red |> clear in
- [ " ___ ___ ___ ___ ";
- " /\\ \\ /\\ \\ /\\ \\ /\\__\\";
- " /::\\ \\ /::\\ \\ _\\:\\ \\ /:/ /";
- " /\\:\\:\\__\\ /::\\:\\__\\ /\\/::\\__\\ /:/__/ ";
- " \\:\\:\\/__/ \\/\\::/ / \\::/\\/__/ \\:\\ \\ ";
- " \\::/ / /:/ / \\:\\__\\ \\:\\__\\";
- " \\/__/ \\/__/ \\/__/ \\/__/";
+ [ {| ___ ___ ___ ___ |};
+ {| /\ \ /\ \ /\ \ /\__\|};
+ {| /::\ \ /::\ \ _\:\ \ /:/ /|};
+ {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
+ {| \:\:\/__/ \/\::/ / \::/\/__/ \:\ \ |};
+ {| \::/ / /:/ / \:\__\ \:\__\|};
+ {| \/__/ \/__/ \/__/ \/__/|};
""
]
|> List.map banner
let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)
+let print_program () =
+ match !current_mode with
+ | Normal -> ()
+ | Evaluation (Step (out, _, _, stack)) ->
+ let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in
+ List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep);
+ print_endline out
+ | Evaluation _ -> ()
+
+let interactive_state = ref (initial_state !interactive_ast)
+
+let rec run () =
+ match !current_mode with
+ | Normal -> ()
+ | Evaluation frame ->
+ begin
+ match frame with
+ | Done (state, v) ->
+ interactive_state := state;
+ print_endline ("Result = " ^ Value.string_of_value v);
+ current_mode := Normal
+ | Step (out, state, _, stack) ->
+ current_mode := Evaluation (eval_frame !interactive_ast frame);
+ run ()
+ | Break frame ->
+ print_endline "Breakpoint";
+ current_mode := Evaluation frame
+ end
+
+let rec run_steps n =
+ match !current_mode with
+ | _ when n <= 0 -> ()
+ | Normal -> ()
+ | Evaluation frame ->
+ begin
+ match frame with
+ | Done (state, v) ->
+ interactive_state := state;
+ print_endline ("Result = " ^ Value.string_of_value v);
+ current_mode := Normal
+ | Step (out, state, _, stack) ->
+ current_mode := Evaluation (eval_frame !interactive_ast frame);
+ run_steps (n - 1)
+ | Break frame ->
+ print_endline "Breakpoint";
+ current_mode := Evaluation frame
+ end
+
let handle_input input =
+ LNoise.history_add input |> ignore;
match !current_mode with
| Normal ->
begin
- LNoise.history_add input |> ignore;
-
if input <> "" && input.[0] = ':' then
let n = try String.index input ' ' with Not_found -> String.length input in
let cmd = Str.string_before input n in
@@ -114,37 +164,50 @@ let handle_input input =
let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !interactive_env in
pretty_sail stdout (doc_binding (typq, typ));
print_newline ();
- | ":q" | ":quit" ->
- exit 0
+ | ":elf" ->
+ Elf_loader.load_elf arg
+ | ":q" | ":quit" -> exit 0
| ":i" | ":infer" ->
let exp = Initial_check.exp_of_string dec_ord arg in
let exp = Type_check.infer_exp !interactive_env exp in
pretty_sail stdout (doc_typ (Type_check.typ_of exp));
print_newline ()
| ":v" | ":verbose" ->
- Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 2
+ Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 3;
+ print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug)
| _ -> print_endline ("Unrecognised command " ^ input)
else if input <> "" then
let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in
- current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state !interactive_ast, return exp, [])))
+ current_mode := Evaluation (eval_frame !interactive_ast (Step ("", !interactive_state, return exp, [])));
+ print_program ()
else ()
end
| Evaluation frame ->
begin
- match frame with
- | Done (_, v) ->
- print_endline ("Result = " ^ Value.string_of_value v);
- current_mode := Normal
- | Step (out, _, _, stack) ->
- let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in
- List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep);
- print_endline out;
- current_mode := Evaluation (eval_frame !interactive_ast frame)
+ if input <> "" && input.[0] = ':' then
+ let n = try String.index input ' ' with Not_found -> String.length input in
+ let cmd = Str.string_before input n in
+ let arg = String.trim (Str.string_after input n) in
+ match cmd with
+ | ":r" | ":run" ->
+ run ()
+ | ":s" | ":step" ->
+ run_steps (int_of_string arg)
+ | ":q" | ":quit" -> exit 0
+ | _ -> print_endline ("Unrecognised command " ^ input)
+ else
+ match frame with
+ | Done (state, v) ->
+ interactive_state := state;
+ print_endline ("Result = " ^ Value.string_of_value v);
+ current_mode := Normal
+ | Step (out, state, _, stack) ->
+ interactive_state := state;
+ current_mode := Evaluation (eval_frame !interactive_ast frame);
+ print_program ()
end
-
-
let () =
(* Auto complete function names based on val specs *)
LNoise.set_completion_callback
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index 1babc1c9..ae58f7b2 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -69,8 +69,6 @@ let split ch s =
let lem_dir =
try Sys.getenv "LEM_DIR" (* LEM_DIR must contain an absolute path *)
with Not_found -> "../../../lem" ;;
-let lem_libdir = lem_dir / "ocaml-lib" / "_build_zarith";;
-let lem_lib = lem_libdir / "extract" ;;
let lem = lem_dir / "lem" ;;
(* All -wl ignores should be removed if you want to see the pattern compilation, exhaustive, and unused var warnings *)
@@ -85,9 +83,8 @@ let lem_opts = [A "-lib"; P "../lem_interp";
dispatch begin function
| After_rules ->
(* ocaml_lib "lem_interp/interp"; *)
- ocaml_lib ~extern:true ~dir:lem_libdir ~tag_name:"use_lem" lem_lib;
ocaml_lib ~extern:false ~dir:"pprint/src" ~tag_name:"use_pprint" "pprint/src/PPrintLib";
-
+
rule "lem -> ml"
~prod: "%.ml"
~dep: "%.lem"
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 89220356..55695114 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -647,7 +647,7 @@ let ocaml_main spec =
^//^ (string "Random.self_init ();"
^/^ string "load_elf ();"
^/^ string (if !opt_trace_ocaml then "Sail_lib.opt_trace := true;" else "Sail_lib.opt_trace := false;")
- ^/^ string "initialize_registers ();"
+ ^/^ string "zinitializze_registers ();"
^/^ string "Printexc.record_backtrace true;"
^/^ string "zmain ()")
]
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 2ecaf91d..3b74d38a 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2924,6 +2924,9 @@ let rewrite_defs_ocaml = [
]
let rewrite_defs_interpreter = [
+ ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+ ("tuple_assignments", rewrite_tuple_assignments);
+ ("remove_vector_concat", rewrite_defs_remove_vector_concat);
("constraint", rewrite_constraint);
("trivial_sizeof", rewrite_trivial_sizeof);
("sizeof", rewrite_sizeof);
diff --git a/src/sail.ml b/src/sail.ml
index 974885c6..eee80045 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -60,7 +60,6 @@ let opt_print_lem_ast = ref false
let opt_print_lem = ref false
let opt_print_sil = ref false
let opt_print_ocaml = ref false
-let opt_convert = ref false
let opt_memo_z3 = ref false
let opt_sanity = ref false
let opt_libs_lem = ref ([]:string list)
@@ -118,9 +117,6 @@ let options = Arg.align ([
( "-no_effects",
Arg.Set Type_check.opt_no_effects,
" (experimental) turn off effect checking");
- ( "-convert",
- Arg.Set opt_convert,
- " (experimental) convert sail to new syntax for use with -new_parser");
( "-just_check",
Arg.Set opt_just_check,
" (experimental) terminate immediately after typechecking");
@@ -185,10 +181,6 @@ let main() =
-> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
let ast = convert_ast Ast_util.inc_ord ast in
- if !opt_convert
- then (Pretty_print_sail.pp_defs stdout ast; exit 0)
- else ();
-
let (ast, type_envs) = check_ast ast in
let (ast, type_envs) =
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index b4dffba9..72974b9a 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -87,10 +87,10 @@ let undefined_bit () =
let undefined_bool () =
if !random then Random.bool () else false
-let rec undefined_vector (start_index, len, item) =
+let rec undefined_vector (len, item) =
if Big_int.equal len Big_int.zero
then []
- else item :: undefined_vector (start_index, Big_int.sub len (Big_int.of_int 1), item)
+ else item :: undefined_vector (Big_int.sub len (Big_int.of_int 1), item)
let undefined_string () = ""
diff --git a/src/type_check.ml b/src/type_check.ml
index 3269de1d..b77d800e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -76,7 +76,7 @@ type type_error =
(* First parameter is the error that caused us to start doing type
coercions, the second is the errors encountered by all possible
coercions *)
- | Err_no_casts of type_error * type_error list
+ | Err_no_casts of unit exp * type_error * type_error list
| Err_no_overloading of id * (id * type_error) list
| Err_unresolved_quants of id * quant_item list
| Err_subtype of typ * typ * n_constraint list
@@ -86,11 +86,13 @@ type type_error =
let pp_type_error err =
let open PPrint in
let rec pp_err = function
- | Err_no_casts (trigger, []) ->
- (string "Tried performing type coercion because" ^//^ pp_err trigger)
- ^/^ string "No possible coercions"
- | Err_no_casts (trigger, errs) ->
- (string "Tried performing type coerction because" ^//^ pp_err trigger)
+ | Err_no_casts (exp, trigger, []) ->
+ (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp)
+ ^/^ (string "Failed because" ^//^ pp_err trigger)
+ ^/^ string "There were no possible casts"
+ | Err_no_casts (exp, trigger, errs) ->
+ (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp)
+ ^/^ string "Failed because" ^//^ pp_err trigger
| Err_no_overloading (id, errs) ->
string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^
group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^^ space ^^ pp_err err) errs)
@@ -2173,7 +2175,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
| _ -> failwith "Cannot switch type for unannotated function"
in
let rec try_casts trigger errs = function
- | [] -> typ_raise l (Err_no_casts (trigger, errs))
+ | [] -> typ_raise l (Err_no_casts (strip_exp annotated_exp, trigger, errs))
| (cast :: casts) -> begin
typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ);
try
diff --git a/src/type_check.mli b/src/type_check.mli
index 33615e43..b43cab6b 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -56,7 +56,7 @@ val opt_tc_debug : int ref
val opt_no_effects : bool ref
type type_error =
- | Err_no_casts of type_error * type_error list
+ | Err_no_casts of unit exp * type_error * type_error list
| Err_no_overloading of id * (id * type_error) list
| Err_unresolved_quants of id * quant_item list
| Err_subtype of typ * typ * n_constraint list
diff --git a/src/value.ml b/src/value.ml
index d9690899..2ddeecae 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -186,6 +186,10 @@ let value_append = function
| [v1; v2] -> V_vector (coerce_gv v1 @ coerce_gv v2)
| _ -> failwith "value append"
+let value_slice = function
+ | [v1; v2; v3] -> V_vector (Sail_lib.slice (coerce_gv v1, coerce_int v2, coerce_int v3))
+ | _ -> failwith "value slice"
+
let value_not = function
| [v] -> V_bool (not (coerce_bool v))
| _ -> failwith "value not"
@@ -214,6 +218,21 @@ let value_get_slice_int = function
| [v1; v2; v3] -> mk_vector (Sail_lib.get_slice_int (coerce_int v1, coerce_int v2, coerce_int v3))
| _ -> failwith "value get_slice_int"
+let value_set_slice_int = function
+ | [v1; v2; v3; v4] ->
+ V_int (Sail_lib.set_slice_int (coerce_int v1, coerce_int v2, coerce_int v3, coerce_bv v4))
+ | _ -> failwith "value set_slice_int"
+
+let value_set_slice = function
+ | [v1; v2; v3; v4; v5] ->
+ mk_vector (Sail_lib.set_slice (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_int v4, coerce_bv v5))
+ | _ -> failwith "value set_slice"
+
+let value_hex_slice = function
+ | [v1; v2; v3] ->
+ mk_vector (Sail_lib.hex_slice (coerce_string v1, coerce_int v2, coerce_int v3))
+ | _ -> failwith "value hex_slice"
+
let value_add = function
| [v1; v2] -> V_int (Sail_lib.add (coerce_int v1, coerce_int v2))
| _ -> failwith "value add"
@@ -222,6 +241,46 @@ let value_sub = function
| [v1; v2] -> V_int (Sail_lib.sub (coerce_int v1, coerce_int v2))
| _ -> failwith "value sub"
+let value_mult = function
+ | [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value mult"
+
+let value_quotient = function
+ | [v1; v2] -> V_int (Sail_lib.quotient (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value quotient"
+
+let value_modulus = function
+ | [v1; v2] -> V_int (Sail_lib.modulus (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value modulus"
+
+let value_add_vec_int = function
+ | [v1; v2] -> mk_vector (Sail_lib.add_vec_int (coerce_bv v1, coerce_int v2))
+ | _ -> failwith "value add_vec_int"
+
+let value_add_vec = function
+ | [v1; v2] -> mk_vector (Sail_lib.add_vec (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value add_vec"
+
+let value_sub_vec = function
+ | [v1; v2] -> mk_vector (Sail_lib.sub_vec (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value sub_vec"
+
+let value_shl_int = function
+ | [v1; v2] -> V_int (Sail_lib.shl_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value shl_int"
+
+let value_shr_int = function
+ | [v1; v2] -> V_int (Sail_lib.shr_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value shr_int"
+
+let value_max_int = function
+ | [v1; v2] -> V_int (Sail_lib.max_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value max_int"
+
+let value_min_int = function
+ | [v1; v2] -> V_int (Sail_lib.min_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value min_int"
+
let value_replicate_bits = function
| [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2))
| _ -> failwith "value replicate_bits"
@@ -230,6 +289,11 @@ let is_bit = function
| V_bit _ -> true
| _ -> false
+
+let is_ctor = function
+ | V_ctor _ -> true
+ | _ -> false
+
let rec string_of_value = function
| V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
| V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]"
@@ -257,10 +321,28 @@ let value_print = function
| [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit
| _ -> assert false
+let value_internal_pick = function
+ | [v1] -> List.hd (coerce_listlike v1);
+ | _ -> failwith "value internal_pick"
+
let value_undefined_vector = function
- | [v1; v2; v3] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, coerce_int v2, v3))
+ | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2))
| _ -> failwith "value undefined_vector"
+let value_read_ram = function
+ | [v1; v2; v3; v4] -> mk_vector (Sail_lib.read_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4))
+ | _ -> failwith "value read_ram"
+
+let value_write_ram = function
+ | [v1; v2; v3; v4; v5] ->
+ Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5);
+ V_unit
+ | _ -> failwith "value write_ram"
+
+let value_putchar = function
+ | [v] -> Sail_lib.putchar (coerce_int v); V_unit
+ | _ -> failwith "value putchar"
+
let primops =
List.fold_left
(fun r (x, y) -> StringMap.add x y r)
@@ -269,6 +351,7 @@ let primops =
("or_bool", or_bool);
("print_endline", value_print);
("prerr_endline", value_print);
+ ("putchar", value_putchar);
("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
("print_bits", fun [msg; bits] -> print_endline (coerce_string msg ^ string_of_value bits); V_unit);
("eq_int", value_eq_int);
@@ -284,6 +367,7 @@ let primops =
("access", value_access);
("update", value_update);
("update_subrange", value_update_subrange);
+ ("slice", value_slice);
("append", value_append);
("not", value_not);
("not_vec", value_not_vec);
@@ -292,10 +376,28 @@ let primops =
("uint", value_uint);
("sint", value_sint);
("get_slice_int", value_get_slice_int);
+ ("set_slice_int", value_set_slice_int);
+ ("set_slice", value_set_slice);
+ ("hex_slice", value_hex_slice);
("add", value_add);
("sub", value_sub);
+ ("mult", value_mult);
+ ("quotient", value_quotient);
+ ("modulus", value_modulus);
+ ("shr_int", value_shr_int);
+ ("shl_int", value_shl_int);
+ ("max_int", value_max_int);
+ ("min_int", value_min_int);
+ ("add_vec_int", value_add_vec_int);
+ ("add_vec", value_add_vec);
+ ("sub_vec", value_sub_vec);
+ ("read_ram", value_read_ram);
+ ("write_ram", value_write_ram);
("undefined_bit", fun _ -> V_bit Sail_lib.B0);
+ ("undefined_int", fun _ -> V_int Big_int.zero);
+ ("undefined_bool", fun _ -> V_bool false);
("undefined_vector", value_undefined_vector);
+ ("internal_pick", value_internal_pick);
("replicate_bits", value_replicate_bits);
("Elf_loader.elf_entry", fun _ -> V_int (Big_int.of_int 0));
]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 14:18:50 +0000