summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile7
-rw-r--r--src/gen_lib/prompt.lem7
-rw-r--r--src/gen_lib/sail_values.lem7
-rw-r--r--src/lem_interp/interp.lem44
-rw-r--r--src/lem_interp/interp_inter_imp.lem34
-rw-r--r--src/lem_interp/interp_interface.lem4
-rw-r--r--src/lem_interp/sail_impl_base.lem43
-rw-r--r--src/pretty_print.ml10
-rw-r--r--src/rewriter.ml5
9 files changed, 91 insertions, 70 deletions
diff --git a/src/Makefile b/src/Makefile
index 30ff9254..8af30456 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -49,6 +49,11 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native
cd _build ;\
../sail.native -lem_ast -o mips $(MIPS_SAILS)
+_build/mips_embedded.lem: $(MIPS_SAILS) ./sail.native
+ mkdir -p _build
+ cd _build ;\
+ ../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS)
+
_build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
mkdir -p _build
cd _build ; \
@@ -80,7 +85,7 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int
run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native
-mips_notlb: _build/mips_notlb.ml _build/mips_extras.ml
+mips_notlb: _build/mips_notlb.ml _build/mips_embedded.lem _build/mips_extras.ml
true
mips: elf run_mips.native
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 6d895a87..4018fd54 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -32,8 +32,8 @@ let inline (>>=) = bind
val (>>) : forall 'b. M unit -> M 'b -> M 'b
let inline (>>) m n = m >>= fun _ -> n
-val exit : forall 'a. string -> M 'a
-let exit s = Fail (Just s)
+val exit : forall 'a 'b. 'b -> M 'a
+let exit s = Fail Nothing
val read_mem : end_flag -> bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
let read_mem endian dir rk addr sz =
@@ -93,6 +93,9 @@ let write_reg_field reg regfield v =
let write_reg_bitfield reg regfield bit =
write_reg_aux (extern_reg_field_whole reg regfield)
(Vector [bit] 0 (is_inc_of_reg reg))
+let write_reg_field_range reg regfield i j v =
+ write_reg_aux (extern_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v
+
val barrier : barrier_kind -> M unit
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 399cc218..2b270e65 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -267,6 +267,8 @@ let hardware_quot (a:integer) (b:integer) : integer =
then (a/b) + 1
else a/b
+let quot_signed = hardware_quot
+
let signed_big = signed
@@ -588,6 +590,11 @@ let rec repeat xs n =
if n = 0 then []
else xs ++ repeat xs (n-1)
+(*
+let duplicate bit length =
+ Vector (repeat [bit] length) (if dir then 0 else length - 1) dir
+ *)
+
let compare_op op (l,r) = bool_to_bit (op l r)
let lt = compare_op (<)
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index fb7053b5..95927318 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -14,6 +14,50 @@ open import Instruction_extractor
type tannot = Interp_utilities.tannot
+type decode_error =
+ | Unsupported_instruction_error of instruction
+ | Not_an_instruction_error of opcode
+ | Internal_error of string
+
+
+let decode_error_compare e1 e2 =
+ match (e1, e2) with
+ | (Unsupported_instruction_error i1, Unsupported_instruction_error i2)
+ -> defaultCompare i1 i2
+ | (Unsupported_instruction_error _, _) -> LT
+ | (_, Unsupported_instruction_error _) -> GT
+
+ | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2
+ | (Not_an_instruction_error _, _) -> LT
+ | (_, Not_an_instruction_error _) -> GT
+
+ | (Internal_error s1, Internal_error s2) -> compare s1 s2
+ (* | (Internal_error _, _) -> LT *)
+ (* | (_, Internal_error _) -> GT *)
+ end
+
+let decode_error_less e1 e2 = decode_error_compare e1 e2 = LT
+let decode_error_less_eq e1 e2 = decode_error_compare e1 e2 <> GT
+let decode_error_greater e1 e2 = decode_error_compare e1 e2 = GT
+let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT
+
+instance (Ord decode_error)
+ let compare = decode_error_compare
+ let (<) = decode_error_less
+ let (<=) = decode_error_less_eq
+ let (>) = decode_error_greater
+ let (>=) = decode_error_greater_eq
+end
+
+let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ
+let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2)
+
+instance (Eq decode_error)
+ let (=) = decode_error_equal
+ let (<>) = decode_error_inequal
+end
+
+
val debug_print : string -> unit
declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 76dc01a1..cd229125 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -307,7 +307,7 @@ type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | I
type interp_value_return =
| Ivh_value of Interp.value
| Ivh_value_after_exn of Interp.value
- | Ivh_error of decode_error
+ | Ivh_error of Interp.decode_error
let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk =
let errk_str = match ivh_mode with
@@ -331,18 +331,18 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
| Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
| Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
(match (ivh_mode,arg) with
- | (Ivh_decode, (Just arg)) -> (Ivh_error (Not_an_instruction_error arg), events_out)
- | (Ivh_illegal, (Just arg)) -> (Ivh_error (Not_an_instruction_error arg), events_out)
- | (Ivh_unsupported, _) -> (Ivh_error (Unsupported_instruction_error instr), events_out)
+ | (Ivh_decode, (Just arg)) -> (Ivh_error (Interp.Not_an_instruction_error arg), events_out)
+ | (Ivh_illegal, (Just arg)) -> (Ivh_error (Interp.Not_an_instruction_error arg), events_out)
+ | (Ivh_unsupported, _) -> (Ivh_error (Interp.Unsupported_instruction_error instr), events_out)
| _ -> Assert_extra.failwith "Reached unreachable pattern" end)
- | _ -> (Ivh_error (Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
- | (Interp.Error l msg,_,_) -> (Ivh_error (Internal_error msg), events_out)
+ | _ -> (Ivh_error (Interp.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
+ | (Interp.Error l msg,_,_) -> (Ivh_error (Interp.Internal_error msg), events_out)
| (Interp.Action (Interp.Return value) stack,_,_) ->
interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
(fun _ -> Interp.resume mode stack (Just value))
| (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
match List.lookup i (Interp_lib.library_functions direction) with
- | Nothing -> (Ivh_error (Internal_error ("External function not available " ^ i)), events_out)
+ | Nothing -> (Ivh_error (Interp.Internal_error ("External function not available " ^ i)), events_out)
| Just f ->
interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
(fun _ -> Interp.resume mode stack (Just (f value)))
@@ -350,8 +350,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
| (Interp.Action (Interp.Fail v) stack, _, _) ->
match (Interp.detaint v) with
| Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) ->
- (Ivh_error (Internal_error ("Assert failed: " ^ s)), events_out)
- | _ -> (Ivh_error (Internal_error "Assert failed"), events_out) end
+ (Ivh_error (Interp.Internal_error ("Assert failed: " ^ s)), events_out)
+ | _ -> (Ivh_error (Interp.Internal_error "Assert failed"), events_out) end
| (Interp.Action (Interp.Exit exp) stack,_,_) ->
interp_to_value_helper arg ivh_mode err_str instr direction registers events true
(fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing)
@@ -361,7 +361,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
| Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i
| _ -> Assert_extra.failwith "Reg not following expected structure" end in
let err_value =
- (Ivh_error (Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)),
+ (Ivh_error (Interp.Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)),
events_out) in
(match registers with
| Nothing -> err_value
@@ -380,14 +380,14 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
interp_to_value_helper arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events)
exn_seen (fun _ -> Interp.resume mode stack Nothing)
| (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
- (Ivh_error (Internal_error ("Read memory request in a " ^ errk_str)), events_out)
+ (Ivh_error (Interp.Internal_error ("Read memory request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
- (Ivh_error (Internal_error ("Write memory request in a " ^ errk_str)), events_out)
+ (Ivh_error (Interp.Internal_error ("Write memory request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
- (Ivh_error (Internal_error ("Write ea request in a " ^ errk_str)), events_out)
+ (Ivh_error (Interp.Internal_error ("Write ea request in a " ^ errk_str)), events_out)
| (Interp.Action (Interp.Write_memv _ _ _) _,_,_) ->
- (Ivh_error (Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
- | _ -> (Ivh_error (Internal_error ("Non expected action in a " ^ errk_str)), events_out)
+ (Ivh_error (Interp.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
+ | _ -> (Ivh_error (Interp.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
end
let call_external_functions direction outcome =
@@ -432,7 +432,7 @@ let translate_address top_level end_flag thunk_name registers address =
| Ivh_value_after_exn _ ->
(Nothing, events)
| Ivh_error err -> match err with
- | Internal_error msg -> Assert_extra.failwith msg
+ | Interp.Internal_error msg -> Assert_extra.failwith msg
| _ -> Assert_extra.failwith "Not an internal error either" end
end
@@ -574,7 +574,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
| _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end)
| Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed"
| Ivh_error err -> match err with
- | Internal_error msg -> Assert_extra.failwith msg
+ | Interp.Internal_error msg -> Assert_extra.failwith msg
| _ -> Assert_extra.failwith "Not an internal error either" end
end
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ea3ba154..2178bb50 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -158,12 +158,12 @@ val initial_instruction_state : context -> string -> list register_value -> inst
type instruction_or_decode_error =
| IDE_instr of instruction * Interp.value
- | IDE_decode_error of decode_error
+ | IDE_decode_error of Interp.decode_error
(** propose to remove the following type and use the above instead *)
type i_state_or_error =
| Instr of instruction * instruction_state
- | Decode_error of decode_error
+ | Decode_error of Interp.decode_error
(** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 63040ebf..bfa161c4 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1356,46 +1356,3 @@ end
type v_kind = Bitv | Bytev
-
-type decode_error =
- | Unsupported_instruction_error of instruction
- | Not_an_instruction_error of opcode
- | Internal_error of string
-
-
-let decode_error_compare e1 e2 =
- match (e1, e2) with
- | (Unsupported_instruction_error i1, Unsupported_instruction_error i2)
- -> defaultCompare i1 i2
- | (Unsupported_instruction_error _, _) -> LT
- | (_, Unsupported_instruction_error _) -> GT
-
- | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2
- | (Not_an_instruction_error _, _) -> LT
- | (_, Not_an_instruction_error _) -> GT
-
- | (Internal_error s1, Internal_error s2) -> compare s1 s2
- (* | (Internal_error _, _) -> LT *)
- (* | (_, Internal_error _) -> GT *)
- end
-
-let decode_error_less e1 e2 = decode_error_compare e1 e2 = LT
-let decode_error_less_eq e1 e2 = decode_error_compare e1 e2 <> GT
-let decode_error_greater e1 e2 = decode_error_compare e1 e2 = GT
-let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT
-
-instance (Ord decode_error)
- let compare = decode_error_compare
- let (<) = decode_error_less
- let (<=) = decode_error_less_eq
- let (>) = decode_error_greater
- let (>=) = decode_error_greater_eq
-end
-
-let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ
-let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2)
-
-instance (Eq decode_error)
- let (=) = decode_error_equal
- let (<>) = decode_error_inequal
-end
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 68a3859c..88b19627 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2266,7 +2266,7 @@ let doc_exp_lem, doc_let_lem =
(prefix 2 1)
(string "write_reg_field_range")
(align (doc_lexp_deref_lem regtypes le ^^ space^^
- doc_id_lem id ^/^ expY e2 ^/^ expY e3 ^/^ expY e))
+ string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e))
| _ ->
(prefix 2 1)
(string "write_reg_range")
@@ -2651,6 +2651,7 @@ let doc_exp_lem, doc_let_lem =
| "multiply" -> aux "*"
| "quot" -> aux2 "quot"
+ | "quot_signed" -> aux2 "quot"
| "modulo" -> aux2 "modulo"
| "add_vec" -> aux2 "add_VVV"
| "add_vec_signed" -> aux2 "addS_VVV"
@@ -3018,7 +3019,8 @@ let doc_dec_lem (DEC_aux (reg,(l,annot))) =
(match annot with
| Base((_,t),_,_,_,_,_) ->
(match t.t with
- | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}]) ->
+ | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}])
+ | Tapp("register", [TA_typ {t= Tabbrev(_,{t=Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])})}]) ->
(match itemt.t,start.nexp,size.nexp with
| Tid "bit", Nconst start, Nconst size ->
let o = if order.order = Oinc then "true" else "false" in
@@ -3048,8 +3050,8 @@ let doc_spec_lem regtypes (VS_aux (valspec,annot)) =
match valspec with
| VS_extern_no_rename _
| VS_extern_spec _ -> empty (* ignore these at the moment *)
- | VS_val_spec (typschm,id) ->
- separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline
+ | VS_val_spec (typschm,id) -> empty
+(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline *)
let doc_def_lem regtypes def = match def with
diff --git a/src/rewriter.ml b/src/rewriter.ml
index dab16ae4..8582f3b5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1596,7 +1596,10 @@ let rewrite_defs_letbind_effects =
k (rewrap (E_comment str))
| E_comment_struc exp' ->
n_exp exp' (fun exp' ->
- k (rewrap (E_comment_struc exp')))
+ k (rewrap (E_comment_struc exp')))
+ | E_return exp' ->
+ n_exp_name exp' (fun exp' ->
+ k (rewrap (E_return exp')))
| E_internal_plet _ -> failwith "E_internal_plet should not be here yet" in
let rewrite_fun _ (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),fdannot)) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:00:24 +0000