summaryrefslogtreecommitdiff
path: root/src/jib
diff options
context:
space:
mode:
Diffstat (limited to 'src/jib')
-rw-r--r--src/jib/c_backend.ml46
-rw-r--r--src/jib/jib_compile.ml60
-rw-r--r--src/jib/jib_compile.mli5
-rw-r--r--src/jib/jib_ir.ml8
-rw-r--r--src/jib/jib_optimize.ml10
-rw-r--r--src/jib/jib_smt.ml10
-rw-r--r--src/jib/jib_ssa.ml1
-rw-r--r--src/jib/jib_util.ml26
8 files changed, 106 insertions, 60 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index c8cee6ab..2b144d35 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -120,7 +120,7 @@ let rec is_stack_ctyp ctyp = match ctyp with
| CT_lint -> false
| CT_lbits _ when !optimize_fixed_bits -> true
| CT_lbits _ -> false
- | CT_real | CT_string | CT_list _ | CT_vector _ -> false
+ | CT_real | CT_string | CT_list _ | CT_vector _ | CT_fvector _ -> false
| CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
| CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *)
| CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
@@ -588,9 +588,9 @@ let fix_early_heap_return ret ret_ctyp instrs =
before
@ [iblock (rewrite_return instrs)]
@ rewrite_return after
- | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+ | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
before
- @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
+ @ [iif l cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
@ rewrite_return after
| before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
before
@@ -625,9 +625,9 @@ let fix_early_stack_return ret ret_ctyp instrs =
before
@ [iblock (rewrite_return instrs)]
@ rewrite_return after
- | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+ | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
before
- @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
+ @ [iif l cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
@ rewrite_return after
| before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
before
@@ -1069,6 +1069,7 @@ let rec sgen_ctyp = function
| CT_variant (id, _) -> "struct " ^ sgen_id id
| CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
| CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
+ | CT_fvector (_, ord, typ) -> sgen_ctyp (CT_vector (ord, typ))
| CT_string -> "sail_string"
| CT_real -> "real"
| CT_ref ctyp -> sgen_ctyp ctyp ^ "*"
@@ -1090,6 +1091,7 @@ let rec sgen_ctyp_name = function
| CT_variant (id, _) -> sgen_id id
| CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
| CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
+ | CT_fvector (_, ord, typ) -> sgen_ctyp_name (CT_vector (ord, typ))
| CT_string -> "sail_string"
| CT_real -> "real"
| CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp
@@ -1153,8 +1155,6 @@ let rec sgen_cval = function
and sgen_call op cvals =
let open Printf in
match op, cvals with
- | Bit_to_bool, [v] ->
- sprintf "((bool) %s)" (sgen_cval v)
| Bnot, [v] -> "!(" ^ sgen_cval v ^ ")"
| List_hd, [v] ->
sprintf "(%s).hd" ("*" ^ sgen_cval v)
@@ -1326,6 +1326,7 @@ let sgen_cval_param cval =
let rec sgen_clexp = function
| CL_id (Have_exception _, _) -> "have_exception"
| CL_id (Current_exception _, _) -> "current_exception"
+ | CL_id (Throw_location _, _) -> "throw_location"
| CL_id (Return _, _) -> assert false
| CL_id (Name (id, _), _) -> "&" ^ sgen_id id
| CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ zencode_uid field ^ ")"
@@ -1337,6 +1338,7 @@ let rec sgen_clexp = function
let rec sgen_clexp_pure = function
| CL_id (Have_exception _, _) -> "have_exception"
| CL_id (Current_exception _, _) -> "current_exception"
+ | CL_id (Throw_location _, _) -> "throw_location"
| CL_id (Return _, _) -> assert false
| CL_id (Name (id, _), _) -> sgen_id id
| CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ zencode_uid field
@@ -1420,21 +1422,26 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline
^^ string " }"
- | I_funcall (x, extern, f, args) ->
+ | I_funcall (x, special_extern, f, args) ->
let c_args = Util.string_of_list ", " sgen_cval args in
let ctyp = clexp_ctyp x in
- let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || extern in
+ let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || special_extern in
let fname =
- if Env.is_extern (fst f) ctx.tc_env "c" then
- Env.get_extern (fst f) ctx.tc_env "c"
- else if extern then
+ if special_extern then
string_of_id (fst f)
+ else if Env.is_extern (fst f) ctx.tc_env "c" then
+ Env.get_extern (fst f) ctx.tc_env "c"
else
sgen_function_uid f
in
let fname =
match fname, ctyp with
| "internal_pick", _ -> Printf.sprintf "pick_%s" (sgen_ctyp_name ctyp)
+ | "cons", _ ->
+ begin match snd f with
+ | [ctyp] -> Util.zencode_string ("cons#" ^ string_of_ctyp ctyp)
+ | _ -> c_error "cons without specified type"
+ end
| "eq_anything", _ ->
begin match args with
| cval :: _ -> Printf.sprintf "eq_%s" (sgen_ctyp_name (cval_ctyp cval))
@@ -1785,6 +1792,8 @@ let codegen_type_def ctx = function
^^ string "struct zexception *current_exception = NULL;"
^^ hardline
^^ string "bool have_exception = false;"
+ ^^ hardline
+ ^^ string "sail_string *throw_location = NULL;"
else
empty
@@ -2115,7 +2124,7 @@ type c_gen_typ =
let rec ctyp_dependencies = function
| CT_tup ctyps -> List.concat (List.map ctyp_dependencies ctyps) @ [CTG_tup ctyps]
| CT_list ctyp -> ctyp_dependencies ctyp @ [CTG_list ctyp]
- | CT_vector (direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)]
+ | CT_vector (direction, ctyp) | CT_fvector (_, direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)]
| CT_ref ctyp -> ctyp_dependencies ctyp
| CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
| CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
@@ -2216,10 +2225,15 @@ let compile_ast env output_chan c_includes ast =
let exn_boilerplate =
if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else
([ " current_exception = sail_malloc(sizeof(struct zexception));";
- " CREATE(zexception)(current_exception);" ],
- [ " KILL(zexception)(current_exception);";
+ " CREATE(zexception)(current_exception);";
+ " throw_location = sail_malloc(sizeof(sail_string));";
+ " CREATE(sail_string)(throw_location);" ],
+ [ " if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *throw_location);}";
+ " KILL(zexception)(current_exception);";
" sail_free(current_exception);";
- " if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception\\n\"); exit(EXIT_FAILURE);}" ])
+ " KILL(sail_string)(throw_location);";
+ " sail_free(throw_location);";
+ " if (have_exception) {exit(EXIT_FAILURE);}" ])
in
let letbind_initializers =
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 051f5c19..4282ae30 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -58,6 +58,7 @@ open Value2
open Anf
let opt_memo_cache = ref false
+let opt_track_throw = ref true
let optimize_aarch64_fast_struct = ref false
@@ -362,11 +363,14 @@ let rec compile_aval l ctx = function
| V_lit (VL_bit Sail2_values.B1, _) ->
[icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))]
| _ ->
- (* FIXME: Make this work in C *)
- setup @ [iif (V_call (Bit_to_bool, [cval])) [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))] [] CT_unit] @ cleanup
+ setup
+ @ [iextern (CL_id (gs, ctyp))
+ (mk_id "update_fbits", [])
+ [V_id (gs, ctyp); V_lit (VL_int (Big_int.of_int i), CT_fint 64); cval]]
+ @ cleanup
in
[idecl ctyp gs;
- icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init 64 (fun _ -> Sail2_values.B0), direction), ctyp))]
+ icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init len (fun _ -> Sail2_values.B0), direction), ctyp))]
@ List.concat (List.mapi aval_mask (List.rev avals)),
V_id (gs, ctyp),
[]
@@ -407,7 +411,7 @@ let rec compile_aval l ctx = function
let gs = ngensym () in
let mk_cons aval =
let setup, cval, cleanup = compile_aval l ctx aval in
- setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp), []) [cval; V_id (gs, CT_list ctyp)]] @ cleanup
+ setup @ [iextern (CL_id (gs, CT_list ctyp)) (mk_id "cons", [ctyp]) [cval; V_id (gs, CT_list ctyp)]] @ cleanup
in
[idecl (CT_list ctyp) gs]
@ List.concat (List.map mk_cons (List.rev avals)),
@@ -510,7 +514,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
let ctyp = cval_ctyp cval in
match apat_aux with
| AP_id (pid, _) when Env.is_union_constructor pid ctx.tc_env ->
- [ijump (V_ctor_kind (cval, pid, [], cval_ctyp cval)) case_label],
+ [ijump l (V_ctor_kind (cval, pid, [], cval_ctyp cval)) case_label],
[],
ctx
@@ -521,7 +525,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
| AP_id (pid, _) when is_ct_enum ctyp ->
begin match Env.lookup_id pid ctx.tc_env with
| Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx
- | _ -> [ijump (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], ctx
+ | _ -> [ijump l (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], ctx
end
| AP_id (pid, typ) ->
@@ -566,7 +570,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
[], ctor_ctyp
in
let instrs, cleanup, ctx = compile_match ctx apat (V_ctor_unwrap (ctor, cval, unifiers, ctor_ctyp)) case_label in
- [ijump (V_ctor_kind (cval, ctor, unifiers, pat_ctyp)) case_label]
+ [ijump l (V_ctor_kind (cval, ctor, unifiers, pat_ctyp)) case_label]
@ instrs,
cleanup,
ctx
@@ -585,12 +589,12 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
| CT_list ctyp ->
let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in
let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in
- [ijump (V_call (Eq, [cval; V_lit (VL_empty_list, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
+ [ijump l (V_call (Eq, [cval; V_lit (VL_empty_list, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
| _ ->
raise (Reporting.err_general l "Tried to pattern match cons on non list type")
end
- | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_empty_list, ctyp)])) case_label], [], ctx
+ | AP_nil _ -> [ijump l (V_call (Neq, [cval; V_lit (VL_empty_list, ctyp)])) case_label], [], ctx
let unit_cval = V_lit (VL_unit, CT_unit)
@@ -637,7 +641,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
destructure
@ (if not trivial_guard then
guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
- @ [iif (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
+ @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
else [])
@ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
@ [igoto finish_match_label]
@@ -678,7 +682,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
destructure @ [icomment "end destructuring"]
@ (if not trivial_guard then
guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
- @ [ijump (V_call (Bnot, [V_id (gs, CT_bool)])) try_label]
+ @ [ijump l (V_call (Bnot, [V_id (gs, CT_bool)])) try_label]
@ [icomment "end guard"]
else [])
@ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
@@ -689,7 +693,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
assert (ctyp_equal ctyp (ctyp_of_typ ctx typ));
[idecl ctyp try_return_id;
itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup);
- ijump (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label]
+ ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label]
@ List.concat (List.map compile_case cases)
@ [igoto fallthrough_label;
ilabel handled_exception_label;
@@ -711,7 +715,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
in
let setup, cval, cleanup = compile_aval l ctx aval in
setup,
- (fun clexp -> iif cval
+ (fun clexp -> iif l cval
(compile_branch then_aexp clexp)
(compile_branch else_aexp clexp)
if_ctyp),
@@ -746,7 +750,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
let gs = ngensym () in
left_setup
@ [ idecl CT_bool gs;
- iif cval
+ iif l cval
(right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
[icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool false, CT_bool))]
CT_bool ]
@@ -759,7 +763,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
let gs = ngensym () in
left_setup
@ [ idecl CT_bool gs;
- iif cval
+ iif l cval
[icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool true, CT_bool))]
(right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
CT_bool ]
@@ -817,7 +821,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
@ [iblock (cond_setup
@ [cond_call (CL_id (gs, CT_bool))]
@ cond_cleanup
- @ [ijump loop_test loop_end_label]
+ @ [ijump l loop_test loop_end_label]
@ body_setup
@ [body_call (CL_id (unit_gs, CT_unit))]
@ body_cleanup
@@ -842,7 +846,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
@ cond_setup
@ [cond_call (CL_id (gs, CT_bool))]
@ cond_cleanup
- @ [ijump loop_test loop_end_label]
+ @ [ijump l loop_test loop_end_label]
@ [igoto loop_start_label])]
@ [ilabel loop_end_label],
(fun clexp -> icopy l clexp unit_cval),
@@ -873,7 +877,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| AE_throw (aval, typ) ->
(* Cleanup info will be handled by fix_exceptions *)
let throw_setup, cval, _ = compile_aval l ctx aval in
- throw_setup @ [ithrow cval],
+ throw_setup @ [ithrow l cval],
(fun clexp -> icomment "unreachable after throw"),
[]
@@ -933,7 +937,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
let loop_body prefix continue =
prefix
- @ [iblock ([ijump (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label]
+ @ [iblock ([ijump l (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label]
@ body_setup
@ [body_call (CL_id (body_gs, CT_unit))]
@ body_cleanup
@@ -1044,19 +1048,23 @@ let fix_exception_block ?return:(return=None) ctx instrs =
before
@ [iblock (rewrite_exception (historic @ before) instrs)]
@ rewrite_exception (historic @ before) after
- | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+ | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
let historic = historic @ before in
before
- @ [iif cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp]
+ @ [iif l cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp]
@ rewrite_exception historic after
| before, I_aux (I_throw cval, (_, l)) :: after ->
before
@ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval;
icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool))]
+ @ (if !opt_track_throw then
+ let loc_string = Reporting.short_loc_to_string l in
+ [icopy l (CL_id (throw_location, CT_string)) (V_lit (VL_string loc_string, CT_string))]
+ else [])
@ generate_cleanup (historic @ before)
@ [igoto end_block_label]
@ rewrite_exception (historic @ before) after
- | before, (I_aux (I_funcall (x, _, f, args), _) as funcall) :: after ->
+ | before, (I_aux (I_funcall (x, _, f, args), (_, l)) as funcall) :: after ->
let effects = match Env.get_val_spec (fst f) ctx.tc_env with
| _, Typ_aux (Typ_fn (_, _, effects), _) -> effects
| exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *)
@@ -1065,7 +1073,7 @@ let fix_exception_block ?return:(return=None) ctx instrs =
if has_effect effects BE_escape then
before
@ [funcall;
- iif (V_id (have_exception, CT_bool)) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
+ iif l (V_id (have_exception, CT_bool)) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
@ rewrite_exception (historic @ before) after
else
before @ funcall :: rewrite_exception (historic @ before) after
@@ -1159,10 +1167,10 @@ let fix_early_return ret instrs =
before
@ [iblock (rewrite_return (historic @ before) instrs)]
@ rewrite_return (historic @ before) after
- | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+ | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
let historic = historic @ before in
before
- @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp]
+ @ [iif l cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp]
@ rewrite_return historic after
| before, I_aux (I_return cval, (_, l)) :: after ->
let cleanup_label = label "cleanup_" in
@@ -1232,7 +1240,7 @@ let compile_funcl ctx id pat guard exp =
@ guard_setup
@ [guard_call (CL_id (gs, CT_bool))]
@ guard_cleanup
- @ [ijump (V_id (gs, CT_bool)) guard_label;
+ @ [ijump (id_loc id) (V_id (gs, CT_bool)) guard_label;
imatch_failure ();
ilabel guard_label]
)]
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index c863b6ba..9014d8f7 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -61,6 +61,11 @@ open Type_check
ARM v8.5 spec. It is unsound in general. *)
val optimize_aarch64_fast_struct : bool ref
+(** If true (default) track the location of the last exception thrown,
+ useful for debugging C but we want to turn it off for SMT generation
+ where we can't use strings *)
+val opt_track_throw : bool ref
+
(** {2 Jib context} *)
(** Dynamic context for compiling Sail to Jib. We need to pass a
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index ca11696e..4bf726aa 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -69,7 +69,9 @@ let string_of_name =
"return" ^ ssa_num n
| Current_exception n ->
"current_exception" ^ ssa_num n
-
+ | Throw_location n ->
+ "throw_location" ^ ssa_num n
+
let rec string_of_clexp = function
| CL_id (id, ctyp) -> string_of_name id
| CL_field (clexp, field) -> string_of_clexp clexp ^ "." ^ string_of_uid field
@@ -107,7 +109,9 @@ module Ir_formatter = struct
| I_label label ->
C.output_label_instr buf label_map label
| I_jump (cval, label) ->
- add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " " ^ C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map))
+ add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " "
+ ^ C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map)
+ ^ " ` \"" ^ Reporting.short_loc_to_string l ^ "\"")
| I_goto label ->
add_instr n buf indent (C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map))
| I_match_failure ->
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index f4d9c9c2..e0f3bf0d 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -102,10 +102,10 @@ let rec flatten_instrs = function
| I_aux ((I_block block | I_try_block block), _) :: instrs ->
flatten_instrs block @ flatten_instrs instrs
- | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs ->
+ | I_aux (I_if (cval, then_instrs, else_instrs, _), (_, l)) :: instrs ->
let then_label = label "then_" in
let endif_label = label "endif_" in
- [ijump cval then_label]
+ [ijump l cval then_label]
@ flatten_instrs else_instrs
@ [igoto endif_label]
@ [ilabel then_label]
@@ -247,6 +247,7 @@ let ssa_name i = function
| Name (id, _) -> Name (id, i)
| Have_exception _ -> Have_exception i
| Current_exception _ -> Current_exception i
+ | Throw_location _ -> Throw_location i
| Return _ -> Return i
let inline cdefs should_inline instrs =
@@ -404,7 +405,7 @@ let remove_tuples cdefs ctx =
CTSet.add ctyp (List.fold_left CTSet.union CTSet.empty (List.map all_tuples ctyps))
| CT_struct (_, id_ctyps) | CT_variant (_, id_ctyps) ->
List.fold_left (fun cts (_, ctyp) -> CTSet.union (all_tuples ctyp) cts) CTSet.empty id_ctyps
- | CT_list ctyp | CT_vector (_, ctyp) | CT_ref ctyp ->
+ | CT_list ctyp | CT_vector (_, ctyp) | CT_fvector (_, _, ctyp) | CT_ref ctyp ->
all_tuples ctyp
| CT_lint | CT_fint _ | CT_lbits _ | CT_sbits _ | CT_fbits _ | CT_constant _
| CT_unit | CT_bool | CT_real | CT_bit | CT_poly | CT_string | CT_enum _ ->
@@ -415,7 +416,7 @@ let remove_tuples cdefs ctx =
1 + List.fold_left (fun d ctyp -> max d (tuple_depth ctyp)) 0 ctyps
| CT_struct (_, id_ctyps) | CT_variant (_, id_ctyps) ->
List.fold_left (fun d (_, ctyp) -> max (tuple_depth ctyp) d) 0 id_ctyps
- | CT_list ctyp | CT_vector (_, ctyp) | CT_ref ctyp ->
+ | CT_list ctyp | CT_vector (_, ctyp) | CT_fvector (_, _, ctyp) | CT_ref ctyp ->
tuple_depth ctyp
| CT_lint | CT_fint _ | CT_lbits _ | CT_sbits _ | CT_fbits _ | CT_constant _
| CT_unit | CT_bool | CT_real | CT_bit | CT_poly | CT_string | CT_enum _ ->
@@ -432,6 +433,7 @@ let remove_tuples cdefs ctx =
CT_variant (id, List.map (fun (id, ctyp) -> id, fix_tuples ctyp) id_ctyps)
| CT_list ctyp -> CT_list (fix_tuples ctyp)
| CT_vector (d, ctyp) -> CT_vector (d, fix_tuples ctyp)
+ | CT_fvector (n, d, ctyp) -> CT_fvector (n, d, fix_tuples ctyp)
| CT_ref ctyp -> CT_ref (fix_tuples ctyp)
| (CT_lint | CT_fint _ | CT_lbits _ | CT_sbits _ | CT_fbits _ | CT_constant _
| CT_unit | CT_bool | CT_real | CT_bit | CT_poly | CT_string | CT_enum _) as ctyp ->
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 725d2a89..81b876a4 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -198,6 +198,8 @@ let rec smt_ctyp ctx = function
| _ -> failwith ("No registers with ctyp: " ^ string_of_ctyp ctyp)
end
| CT_list _ -> raise (Reporting.err_todo ctx.pragma_l "Lists not yet supported in SMT generation")
+ | CT_fvector _ ->
+ Reporting.unreachable ctx.pragma_l __POS__ "Found CT_fvector in SMT property"
| CT_poly ->
Reporting.unreachable ctx.pragma_l __POS__ "Found polymorphic type in SMT property"
@@ -346,8 +348,6 @@ let rec smt_cval ctx cval =
Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])])
| V_call (Bvor, [cval1; cval2]) ->
Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
- | V_call (Bit_to_bool, [cval]) ->
- Fn ("=", [smt_cval ctx cval; Bitvec_lit [Sail2_values.B1]])
| V_call (Eq, [cval1; cval2]) ->
Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])
| V_call (Bnot, [cval]) ->
@@ -2064,7 +2064,7 @@ let expand_reg_deref env register_map = function
let end_label = label "end_reg_write_" in
let try_reg r =
let next_label = label "next_reg_write_" in
- [ijump (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
+ [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
ifuncall (CL_id (name r, reg_ctyp)) function_id args;
igoto end_label;
ilabel next_label]
@@ -2088,7 +2088,7 @@ let expand_reg_deref env register_map = function
let end_label = label "end_reg_deref_" in
let try_reg r =
let next_label = label "next_reg_deref_" in
- [ijump (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label;
+ [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label;
icopy l clexp (V_id (name r, reg_ctyp));
igoto end_label;
ilabel next_label]
@@ -2110,7 +2110,7 @@ let expand_reg_deref env register_map = function
let end_label = label "end_reg_write_" in
let try_reg r =
let next_label = label "next_reg_write_" in
- [ijump (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
+ [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
icopy l (CL_id (name r, reg_ctyp)) cval;
igoto end_label;
ilabel next_label]
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index b971c1fa..fe3238a4 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -504,6 +504,7 @@ let rename_variables graph root children =
| Name (id, _) -> Name (id, i)
| Have_exception _ -> Have_exception i
| Current_exception _ -> Current_exception i
+ | Throw_location _ -> Throw_location i
| Return _ -> Return i
in
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index d24e6b8a..9b06c7be 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -83,7 +83,7 @@ let ireset ?loc:(l=Parse_ast.Unknown) ctyp id =
let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval =
I_aux (I_init (ctyp, id, cval), (instr_number (), l))
-let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp =
+let iif l cval then_instrs else_instrs ctyp =
I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l))
let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals =
@@ -113,7 +113,7 @@ let iblock ?loc:(l=Parse_ast.Unknown) instrs =
let itry_block ?loc:(l=Parse_ast.Unknown) instrs =
I_aux (I_try_block instrs, (instr_number (), l))
-let ithrow ?loc:(l=Parse_ast.Unknown) cval =
+let ithrow l cval =
I_aux (I_throw cval, (instr_number (), l))
let icomment ?loc:(l=Parse_ast.Unknown) str =
@@ -134,7 +134,7 @@ let imatch_failure ?loc:(l=Parse_ast.Unknown) () =
let iraw ?loc:(l=Parse_ast.Unknown) str =
I_aux (I_raw str, (instr_number (), l))
-let ijump ?loc:(l=Parse_ast.Unknown) cval label =
+let ijump l cval label =
I_aux (I_jump (cval, label), (instr_number (), l))
module Name = struct
@@ -153,6 +153,8 @@ module Name = struct
| _, Have_exception _ -> -1
| Current_exception _, _ -> 1
| _, Current_exception _ -> -1
+ | Throw_location _, _ -> 1
+ | _, Throw_location _ -> -1
end
module NameSet = Set.Make(Name)
@@ -160,6 +162,7 @@ module NameMap = Map.Make(Name)
let current_exception = Current_exception (-1)
let have_exception = Have_exception (-1)
+let throw_location = Throw_location (-1)
let return = Return (-1)
let name id = Name (id, -1)
@@ -268,6 +271,8 @@ let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true)
"(*current_exception)" ^ ssa_num n
| Current_exception n ->
"current_exception" ^ ssa_num n
+ | Throw_location n ->
+ "throw_location" ^ ssa_num n
let string_of_op = function
| Bnot -> "@not"
@@ -275,7 +280,6 @@ let string_of_op = function
| Bor -> "@or"
| List_hd -> "@hd"
| List_tl -> "@tl"
- | Bit_to_bool -> "@bit_to_bool"
| Eq -> "@eq"
| Neq -> "@neq"
| Bvnot -> "@bvnot"
@@ -320,6 +324,7 @@ let rec string_of_ctyp = function
| CT_enum (id, _) -> "%enum " ^ Util.zencode_string (string_of_id id)
| CT_variant (id, _) -> "%union " ^ Util.zencode_string (string_of_id id)
| CT_vector (_, ctyp) -> "%vec(" ^ string_of_ctyp ctyp ^ ")"
+ | CT_fvector (n, _, ctyp) -> "%fvec(" ^ string_of_int n ^ ", " ^ string_of_ctyp ctyp ^ ")"
| CT_list ctyp -> "%list(" ^ string_of_ctyp ctyp ^ ")"
| CT_ref ctyp -> "&(" ^ string_of_ctyp ctyp ^ ")"
| CT_poly -> "*"
@@ -392,6 +397,7 @@ let rec map_ctyp f = function
| CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps))
| CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp))
| CT_vector (direction, ctyp) -> f (CT_vector (direction, map_ctyp f ctyp))
+ | CT_fvector (n, direction, ctyp) -> f (CT_fvector (n, direction, map_ctyp f ctyp))
| CT_list ctyp -> f (CT_list (map_ctyp f ctyp))
| CT_struct (id, ctors) ->
f (CT_struct (id, List.map (fun ((id, ctyps), ctyp) -> (id, List.map (map_ctyp f) ctyps), map_ctyp f ctyp) ctors))
@@ -417,6 +423,7 @@ let rec ctyp_equal ctyp1 ctyp2 =
| CT_string, CT_string -> true
| CT_real, CT_real -> true
| CT_vector (d1, ctyp1), CT_vector (d2, ctyp2) -> d1 = d2 && ctyp_equal ctyp1 ctyp2
+ | CT_fvector (n1, d1, ctyp1), CT_fvector (n2, d2, ctyp2) -> n1 = n2 && d1 = d2 && ctyp_equal ctyp1 ctyp2
| CT_list ctyp1, CT_list ctyp2 -> ctyp_equal ctyp1 ctyp2
| CT_ref ctyp1, CT_ref ctyp2 -> ctyp_equal ctyp1 ctyp2
| CT_poly, CT_poly -> true
@@ -486,6 +493,11 @@ let rec ctyp_compare ctyp1 ctyp2 =
| CT_vector _, _ -> 1
| _, CT_vector _ -> -1
+ | CT_fvector (n1, d1, ctyp1), CT_fvector (n2, d2, ctyp2) ->
+ lex_ord (compare n1 n2) (lex_ord (ctyp_compare ctyp1 ctyp2) (compare d1 d2))
+ | CT_fvector _, _ -> 1
+ | _, CT_fvector _ -> -1
+
| ctyp1, ctyp2 -> String.compare (full_string_of_ctyp ctyp1) (full_string_of_ctyp ctyp2)
module CT = struct
@@ -558,6 +570,7 @@ let rec ctyp_suprema = function
| CT_struct (id, ctors) -> CT_struct (id, ctors)
| CT_variant (id, ctors) -> CT_variant (id, ctors)
| CT_vector (d, ctyp) -> CT_vector (d, ctyp_suprema ctyp)
+ | CT_fvector (n, d, ctyp) -> CT_fvector (n, d, ctyp_suprema ctyp)
| CT_list ctyp -> CT_list (ctyp_suprema ctyp)
| CT_ref ctyp -> CT_ref (ctyp_suprema ctyp)
| CT_poly -> CT_poly
@@ -567,7 +580,7 @@ let rec ctyp_ids = function
| CT_struct (id, ctors) | CT_variant (id, ctors) ->
IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors)
| CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps
- | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
+ | CT_vector (_, ctyp) | CT_fvector (_, _, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
| CT_lint | CT_fint _ | CT_constant _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
| CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
@@ -582,7 +595,7 @@ let rec is_polymorphic = function
| CT_tup ctyps -> List.exists is_polymorphic ctyps
| CT_enum _ -> false
| CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors
- | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp
+ | CT_fvector (_, _, ctyp) | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp
| CT_poly -> true
let rec cval_deps = function
@@ -831,7 +844,6 @@ let label str =
let rec infer_call op vs =
match op, vs with
- | Bit_to_bool, _ -> CT_bool
| Bnot, _ -> CT_bool
| Band, _ -> CT_bool
| Bor, _ -> CT_bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 00:13:45 +0000