summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/_tags2
-rw-r--r--src/initial_check.ml4
-rw-r--r--src/interpreter.ml23
-rw-r--r--src/isail.ml3
-rw-r--r--src/pretty_print_lem_ast.ml21
-rw-r--r--src/rewriter.ml1
-rw-r--r--src/sail.ml2
-rw-r--r--src/sail_lib.ml2
-rw-r--r--src/spec_analysis.ml6
-rw-r--r--src/type_check.ml1
-rw-r--r--src/value.ml12
11 files changed, 45 insertions, 32 deletions
diff --git a/src/_tags b/src/_tags
index f1d54db1..bb9b9c04 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,7 +1,7 @@
true: -traverse, debug, use_menhir
<**/*.ml>: bin_annot, annot
# <lem_interp> or <test>: include
-<sail.{byte,native}>: package(zarith), use_pprint, use_unix, use_str, package(lem)
+<sail.{byte,native}>: package(zarith), package(linksem), package(lem), use_pprint
<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), use_pprint
<isail.ml>: package(linenoise)
<elf_loader.ml>: package(linksem)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 28579291..5f3930b6 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -536,7 +536,7 @@ and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l
let is_ok_in_tup (LEXP_aux (le,(l,_))) =
match le with
| LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
- | LEXP_memory _ ->
+ | LEXP_memory _ | LEXP_deref _ ->
typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in
List.iter is_ok_in_tup ltups;
LEXP_tup(ltups)
@@ -1100,4 +1100,4 @@ let process_ast order defs =
let ast_of_def_string order str =
let def = Parser.def_eof Lexer.token (Lexing.from_string str) in
- process_ast order (Defs [def])
+ process_ast order (Parse_ast.Defs [def])
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 59b20a17..a0482f27 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -81,8 +81,8 @@ let initial_state ast = initial_lstate, initial_gstate ast
let value_of_lit (L_aux (l_aux, _)) =
match l_aux with
| L_unit -> V_unit
- | L_zero -> V_bit B0
- | L_one -> V_bit B1
+ | L_zero -> V_bit Sail_lib.B0
+ | L_one -> V_bit Sail_lib.B1
| L_true -> V_bool true
| L_false -> V_bool false
| L_string str -> V_string str
@@ -389,8 +389,13 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| [] when Env.is_extern id (env_of_annot annot) "interpreter" ->
begin
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)))
+ if extern = "reg_deref" then
+ let regname = List.hd evaluated |> value_of_exp |> coerce_ref in
+ gets >>= fun (_, gstate) ->
+ return (exp_of_value (Bindings.find (mk_id regname) gstate.registers))
+ else
+ 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))
end
@@ -522,7 +527,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| 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
+ puts ({ locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp
| _ -> failwith "Assign"
end
| E_assign (LEXP_aux (LEXP_deref reference, annot), exp) when not (is_value reference) ->
@@ -563,17 +568,12 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
| 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_deref exp -> mk_exp (E_app (mk_id "_reg_deref", [exp]))
| 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 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
@@ -664,7 +664,6 @@ let rec eval_frame' ast = function
| 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
diff --git a/src/isail.ml b/src/isail.ml
index 6b60581b..d8aa55c1 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -206,6 +206,9 @@ let handle_input input =
interactive_state := state;
current_mode := Evaluation (eval_frame !interactive_ast frame);
print_program ()
+ | Break frame ->
+ print_endline "Breakpoint";
+ current_mode := Evaluation frame
end
let () =
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index d42cd2a5..21001f55 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -355,6 +355,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
(list_pp pp_semi_lem_exp pp_lem_exp) exps
kwd ")" pp_lem_l l pp_annot annot
| E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l (pp_annot_tag (tag_id id env)) annot
+ | E_ref(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_ref" pp_lem_id id pp_lem_l l (pp_annot_tag (tag_id id env)) annot
| E_lit(lit) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_lit" pp_lem_lit lit pp_lem_l l pp_annot annot
| E_cast(typ,exp) ->
fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot
@@ -461,15 +462,17 @@ and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd
and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
let print_le ppf lexp =
match lexp with
- | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
- | LEXP_memory(id,args) ->
- fprintf ppf "(LEXP_memory %a [%a])" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
- | LEXP_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id
- | LEXP_tup tups -> fprintf ppf "(LEXP_tup [%a])" (list_pp pp_semi_lem_lexp pp_lem_lexp) tups
- | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
- | LEXP_vector_range(v,e1,e2) ->
- fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2
- | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
+ | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
+ | LEXP_deref exp ->
+ fprintf ppf "(LEXP_deref %a)" pp_lem_exp exp
+ | LEXP_memory(id,args) ->
+ fprintf ppf "(LEXP_memory %a [%a])" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
+ | LEXP_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id
+ | LEXP_tup tups -> fprintf ppf "(LEXP_tup [%a])" (list_pp pp_semi_lem_lexp pp_lem_lexp) tups
+ | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
+ | LEXP_vector_range(v,e1,e2) ->
+ fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2
+ | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
in
fprintf ppf "@[(LEXP_aux %a (%a, %a))@]" print_le lexp pp_lem_l l pp_annot annot
and pp_semi_lem_lexp ppf le = fprintf ppf "@[<1>%a%a@]" pp_lem_lexp le kwd ";"
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 53a43e5b..e0297ae0 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -158,6 +158,7 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with
let effsum = union_effects eff (match lexp with
| LEXP_id _ -> no_effect
| LEXP_cast _ -> no_effect
+ | LEXP_deref e -> effect_of e
| LEXP_memory (_,es) -> union_eff_exps es
| LEXP_tup les ->
List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les
diff --git a/src/sail.ml b/src/sail.ml
index eee80045..e9e55487 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -72,7 +72,7 @@ let options = Arg.align ([
Arg.String (fun f -> opt_file_out := Some f),
"<prefix> select output filename prefix");
( "-i",
- Arg.Set opt_interactive,
+ Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen],
" start interactive interpreter");
( "-ocaml",
Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 72974b9a..849aa16c 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -270,6 +270,7 @@ let hex_char = function
| 'D' | 'd' -> [B1; B1; B0; B1]
| 'E' | 'e' -> [B1; B1; B1; B0]
| 'F' | 'f' -> [B1; B1; B1; B1]
+ | _ -> failwith "Invalid hex character"
let list_of_string s =
let rec aux i acc =
@@ -307,6 +308,7 @@ let string_of_hex = function
| [B1; B1; B0; B1] -> "D"
| [B1; B1; B1; B0] -> "E"
| [B1; B1; B1; B1] -> "F"
+ | _ -> failwith "Cannot convert binary sequence to hex"
let string_of_bits bits =
if List.length bits mod 4 == 0
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 96f6e546..23ce6663 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -367,13 +367,13 @@ and fv_of_pes consider_var bound used set pes =
let bound_g,us_g,set_g = fv_of_exp consider_var bound_p us_p set g in
let bound_e,us_e,set_e = fv_of_exp consider_var bound_g us_g set_g e in
fv_of_pes consider_var bound us_e set_e pes
-
+
and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with
| LB_val(pat,exp) ->
let bound_p, us_p = pat_bindings consider_var bound used pat in
let _,us_e,set_e = fv_of_exp consider_var bound used set exp in
bound_p,Nameset.union us_p us_e,set_e
-
+
and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
match lexp with
| LEXP_id id ->
@@ -382,6 +382,8 @@ and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
if Nameset.mem i bound
then bound, used, Nameset.add i set
else Nameset.add i bound, Nameset.add i used, set
+ | LEXP_deref exp ->
+ fv_of_exp consider_var bound used set exp
| LEXP_cast(typ,id) ->
let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
let i = string_of_id id in
diff --git a/src/type_check.ml b/src/type_check.ml
index b77d800e..66805ba5 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3495,7 +3495,6 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
| _ ->
typ_error l "Bad bitfield type"
end
- | _ -> td_err ()
and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
fun env def ->
diff --git a/src/value.ml b/src/value.ml
index 2ddeecae..7dd3b30b 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -299,8 +299,8 @@ let rec string_of_value = function
| V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]"
| V_bool true -> "true"
| V_bool false -> "false"
- | V_bit B0 -> "bitzero"
- | V_bit B1 -> "bitone"
+ | V_bit Sail_lib.B0 -> "bitzero"
+ | V_bit Sail_lib.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 ^ "|]"
@@ -343,6 +343,10 @@ let value_putchar = function
| [v] -> Sail_lib.putchar (coerce_int v); V_unit
| _ -> failwith "value putchar"
+let value_print_bits = function
+ | [msg; bits] -> print_endline (coerce_string msg ^ string_of_value bits); V_unit
+ | _ -> failwith "value print_bits"
+
let primops =
List.fold_left
(fun r (x, y) -> StringMap.add x y r)
@@ -353,7 +357,7 @@ let primops =
("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);
+ ("print_bits", value_print_bits);
("eq_int", value_eq_int);
("lteq", value_lteq);
("gteq", value_gteq);
@@ -399,5 +403,5 @@ let primops =
("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));
+ ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry));
]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:06:24 +0000