summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml4
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/initial_check.ml2
-rw-r--r--src/interpreter.ml233
-rw-r--r--src/isail.ml46
-rw-r--r--src/lexer2.mll3
-rw-r--r--src/parse_ast.ml1
-rw-r--r--src/parser2.mly17
-rw-r--r--src/pretty_print_lem.ml16
-rw-r--r--src/pretty_print_sail2.ml5
-rw-r--r--src/process_file.ml2
-rw-r--r--src/rewrites.ml15
-rw-r--r--src/type_check.ml143
-rw-r--r--src/type_check.mli5
-rw-r--r--src/util.ml1
-rw-r--r--src/util.mli1
-rw-r--r--src/value.ml204
17 files changed, 451 insertions, 249 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 7e3e0da7..4407b7f1 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -238,6 +238,8 @@ let unit_typ = mk_id_typ (mk_id "unit")
let bit_typ = mk_id_typ (mk_id "bit")
let real_typ = mk_id_typ (mk_id "real")
let app_typ id args = mk_typ (Typ_app (id, args))
+let ref_typ typ = mk_typ (Typ_app (mk_id "ref", [mk_typ_arg (Typ_arg_typ typ)]))
+let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (Typ_arg_typ typ)]))
let atom_typ nexp =
mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))]))
let range_typ nexp1 nexp2 =
@@ -338,6 +340,7 @@ and map_exp_annot_aux f = function
| E_block xs -> E_block (List.map (map_exp_annot f) xs)
| E_nondet xs -> E_nondet (List.map (map_exp_annot f) xs)
| E_id id -> E_id id
+ | E_ref id -> E_ref id
| E_lit lit -> E_lit lit
| E_cast (typ, exp) -> E_cast (typ, map_exp_annot f exp)
| E_app (id, xs) -> E_app (id, List.map (map_exp_annot f) xs)
@@ -582,6 +585,7 @@ let rec string_of_exp (E_aux (exp, _)) =
match exp with
| E_block exps -> "{ " ^ string_of_list "; " string_of_exp exps ^ " }"
| E_id v -> string_of_id v
+ | E_ref id -> "ref " ^ string_of_id id
| E_sizeof nexp -> "sizeof " ^ string_of_nexp nexp
| E_constraint nc -> "constraint(" ^ string_of_n_constraint nc ^ ")"
| E_lit lit -> string_of_lit lit
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 7ff46b02..a4ad92fb 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -103,6 +103,8 @@ val range_typ : nexp -> nexp -> typ
val bit_typ : typ
val bool_typ : typ
val app_typ : id -> typ_arg list -> typ
+val ref_typ : typ -> typ
+val register_typ : typ -> typ
val unit_typ : typ
val string_typ : typ
val real_typ : typ
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4fde87cd..0915bc38 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -472,6 +472,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
| None -> E_block(List.map (to_ast_exp k_env def_ord) exps))
| Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env def_ord) exps)
| Parse_ast.E_id(id) -> E_id(to_ast_id id)
+ | Parse_ast.E_ref(id) -> E_ref(to_ast_id id)
| Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit)
| Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env def_ord typ, to_ast_exp k_env def_ord exp)
| Parse_ast.E_app(f,args) ->
@@ -945,6 +946,7 @@ let initial_kind_env =
("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})});
("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
+ ("ref", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) });
("vector", {k = K_Lam( [{k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } );
("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})});
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 3356b9dc..4fd75094 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -51,9 +51,22 @@
open Ast
open Ast_util
open Value
-(* open Type_check *)
-type state = St
+type gstate =
+ { registers : value Bindings.t }
+
+type lstate =
+ { locals : value Bindings.t }
+
+type state = lstate * gstate
+
+let initial_gstate =
+ { registers = Bindings.empty }
+
+let initial_lstate =
+ { locals = Bindings.empty }
+
+let initial_state = initial_lstate, initial_gstate
let value_of_lit (L_aux (l_aux, _)) =
match l_aux with
@@ -63,6 +76,7 @@ let value_of_lit (L_aux (l_aux, _)) =
| L_true -> V_bool true
| L_false -> V_bool false
| L_string str -> V_string str
+ | L_num n -> V_int n
| _ -> failwith "Unimplemented value_of_lit" (* TODO *)
let is_value = function
@@ -87,23 +101,23 @@ let value_of_exp = function
(**************************************************************************)
type 'a response =
- | Final of value
+ | Early_return of value
| Exception of value
| Assertion_failed of string
| Call of id * value list * (value -> 'a)
| Gets of (state -> 'a)
- | Puts of state * 'a
+ | Puts of state * (unit -> 'a)
and 'a monad =
| Pure of 'a
| Yield of ('a monad response)
let map_response f = function
- | Final v -> Final v
+ | Early_return v -> Early_return v
| Exception v -> Exception v
| Assertion_failed str -> Assertion_failed str
| Gets g -> Gets (fun s -> f (g s))
- | Puts (s, x) -> Puts (s, f x)
+ | Puts (s, cont) -> Puts (s, fun () -> f (cont ()))
| Call (id, vals, cont) -> Call (id, vals, fun v -> f (cont v))
let rec liftM f = function
@@ -142,9 +156,9 @@ let gets : state monad =
Yield (Gets (fun s -> Pure s))
let puts (s : state) : unit monad =
- Yield (Puts (s, Pure ()))
+ Yield (Puts (s, fun () -> Pure ()))
-let final v = Yield (Final v)
+let early_return v = Yield (Early_return v)
let assertion_failed msg = Yield (Assertion_failed msg)
@@ -156,9 +170,22 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
| E_block exps -> E_block (List.map (subst id value) exps)
| E_nondet exps -> E_nondet (List.map (subst id value) exps)
| 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)
- | _ -> assert false (* TODO *)
+ | 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 (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_vector exps -> E_vector (List.map (subst id value) exps)
+ | E_return exp -> E_return (subst id value exp)
+ | 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
@@ -167,7 +194,12 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
(* 2. Expression Evaluation *)
(**************************************************************************)
-let rec step (E_aux (e_aux, annot)) =
+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 step (E_aux (e_aux, annot) as orig_exp) =
let wrap e_aux' = return (E_aux (e_aux', annot)) in
match e_aux with
| E_block [] -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown)))
@@ -183,11 +215,38 @@ let rec step (E_aux (e_aux, annot)) =
| E_if (exp, then_exp, else_exp) ->
step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp))
- | E_assert (exp, msg) when is_true exp -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown)))
+ | 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) ->
step exp >>= fun exp' -> wrap (E_assert (exp', msg))
+ | E_vector exps ->
+ let evaluated, unevaluated = Util.take_drop is_value exps in
+ begin
+ match unevaluated with
+ | exp :: exps ->
+ step exp >>= fun exp' -> wrap (E_vector (evaluated @ exp' :: exps))
+ | [] -> return (exp_of_value (V_vector (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]))
+ | E_app (id, [x; y]) when string_of_id id = "and_bool" && is_false x ->
+ return (exp_of_value (V_bool false))
+ | E_app (id, [x; y]) when string_of_id id = "or_bool" && is_true x ->
+ return (exp_of_value (V_bool true))
+
+ | 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
+ if matched then
+ return (List.fold_left (fun body (id, v) -> subst id v body) body (Bindings.bindings bindings))
+ else
+ failwith "Match failure"
+
+ (* otherwise left-to-right evaluation order for function applications *)
| E_app (id, exps) ->
let evaluated, unevaluated = Util.take_drop is_value exps in
begin
@@ -199,7 +258,8 @@ let rec step (E_aux (e_aux, annot)) =
return (exp_of_value (V_ctor (string_of_id id, List.map value_of_exp evaluated)))
| [] when Env.is_extern id (env_of_annot annot) "interpreter" ->
begin
- let primop = StringMap.find (Env.get_extern id (env_of_annot annot) "interpreter") primops in
+ let extern = Env.get_extern id (env_of_annot annot) "interpreter" in
+ let primop = try StringMap.find extern primops with Not_found -> failwith ("No primop " ^ extern) in
return (exp_of_value (primop (List.map value_of_exp evaluated)))
end
| [] -> liftM exp_of_value (call id (List.map value_of_exp evaluated))
@@ -211,7 +271,7 @@ let rec step (E_aux (e_aux, annot)) =
| E_app_infix (x, id, y) ->
step x >>= fun x' -> wrap (E_app_infix (x', id, y))
- | E_return exp when is_value exp -> final (value_of_exp exp)
+ | E_return exp when is_value exp -> early_return (value_of_exp exp)
| E_return exp -> step exp >>= fun exp' -> wrap (E_return exp')
| E_tuple exps ->
@@ -238,6 +298,76 @@ let rec step (E_aux (e_aux, annot)) =
| E_throw exp when is_value exp -> throw (value_of_exp exp)
| E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp')
+ | E_id id ->
+ begin
+ let open Type_check in
+ gets >>= fun (lstate, gstate) ->
+ match Env.lookup_id id (env_of_annot annot) with
+ | Register _ ->
+ let exp =
+ try exp_of_value (Bindings.find id gstate.registers) with
+ | Not_found ->
+ let exp = mk_exp (E_app (mk_id ("undefined_" ^ string_of_typ (typ_of orig_exp)), [mk_exp (E_lit (mk_lit (L_unit)))])) in
+ Type_check.check_exp (env_of_annot annot) exp (typ_of orig_exp)
+ in
+ return exp
+ | Local (Mutable, _) -> return (exp_of_value (Bindings.find id lstate.locals))
+ | _ -> failwith "id"
+ end
+
+ | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) ->
+ let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in
+ begin
+ match unevaluated with
+ | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps ->
+ step exp >>= fun exp' ->
+ wrap (E_record (FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot)))
+ | [] ->
+ List.map value_of_fexp fexps
+ |> List.fold_left (fun record (field, v) -> StringMap.add field v record) StringMap.empty
+ |> (fun record -> V_record record)
+ |> exp_of_value
+ |> return
+ end
+
+ | E_record_update (exp, fexps) when not (is_value exp) ->
+ step exp >>= fun exp' -> wrap (E_record_update (exp', fexps))
+ | E_record_update (record, FES_aux (FES_Fexps (fexps, flag), fes_annot)) ->
+ let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in
+ begin
+ match unevaluated with
+ | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps ->
+ step exp >>= fun exp' ->
+ wrap (E_record_update (record, FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot)))
+ | [] ->
+ List.map value_of_fexp fexps
+ |> List.fold_left (fun record (field, v) -> StringMap.add field v record) (coerce_record (value_of_exp record))
+ |> (fun record -> V_record record)
+ |> exp_of_value
+ |> return
+ end
+
+ | 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) ->
+ 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_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) ->
+ begin
+ let open Type_check in
+ gets >>= fun (lstate, gstate) ->
+ match Env.lookup_id id (env_of_annot annot) with
+ | Register _ ->
+ puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp
+ | Local (Mutable, _) | Unbound ->
+ puts ({ lstate with locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp
+ | _ -> failwith "Assign"
+ end
+ | E_assign _ -> assert false
+
| E_try (exp, pexps) when is_value exp -> return exp
| E_try (exp, pexps) ->
begin
@@ -249,7 +379,7 @@ let rec step (E_aux (e_aux, annot)) =
| E_sizeof _ | E_constraint _ -> assert false (* Must be re-written before interpreting *)
- | _ -> assert false (* TODO *)
+ | _ -> failwith ("Unimplemented " ^ string_of_exp orig_exp)
and combine _ v1 v2 =
match (v1, v2) with
@@ -258,6 +388,22 @@ and combine _ v1 v2 =
| None, Some v2 -> Some v2
| Some v1, Some v2 -> failwith "Pattern binds same identifier twice!"
+and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
+ match lexp_aux with
+ | LEXP_id id -> mk_exp (E_id id)
+ | LEXP_memory (f, args) -> mk_exp (E_app (f, args))
+ | LEXP_cast (typ, id) -> mk_exp (E_cast (typ, mk_exp (E_id id)))
+ | LEXP_tup lexps -> mk_exp (E_tuple (List.map exp_of_lexp lexps))
+ | LEXP_vector (lexp, exp) -> mk_exp (E_vector_access (exp_of_lexp lexp, exp))
+ | LEXP_vector_range (lexp, exp1, exp2) -> mk_exp (E_vector_subrange (exp_of_lexp lexp, exp1, exp2))
+ | 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);
+ 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);
match p_aux with
@@ -294,27 +440,38 @@ let rec get_fundef id (Defs defs) =
| (DEF_fundef fdef) :: _ when Id.compare id (id_of_fundef fdef) = 0 -> fdef
| _ :: defs -> get_fundef id (Defs defs)
-let rec untilM p f x =
- if p x then
- return x
- else
- f (return x) >>= fun x' -> untilM p f x'
-
-type trace =
- | Done of value
- | Step of (Type_check.tannot exp) monad * (value -> (Type_check.tannot exp) monad) list
-
-let rec eval_exp ast m =
- match m with
- | Pure v when is_value v -> Done (value_of_exp v)
- | Pure exp' ->
- Pretty_print_sail2.pretty_sail stdout (Pretty_print_sail2.doc_exp exp');
- print_newline ();
- Step (step exp', [])
- | Yield (Call (id, vals, cont)) ->
- 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 (return body, [cont])
- | _ -> assert false
-
+let stack_cont (_, _, cont) = cont
+let stack_string (str, _, _) = str
+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
+
+let rec eval_frame ast = function
+ | Done (state, v) -> Done (state, v)
+ | 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);
+ Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack')
+ | Pure exp', _ ->
+ let out' = Pretty_print_sail2.to_string (Pretty_print_sail2.doc_exp exp') in
+ Step (out', state, step exp', stack)
+ | Yield (Call(id, vals, cont)), _ ->
+ 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))
+ | Yield (Puts (state', cont)), _ ->
+ 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);
+ Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack')
+ | Yield (Assertion_failed msg), _ ->
+ failwith msg
+ | _ -> assert false
diff --git a/src/isail.ml b/src/isail.ml
index 97b92809..88835b8a 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -56,7 +56,7 @@ open Interpreter
open Pretty_print_sail2
type mode =
- | Evaluation of trace
+ | Evaluation of frame
| Normal
let current_mode = ref Normal
@@ -86,14 +86,14 @@ let clear str = str ^ termcode 0
let sail_logo =
let banner str = str |> bold |> red |> clear in
- [ {| ___ ___ ___ ___ |};
- {| /\ \ /\ \ /\ \ /\__\ |};
- {| /::\ \ /::\ \ _\:\ \ /:/ / |};
- {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
- {| \:\:\/__/ \/\::/ / \::/\/__/ \:\ \ |};
- {| \::/ / /:/ / \:\__\ \:\__\ |};
- {| \/__/ \/__/ \/__/ \/__/ |};
- {| |}
+ [ " ___ ___ ___ ___ ";
+ " /\\ \\ /\\ \\ /\\ \\ /\\__\\";
+ " /::\\ \\ /::\\ \\ _\\:\\ \\ /:/ /";
+ " /\\:\\:\\__\\ /::\\:\\__\\ /\\/::\\__\\ /:/__/ ";
+ " \\:\\:\\/__/ \\/\\::/ / \\::/\\/__/ \\:\\ \\ ";
+ " \\::/ / /:/ / \\:\\__\\ \\:\\__\\";
+ " \\/__/ \\/__/ \\/__/ \\/__/";
+ ""
]
|> List.map banner
@@ -127,31 +127,27 @@ let handle_input input =
| _ -> 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_exp !interactive_ast (return exp))
+ current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state, return exp, [])))
else ()
end
- | Evaluation trace ->
+ | Evaluation frame ->
begin
- match trace with
- | Done v ->
+ match frame with
+ | Done (_, v) ->
print_endline ("Result = " ^ Value.string_of_value v);
current_mode := Normal
- | Step (exp, stack) ->
- let next = match eval_exp !interactive_ast exp with
- | Step (exp', stack') -> Evaluation (Step (exp', stack' @ stack))
- | Done v when stack = [] ->
- print_endline ("Result = " ^ Value.string_of_value v);
- Normal
- | Done v ->
- print_endline ("Returning: " ^ Value.string_of_value v |> Util.cyan |> Util.clear);
- Evaluation (Step (List.hd stack v, List.tl stack))
- in
- current_mode := next
+ | 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)
end
let () =
+ List.iter print_endline sail_logo;
+
(* Auto complete function names based on val specs *)
LNoise.set_completion_callback
begin
@@ -177,5 +173,5 @@ let () =
LNoise.history_set ~max_length:100 |> ignore;
if !opt_interactive then
- (List.iter print_endline sail_logo; user_input handle_input)
+ user_input handle_input
else ()
diff --git a/src/lexer2.mll b/src/lexer2.mll
index e2361a04..b293046f 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -130,6 +130,7 @@ let kw_table =
("inc", (fun _ -> Inc));
("let", (fun x -> Let_));
("var", (fun _ -> Var));
+ ("ref", (fun _ -> Ref));
("record", (fun _ -> Record));
("Int", (fun x -> Int));
("Order", (fun x -> Order));
@@ -171,6 +172,8 @@ let kw_table =
("escape", (fun x -> Escape));
]
+
+
}
let ws = [' ''\t']+
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index df4c2d2c..83b116a2 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -267,6 +267,7 @@ exp_aux = (* Expression *)
E_block of (exp) list (* block (parsing conflict with structs?) *)
| E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *)
| E_id of id (* identifier *)
+ | E_ref of id
| E_lit of lit (* literal constant *)
| E_cast of atyp * exp (* cast *)
| E_app of id * (exp) list (* function application *)
diff --git a/src/parser2.mly b/src/parser2.mly
index 74812d1e..ebe829c2 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -69,6 +69,10 @@ let string_of_id = function
| Id_aux (Id str, _) -> str
| Id_aux (DeIid str, _) -> str
+let prepend_id str1 = function
+ | Id_aux (Id str2, loc) -> Id_aux (Id (str1 ^ str2), loc)
+ | _ -> assert false
+
let mk_id i n m = Id_aux (i, loc n m)
let mk_kid str n m = Kid_aux (Var str, loc n m)
@@ -152,7 +156,7 @@ let rec desugar_rchain chain s e =
%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
%token Undefined Union With Val Constraint Throw Try Catch Exit
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
-%token Repeat Until While Do Record Mutual Var
+%token Repeat Until While Do Record Mutual Var Ref
%nonassoc Then
%nonassoc Else
@@ -513,8 +517,11 @@ atomic_typ:
| id Lparen typ_list Rparen
{ mk_typ (ATyp_app ($1, $3)) $startpos $endpos }
| Register Lparen typ Rparen
- { let register_id = mk_id (Id "register") $startpos $endpos in
+ { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in
mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos }
+ | Ref Lparen typ Rparen
+ { let ref_id = mk_id (Id "ref") $startpos($1) $endpos($1) in
+ mk_typ (ATyp_app (ref_id, [$3])) $startpos $endpos }
| Lparen typ Rparen
{ $2 }
| Lparen typ Comma typ_list Rparen
@@ -953,12 +960,18 @@ atomic_exp:
{ mk_exp (E_cast ($3, $1)) $startpos $endpos }
| lit
{ mk_exp (E_lit $1) $startpos $endpos }
+ | id MinusGt id Lparen exp_list Rparen
+ { mk_exp (E_app (prepend_id "_mod_" $3, mk_exp (E_ref $1) $startpos($1) $endpos($1) :: $5)) $startpos $endpos }
+ | atomic_exp Dot id Lparen exp_list Rparen
+ { mk_exp (E_app (prepend_id "_mod_" $3, $1 :: $5)) $startpos $endpos }
| atomic_exp Dot id
{ mk_exp (E_field ($1, $3)) $startpos $endpos }
| id
{ mk_exp (E_id $1) $startpos $endpos }
| kid
{ mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos }
+ | Ref id
+ { mk_exp (E_ref $2) $startpos $endpos }
| id Unit
{ mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
| id Lparen exp_list Rparen
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 3827376f..8f789c14 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -152,7 +152,6 @@ let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs
let is_regtyp (Typ_aux (typ, _)) env = match typ with
| Typ_app(id, _) when string_of_id id = "register" -> true
- | Typ_id(id) when Env.is_regtyp id env -> true
| _ -> false
let doc_nexp_lem nexp =
@@ -720,18 +719,6 @@ let doc_exp_lem, doc_let_lem =
| E_field((E_aux(_,(l,fannot)) as fexp),id) ->
let ft = typ_of_annot (l,fannot) in
(match fannot with
- | Some(env, (Typ_aux (Typ_id tid, _)), _)
- | Some(env, (Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]), _)), _)
- when Env.is_regtyp tid env ->
- let t = (* Env.base_typ_of (env_of full_exp) *) (typ_of full_exp) in
- let eff = effect_of full_exp in
- let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in
- let (ta,aexp_needed) =
- if typ_needs_printed t
- then (doc_tannot_lem sequential mwords (effectful eff) t, true)
- else (empty, aexp_needed) in
- let epp = field_f ^^ space ^^ (expY fexp) in
- if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
| Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env ->
let fname =
if prefix_recordtype
@@ -1336,9 +1323,6 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
else
let env = env_of_annot annot in
(match typ with
- | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env ->
- separate space [string "let";doc_id_lem id;equals;
- string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
| _ ->
let rt = Env.base_typ_of env typ in
if is_vector_typ rt then
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index 0f1ee016..22b6e9ee 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -531,3 +531,8 @@ let doc_defs (Defs(defs)) =
let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d)
let pretty_sail f doc = ToChannel.pretty 1. 120 f doc
+
+let to_string doc =
+ let b = Buffer.create 120 in
+ ToBuffer.pretty 1. 120 b doc;
+ Buffer.contents b
diff --git a/src/process_file.ml b/src/process_file.ml
index 68e5786e..d57127a4 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -121,7 +121,7 @@ let opt_dno_cast = ref false
let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t =
let ienv = if !opt_dno_cast then Type_check.Env.no_casts Type_check.initial_env else Type_check.initial_env in
let ast, env = Type_check.check ienv defs in
- let () = if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else () in
+ let () = if !opt_ddump_tc_ast then Pretty_print_sail2.pp_defs stdout ast else () in
let () = if !opt_just_check then exit 0 else () in
(ast, env)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 25953776..a28352f5 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1389,21 +1389,6 @@ let rec rewrite_lexp_to_rhs (do_rewrite : tannot lexp -> bool) ((LEXP_aux(lexp,(
let (LEXP_aux (_, lannot)) = lexp in
let env = env_of_annot lannot in
match Env.expand_synonyms env (typ_of_annot lannot) with
- | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp_id, _)), _)]), _)
- | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env ->
- let base, top, ranges = Env.get_regtyp regtyp_id env in
- let range, _ =
- try List.find (fun (_, fid) -> Id.compare fid id = 0) ranges with
- | Not_found ->
- raise (Reporting_basic.err_typ l ("Field " ^ string_of_id id ^ " doesn't exist for register type " ^ string_of_id regtyp_id))
- in
- let lexp_exp = E_aux (E_app (mk_id ("cast_" ^ string_of_id regtyp_id), [lexp_to_exp lexp]), (l, None)) in
- let n, m = match range with
- | BF_aux (BF_single n, _) -> n, n
- | BF_aux (BF_range (n, m), _) -> n, m
- | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) in
- let rhs' exp = rhs (E_aux (E_vector_update_subrange (lexp_exp, simple_num l n, simple_num l m, exp), lannot)) in
- (lhs, rhs')
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
(lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot))))
diff --git a/src/type_check.ml b/src/type_check.ml
index c2467cee..907c23a5 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -307,9 +307,6 @@ module Env : sig
val is_register : id -> t -> bool
val get_register : id -> t -> typ
val add_register : id -> typ -> t -> t
- val add_regtyp : id -> Big_int.num -> Big_int.num -> (index_range * id) list -> t -> t
- val is_regtyp : id -> t -> bool
- val get_regtyp : id -> t -> Big_int.num * Big_int.num * (index_range * id) list
val is_mutable : id -> t -> bool
val get_constraints : t -> n_constraint list
val add_constraint : n_constraint -> t -> t
@@ -364,7 +361,6 @@ end = struct
locals : (mut * typ) Bindings.t;
union_ids : (typquant * typ) Bindings.t;
registers : typ Bindings.t;
- regtyps : (Big_int.num * Big_int.num * (index_range * id) list) Bindings.t;
variants : (typquant * type_union list) Bindings.t;
typ_vars : base_kind_aux KBindings.t;
typ_synonyms : (t -> typ_arg list -> typ) Bindings.t;
@@ -390,7 +386,6 @@ end = struct
locals = Bindings.empty;
union_ids = Bindings.empty;
registers = Bindings.empty;
- regtyps = Bindings.empty;
variants = Bindings.empty;
typ_vars = KBindings.empty;
typ_synonyms = Bindings.empty;
@@ -430,6 +425,7 @@ end = struct
("atom", [BK_nat]);
("vector", [BK_nat; BK_order; BK_type]);
("register", [BK_type]);
+ ("ref", [BK_type]);
("bit", []);
("unit", []);
("int", []);
@@ -445,7 +441,6 @@ end = struct
Bindings.mem id env.typ_synonyms
|| Bindings.mem id env.variants
|| Bindings.mem id env.records
- || Bindings.mem id env.regtyps
|| Bindings.mem id env.enums
|| Bindings.mem id builtin_typs
@@ -476,7 +471,7 @@ end = struct
fst (Bindings.find id env.variants)
else if Bindings.mem id env.records then
fst (Bindings.find id env.records)
- else if Bindings.mem id env.enums || Bindings.mem id env.regtyps then
+ else if Bindings.mem id env.enums then
mk_typquant []
else if Bindings.mem id env.typ_synonyms then
typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id)
@@ -708,7 +703,7 @@ end = struct
| Mutable -> true
| Immutable -> false
with
- | Not_found -> typ_error (id_loc id) ("No local binding found for " ^ string_of_id id)
+ | Not_found -> false
let string_of_mtyp (mut, typ) = match mut with
| Immutable -> string_of_typ typ
@@ -768,29 +763,6 @@ end = struct
let get_casts env = env.casts
- let check_index_range cmp f t (BF_aux (ir, l)) =
- match ir with
- | BF_single n ->
- if cmp f n && cmp n t
- then n
- else typ_error l ("Badly ordered index range: " ^ string_of_list ", " Big_int.to_string [f; n; t])
- | BF_range (n1, n2) ->
- if cmp f n1 && cmp n1 n2 && cmp n2 t
- then n2
- else typ_error l ("Badly ordered index range: " ^ string_of_list ", " Big_int.to_string [f; n1; n2; t])
- | BF_concat _ -> typ_error l "Index range concatenation currently unsupported"
-
- let rec check_index_ranges ids cmp base top = function
- | [] -> ()
- | ((range, id) :: ranges) ->
- if IdSet.mem id ids
- then typ_error (id_loc id) ("Duplicate id " ^ string_of_id id ^ " in register typedef")
- else
- begin
- let base' = check_index_range cmp base top range in
- check_index_ranges (IdSet.add id ids) cmp base' top ranges
- end
-
let add_register id typ env =
wf_typ env typ;
if Bindings.mem id env.registers
@@ -801,24 +773,6 @@ end = struct
{ env with registers = Bindings.add id typ env.registers }
end
- let add_regtyp id base top ranges env =
- if Bindings.mem id env.regtyps
- then typ_error (id_loc id) ("Register type " ^ string_of_id id ^ " is already bound")
- else
- begin
- typ_print ("Adding register type " ^ string_of_id id);
- if Big_int.greater base top
- then check_index_ranges IdSet.empty Big_int.greater (Big_int.add base (Big_int.of_int 1)) (Big_int.sub top (Big_int.of_int 1)) ranges
- else check_index_ranges IdSet.empty Big_int.less (Big_int.sub base (Big_int.of_int 1)) (Big_int.add top (Big_int.of_int 1)) ranges;
- { env with regtyps = Bindings.add id (base, top, ranges) env.regtyps }
- end
-
- let is_regtyp id env = Bindings.mem id env.regtyps
-
- let get_regtyp id env =
- try Bindings.find id env.regtyps with
- | Not_found -> typ_error (id_loc id) (string_of_id id ^ " is not a register type")
-
let get_locals env = env.locals
let lookup_id id env =
@@ -923,16 +877,11 @@ end = struct
rewrap (Typ_fn (aux t1, aux t2, eff))
| Typ_tup ts ->
rewrap (Typ_tup (List.map aux ts))
- | Typ_app (register, [Typ_arg_aux (Typ_arg_typ rtyp,_)])
- when string_of_id register = "register" ->
+ | Typ_app (r, [Typ_arg_aux (Typ_arg_typ rtyp,_)])
+ when string_of_id r = "register" || string_of_id r = "ref" ->
aux rtyp
| Typ_app (id, targs) ->
rewrap (Typ_app (id, List.map aux_arg targs))
- | Typ_id id when is_regtyp id env ->
- let base, top, ranges = get_regtyp id env in
- let len = Big_int.succ (Big_int.abs (Big_int.sub top base)) in
- vector_typ (nconstant len) (get_default_order env) bit_typ
- (* TODO registers with non-default order? non-bitvector registers? *)
| t -> rewrap t
and aux_arg (Typ_arg_aux (targ,a)) =
let rewrap targ = Typ_arg_aux (targ,a) in
@@ -2173,11 +2122,6 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
if is_typ_monomorphic typ || Env.polymorphic_undefineds env
then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
else typ_error l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction")
- (* This rule allows registers of type t to be passed by name with type register<t>*)
- | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ arg_typ, _)])
- when string_of_id id = "register" && Env.is_register reg env ->
- let rtyp = Env.get_register reg env in
- subtyp l env rtyp arg_typ; annot_exp (E_id reg) typ (* CHECK: is this subtyp the correct way around? *)
| E_id id, _ when is_union_id id env ->
begin
match Env.lookup_id id env with
@@ -2513,24 +2457,6 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
let regtyp, inferred_flexp, is_register = infer_flexp flexp in
typ_debug ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp));
match Env.expand_synonyms env regtyp with
- | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp_id, _)), _)]), _)
- (* FIXME: Almost certainly broken *)
- | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env ->
- let eff = mk_effect [BE_wreg] in
- let base, top, ranges = Env.get_regtyp regtyp_id env in
- let range, _ =
- try List.find (fun (_, id) -> Id.compare id field = 0) ranges with
- | Not_found -> typ_error l ("Field " ^ string_of_id field ^ " doesn't exist for register type " ^ string_of_id regtyp_id)
- in
- let vec_typ = match range, Env.get_default_order env with
- | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) ->
- dvector_typ env (nint 1) (mk_typ (Typ_id (mk_id "bit")))
- | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) ->
- dvector_typ env (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) (mk_typ (Typ_id (mk_id "bit")))
- | _, _ -> typ_error l "Not implemented this register field type yet..."
- in
- let checked_exp = crule check_exp env exp vec_typ in
- annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) vec_typ) checked_exp, env
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
let eff = if is_register then mk_effect [BE_wreg] else no_effect in
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
@@ -2565,6 +2491,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
match lexp_aux with
| LEXP_id v ->
begin match Env.lookup_id v env with
+ | Local (Immutable, Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _)) when string_of_id r = "ref" ->
+ subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
| Local (Immutable, _) | Enum _ | Union _ ->
typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
| Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
@@ -2747,31 +2675,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
begin
let inferred_exp = irule infer_exp env exp in
match Env.expand_synonyms env (typ_of inferred_exp) with
- (* Accessing a (bit) field of a register *)
- | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ ((Typ_aux (Typ_id regtyp, _) as regtyp_aux)), _)]), _)
- | (Typ_aux (Typ_id regtyp, _) as regtyp_aux) when Env.is_regtyp regtyp env ->
- let base, top, ranges = Env.get_regtyp regtyp env in
- let range, _ =
- try List.find (fun (_, id) -> Id.compare id field = 0) ranges with
- | Not_found -> typ_error l ("Field " ^ string_of_id field ^ " doesn't exist for register type " ^ string_of_id regtyp)
- in
- let checked_exp = crule check_exp env (strip_exp inferred_exp) regtyp_aux in
- begin
- match range, Env.get_default_order env with
- | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) ->
- let vec_typ = dvector_typ env (nint 1) bit_typ in
- annot_exp (E_field (checked_exp, field)) vec_typ
- | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) ->
- let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) bit_typ in
- annot_exp (E_field (checked_exp, field)) vec_typ
- | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) ->
- let vec_typ = dvector_typ env (nint 1) bit_typ in
- annot_exp (E_field (checked_exp, field)) vec_typ
- | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) ->
- let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub m n) (Big_int.of_int 1))) bit_typ in
- annot_exp (E_field (checked_exp, field)) vec_typ
- | _, _ -> typ_error l "Invalid register field type"
- end
(* Accessing a field of a record *)
| Typ_aux (Typ_id rectyp, _) as typ when Env.is_record rectyp env ->
begin
@@ -2911,6 +2814,12 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let tpat, env = bind_pat env pat ptyp in
let inferred_exp = irule infer_exp env exp in
annot_exp (E_let (LB_aux (LB_val (tpat, bind_exp), (let_loc, None)), inferred_exp)) (typ_of inferred_exp)
+ | E_ref id when Env.is_mutable id env ->
+ let (_, typ) = Bindings.find id (Env.get_locals env) in
+ annot_exp (E_ref id) (ref_typ typ)
+ | E_ref id when Env.is_register id env ->
+ let typ = Env.get_register id env in
+ annot_exp (E_ref id) (register_typ typ)
| _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp)
and infer_funapp l env f xs ret_ctx_typ = fst (infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ)
@@ -3112,6 +3021,7 @@ and propagate_exp_effect_aux = function
let p_xs = List.map propagate_exp_effect xs in
E_nondet p_xs, collect_effects p_xs
| E_id id -> E_id id, no_effect
+ | E_ref id -> E_ref id, no_effect
| E_lit lit -> E_lit lit, no_effect
| E_cast (typ, exp) ->
let p_exp = propagate_exp_effect exp in
@@ -3463,6 +3373,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
| VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext_opt, is_cast) ->
let env = match ext_opt "smt" with Some op -> Env.add_smt_op id op env | None -> env in
Env.wf_typ (add_typquant quants env) typ;
+ typ_debug "CHECKED WELL-FORMED VAL SPEC";
let env =
(* match ext_opt with
| None -> env
@@ -3472,7 +3383,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
let env = if is_cast then Env.add_cast id env else env in
(id, quants, typ, env)
in
- [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms env typ) env
+ [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant quants env) typ) env
let check_default env (DT_aux (ds, l)) =
match ds with
@@ -3483,23 +3394,6 @@ let check_default env (DT_aux (ds, l)) =
(* This branch allows us to write something like: default forall Nat 'n. [|'n|] name... what does this even mean?! *)
| DT_typ (typschm, id) -> typ_error l ("Unsupported default construct")
-let check_register env id base top ranges =
- match base, top with
- | Nexp_aux (Nexp_constant basec, _), Nexp_aux (Nexp_constant topc, _) ->
- let no_typq = TypQ_aux (TypQ_tq [], Parse_ast.Unknown) (* Maybe could be TypQ_no_forall? *) in
- (* FIXME: wrong for default Order inc? *)
- let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub basec topc) (Big_int.of_int 1))) bit_typ in
- let cast_typ = mk_typ (Typ_fn (mk_id_typ id, vec_typ, no_effect)) in
- let cast_to_typ = mk_typ (Typ_fn (vec_typ, mk_id_typ id, no_effect)) in
- env
- |> Env.add_regtyp id basec topc ranges
- (* |> Env.add_typ_synonym id (fun _ -> vec_typ) *)
- |> Env.add_val_spec (mk_id ("cast_" ^ string_of_id id)) (no_typq, cast_typ)
- |> Env.add_cast (mk_id ("cast_" ^ string_of_id id))
- |> Env.add_val_spec (mk_id ("cast_to_" ^ string_of_id id)) (no_typq, cast_to_typ)
- |> Env.add_cast (mk_id ("cast_to_" ^ string_of_id id))
- | _, _ -> typ_error (id_loc id) "Num expressions in register type declaration do not evaluate to constants"
-
let kinded_id_arg kind_id =
let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in
match kind_id with
@@ -3549,7 +3443,9 @@ let mk_synonym typq typ =
let typ, ncs = subst_args kopts args in
if List.for_all (prove env) ncs
then typ
- else typ_error Parse_ast.Unknown "Could not prove constraints in type synonym"
+ else typ_error Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
+ ^ " in type synonym " ^ string_of_typ typ
+ ^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
let check_typedef env (TD_aux (tdef, (l, _))) =
let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Typedef") in
@@ -3567,7 +3463,6 @@ let check_typedef env (TD_aux (tdef, (l, _))) =
[DEF_type (TD_aux (tdef, (l, None)))], env
| TD_enum(id, nmscm, ids, _) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_enum id ids env
- | TD_register(id, base, top, ranges) -> [DEF_type (TD_aux (tdef, (l, Some (env, unit_typ, no_effect))))], check_register env id base top ranges
let check_kinddef env (KD_aux (kdef, (l, _))) =
let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
diff --git a/src/type_check.mli b/src/type_check.mli
index 8f0cd98c..33615e43 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -84,15 +84,10 @@ module Env : sig
val get_register : id -> t -> typ
- val get_regtyp : id -> t -> Big_int.num * Big_int.num * (index_range * id) list
-
(* Return all the identifiers in an enumeration. Throws a type error
if the enumeration doesn't exist. *)
val get_enum : id -> t -> id list
- (* Returns true if id is a register type, false otherwise *)
- val is_regtyp : id -> t -> bool
-
val get_locals : t -> (mut * typ) Bindings.t
val add_local : id -> mut * typ -> t -> t
diff --git a/src/util.ml b/src/util.ml
index bd083a8b..51ed8926 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -392,4 +392,5 @@ let green str = termcode 92 ^ str
let yellow str = termcode 93 ^ str
let red str = termcode 91 ^ str
let cyan str = termcode 96 ^ str
+let blue str = termcode 94 ^ str
let clear str = str ^ termcode 0
diff --git a/src/util.mli b/src/util.mli
index bdf6e594..39bc8a19 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -238,4 +238,5 @@ val green : string -> string
val red : string -> string
val yellow : string -> string
val cyan : string -> string
+val blue : string -> string
val clear : string -> string
diff --git a/src/value.ml b/src/value.ml
index f49b230c..59dadafe 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -50,33 +50,19 @@
module Big_int = Nat_big_num
-type bit = B0 | B1
+module StringMap = Map.Make(String)
type value =
| V_vector of value list
| V_list of value list
| V_int of Big_int.num
| V_bool of bool
- | V_bit of bit
+ | V_bit of Sail_lib.bit
| V_tuple of value list
| V_unit
| V_string of string
| V_ctor of string * value list
-
-let rec string_of_value = function
- | V_vector _ -> "VEC"
- | V_bool true -> "true"
- | V_bool false -> "false"
- | V_bit B0 -> "bitzero"
- | V_bit B1 -> "bitone"
- | V_int n -> Big_int.to_string n
- | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
- | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]"
- | V_unit -> "()"
- | V_string str -> "\"" ^ str ^ "\""
- | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
-
-let eq_value v1 v2 = string_of_value v1 = string_of_value v2
+ | V_record of value StringMap.t
let coerce_bit = function
| V_bit b -> b
@@ -90,6 +76,10 @@ let coerce_bool = function
| V_bool b -> b
| _ -> assert false
+let coerce_record = function
+ | V_record record -> record
+ | _ -> assert false
+
let and_bool = function
| [v1; v2] -> V_bool (coerce_bool v1 && coerce_bool v2)
| _ -> assert false
@@ -98,12 +88,14 @@ let or_bool = function
| [v1; v2] -> V_bool (coerce_bool v1 || coerce_bool v2)
| _ -> assert false
-let print = function
- | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit
- | _ -> assert false
-
let tuple_value (vs : value list) : value = V_tuple vs
+let mk_vector (bits : Sail_lib.bit list) : value = V_vector (List.map (fun bit -> V_bit bit) bits)
+
+let coerce_bit = function
+ | V_bit b -> b
+ | _ -> assert false
+
let coerce_tuple = function
| V_tuple vs -> vs
| _ -> assert false
@@ -111,6 +103,11 @@ let coerce_tuple = function
let coerce_listlike = function
| V_tuple vs -> vs
| V_list vs -> vs
+ | V_unit -> []
+ | _ -> assert false
+
+let coerce_int = function
+ | V_int i -> i
| _ -> assert false
let coerce_cons = function
@@ -118,9 +115,140 @@ let coerce_cons = function
| V_list [] -> None
| _ -> assert false
+let coerce_gv = function
+ | V_vector vs -> vs
+ | _ -> assert false
+
+let coerce_bv = function
+ | V_vector vs -> List.map coerce_bit vs
+ | _ -> assert false
+
+let coerce_string = function
+ | V_string str -> str
+ | _ -> assert false
+
let unit_value = V_unit
-module StringMap = Map.Make(String)
+let value_eq_int = function
+ | [v1; v2] -> V_bool (Sail_lib.eq_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value eq_int"
+
+let value_lteq = function
+ | [v1; v2] -> V_bool (Sail_lib.lteq (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value lteq"
+
+let value_gteq = function
+ | [v1; v2] -> V_bool (Sail_lib.gteq (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value gteq"
+
+let value_lt = function
+ | [v1; v2] -> V_bool (Sail_lib.lt (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value lt"
+
+let value_gt = function
+ | [v1; v2] -> V_bool (Sail_lib.gt (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value gt"
+
+let value_eq_list = function
+ | [v1; v2] -> V_bool (Sail_lib.eq_list (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value eq_list"
+
+let value_eq_string = function
+ | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2))
+ | _ -> failwith "value eq_string"
+
+let value_length = function
+ | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int)
+ | _ -> failwith "value length"
+
+let value_subrange = function
+ | [v1; v2; v3] -> mk_vector (Sail_lib.subrange (coerce_bv v1, coerce_int v2, coerce_int v3))
+ | _ -> failwith "value subrange"
+
+let value_access = function
+ | [v1; v2] -> Sail_lib.access (coerce_gv v1, coerce_int v2)
+ | _ -> failwith "value access"
+
+let value_update = function
+ | [v1; v2; v3] -> V_vector (Sail_lib.update (coerce_gv v1, coerce_int v2, v3))
+ | _ -> failwith "value update"
+
+let value_update_subrange = function
+ | [v1; v2; v3; v4] -> mk_vector (Sail_lib.update_subrange (coerce_bv v1, coerce_int v2, coerce_int v3, coerce_bv v4))
+ | _ -> failwith "value update_subrange"
+
+let value_append = function
+ | [v1; v2] -> V_vector (coerce_gv v1 @ coerce_gv v2)
+ | _ -> failwith "value append"
+
+let value_not = function
+ | [v] -> V_bool (not (coerce_bool v))
+ | _ -> failwith "value not"
+
+let value_not_vec = function
+ | [v] -> mk_vector (Sail_lib.not_vec (coerce_bv v))
+ | _ -> failwith "value not_vec"
+
+let value_and_vec = function
+ | [v1; v2] -> mk_vector (Sail_lib.and_vec (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value not_vec"
+
+let value_or_vec = function
+ | [v1; v2] -> mk_vector (Sail_lib.or_vec (coerce_bv v1, coerce_bv v2))
+ | _ -> failwith "value not_vec"
+
+let value_uint = function
+ | [v] -> V_int (Sail_lib.uint (coerce_bv v))
+ | _ -> failwith "value uint"
+
+let value_sint = function
+ | [v] -> V_int (Sail_lib.sint (coerce_bv v))
+ | _ -> failwith "value sint"
+
+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_add = function
+ | [v1; v2] -> V_int (Sail_lib.add (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value add"
+
+let value_sub = function
+ | [v1; v2] -> V_int (Sail_lib.sub (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value sub"
+
+let value_replicate_bits = function
+ | [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2))
+ | _ -> failwith "value replicate_bits"
+
+let rec string_of_value = function
+ | V_vector vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
+ | V_bool true -> "true"
+ | V_bool false -> "false"
+ | V_bit B0 -> "bitzero"
+ | V_bit B1 -> "bitone"
+ | V_int n -> Big_int.to_string n
+ | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
+ | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]"
+ | V_unit -> "()"
+ | V_string str -> "\"" ^ str ^ "\""
+ | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
+ | V_record record ->
+ "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}"
+
+let eq_value v1 v2 = string_of_value v1 = string_of_value v2
+
+let value_eq_anything = function
+ | [v1; v2] -> V_bool (eq_value v1 v2)
+ | _ -> failwith "value eq_anything"
+
+let value_print = function
+ | [v] -> print_endline (string_of_value v |> Util.red |> Util.clear); V_unit
+ | _ -> assert false
+
+let value_undefined_vector = function
+ | [v1; v2; v3] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, coerce_int v2, v3))
+ | _ -> failwith "value undefined_vector"
let primops =
List.fold_left
@@ -128,5 +256,35 @@ let primops =
StringMap.empty
[ ("and_bool", and_bool);
("or_bool", or_bool);
- ("print_endline", print);
+ ("print_endline", value_print);
+ ("prerr_endline", value_print);
+ ("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);
+ ("lteq", value_lteq);
+ ("gteq", value_gteq);
+ ("lt", value_lt);
+ ("gt", value_gt);
+ ("eq_list", value_eq_list);
+ ("eq_string", value_eq_string);
+ ("eq_anything", value_eq_anything);
+ ("length", value_length);
+ ("subrange", value_subrange);
+ ("access", value_access);
+ ("update", value_update);
+ ("update_subrange", value_update_subrange);
+ ("append", value_append);
+ ("not", value_not);
+ ("not_vec", value_not_vec);
+ ("and_vec", value_and_vec);
+ ("or_vec", value_or_vec);
+ ("uint", value_uint);
+ ("sint", value_sint);
+ ("get_slice_int", value_get_slice_int);
+ ("add", value_add);
+ ("sub", value_sub);
+ ("undefined_bit", fun _ -> V_bit Sail_lib.B0);
+ ("undefined_vector", value_undefined_vector);
+ ("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 05:43:36 +0000