summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/coverage/Cargo.toml11
-rw-r--r--lib/coverage/Makefile3
-rw-r--r--lib/coverage/src/lib.rs132
-rw-r--r--sailcov/Makefile4
-rw-r--r--sailcov/dune2
-rw-r--r--sailcov/dune-project1
-rw-r--r--sailcov/main.ml190
-rw-r--r--src/ast_util.ml2
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/jib/anf.ml13
-rw-r--r--src/jib/c_backend.ml149
-rw-r--r--src/jib/c_backend.mli3
-rw-r--r--src/jib/c_codegen.ml14
-rw-r--r--src/jib/jib_compile.ml44
-rw-r--r--src/jib/jib_compile.mli11
-rw-r--r--src/jib/jib_smt.ml7
-rw-r--r--src/lexer.mll12
-rw-r--r--src/rewrites.ml18
-rw-r--r--src/sail.ml9
-rw-r--r--src/type_check.ml16
20 files changed, 460 insertions, 183 deletions
diff --git a/lib/coverage/Cargo.toml b/lib/coverage/Cargo.toml
new file mode 100644
index 00000000..f4fdf1d7
--- /dev/null
+++ b/lib/coverage/Cargo.toml
@@ -0,0 +1,11 @@
+[package]
+name = "sail-coverage"
+version = "0.1.0"
+authors = ["Alasdair <alasdair.armstrong@cl.cam.ac.uk>"]
+edition = "2018"
+
+[dependencies]
+lazy_static = "1.4.0"
+
+[lib]
+crate-type = ["staticlib"]
diff --git a/lib/coverage/Makefile b/lib/coverage/Makefile
new file mode 100644
index 00000000..55ed9fdc
--- /dev/null
+++ b/lib/coverage/Makefile
@@ -0,0 +1,3 @@
+libsail_coverage.a: src/*.rs Cargo.toml Makefile
+ cargo build --release
+ cp target/release/libsail_coverage.a .
diff --git a/lib/coverage/src/lib.rs b/lib/coverage/src/lib.rs
new file mode 100644
index 00000000..003f8b88
--- /dev/null
+++ b/lib/coverage/src/lib.rs
@@ -0,0 +1,132 @@
+extern crate lazy_static;
+use lazy_static::lazy_static;
+
+use std::collections::HashSet;
+use std::ffi::{CStr, CString};
+use std::fs::{OpenOptions, File};
+use std::io::Write;
+use std::os::raw::{c_char, c_int};
+use std::sync::Mutex;
+
+#[derive(Eq, PartialEq, Hash)]
+struct Span {
+ sail_file: CString,
+ line1: i32,
+ char1: i32,
+ line2: i32,
+ char2: i32,
+}
+
+lazy_static! {
+ static ref BRANCHES: Mutex<HashSet<Span>> = Mutex::new(HashSet::new());
+ static ref FUNCTIONS: Mutex<HashSet<Span>> = Mutex::new(HashSet::new());
+}
+
+fn function_entry(_function_name: &CStr, span: Span) {
+ FUNCTIONS.lock().unwrap().insert(span);
+}
+
+fn branch_taken(_branch_id: i32, span: Span) {
+ BRANCHES.lock().unwrap().insert(span);
+}
+
+fn branch_reached(_branch_id: i32, _span: Span) {
+ ()
+}
+
+fn write_locations(file: &mut File, kind: char, spans: &Mutex<HashSet<Span>>) -> bool {
+ for span in spans.lock().unwrap().iter() {
+ let res = write!(
+ file,
+ "{} \"{}\", {}, {}, {}, {}\n",
+ kind,
+ span.sail_file.to_string_lossy(),
+ span.line1,
+ span.char1,
+ span.line2,
+ span.char2,
+ );
+ if res.is_err() {
+ return false;
+ }
+ };
+ true
+}
+
+#[no_mangle]
+pub extern "C" fn sail_coverage_exit() -> c_int {
+ if let Ok(mut file) = OpenOptions::new().create(true).append(true).open("sail_coverage") {
+ if !write_locations(&mut file, 'B', &BRANCHES) {
+ return 1
+ }
+ if !write_locations(&mut file, 'F', &FUNCTIONS) {
+ return 1
+ }
+ 0
+ } else {
+ 1
+ }
+}
+
+#[no_mangle]
+pub unsafe extern "C" fn sail_function_entry(
+ function_name: *const c_char,
+ sail_file: *const c_char,
+ l1: c_int,
+ c1: c_int,
+ l2: c_int,
+ c2: c_int,
+) {
+ function_entry(
+ CStr::from_ptr(function_name),
+ Span {
+ sail_file: CStr::from_ptr(sail_file).into(),
+ line1: l1 as i32,
+ char1: c1 as i32,
+ line2: l2 as i32,
+ char2: c2 as i32,
+ },
+ )
+}
+
+#[no_mangle]
+pub unsafe extern "C" fn sail_branch_taken(
+ branch_id: c_int,
+ sail_file: *const c_char,
+ l1: c_int,
+ c1: c_int,
+ l2: c_int,
+ c2: c_int,
+) {
+ branch_taken(
+ branch_id as i32,
+ Span {
+ sail_file: CStr::from_ptr(sail_file).into(),
+ line1: l1 as i32,
+ char1: c1 as i32,
+ line2: l2 as i32,
+ char2: c2 as i32,
+ },
+ )
+}
+
+#[no_mangle]
+pub unsafe extern "C" fn sail_branch_reached(
+ branch_id: c_int,
+ sail_file: *const c_char,
+ l1: c_int,
+ c1: c_int,
+ l2: c_int,
+ c2: c_int,
+) {
+ branch_reached(
+ branch_id as i32,
+ Span {
+ sail_file: CStr::from_ptr(sail_file).into(),
+ line1: l1 as i32,
+ char1: c1 as i32,
+ line2: l2 as i32,
+ char2: c2 as i32,
+ },
+ )
+}
diff --git a/sailcov/Makefile b/sailcov/Makefile
new file mode 100644
index 00000000..bc9e39d8
--- /dev/null
+++ b/sailcov/Makefile
@@ -0,0 +1,4 @@
+
+sailcov: *.ml dune
+ dune build main.exe
+ cp -f _build/default/main.exe sailcov
diff --git a/sailcov/dune b/sailcov/dune
new file mode 100644
index 00000000..c69fec07
--- /dev/null
+++ b/sailcov/dune
@@ -0,0 +1,2 @@
+(executable
+ (name main))
diff --git a/sailcov/dune-project b/sailcov/dune-project
new file mode 100644
index 00000000..4c6dd5ae
--- /dev/null
+++ b/sailcov/dune-project
@@ -0,0 +1 @@
+(lang dune 2.4)
diff --git a/sailcov/main.ml b/sailcov/main.ml
new file mode 100644
index 00000000..84fbd595
--- /dev/null
+++ b/sailcov/main.ml
@@ -0,0 +1,190 @@
+
+let opt_files = ref ([] : string list)
+
+let opt_taken = ref "sail_coverage"
+
+let opt_all = ref "all_branches"
+
+let options =
+ Arg.align [
+ ( "-t",
+ Arg.String (fun str -> opt_taken := str),
+ "<file> coverage information for branches taken while executing the model (default: sail_coverage)");
+ ( "-a",
+ Arg.String (fun str -> opt_all := str),
+ "<file> information about all possible branches (default: all_branches)")
+ ]
+
+type span = {
+ file : string;
+ l1 : int;
+ c1 : int;
+ l2 : int;
+ c2 : int;
+ }
+
+module Span = struct
+ type t = span
+ let compare s1 s2 = compare s1 s2
+end
+
+module SpanSet = Set.Make(Span)
+module SpanMap = Map.Make(Span)
+
+let mk_span _ file l1 c1 l2 c2 = { file = Filename.basename file; l1 = l1; c1 = c1; l2 = l2; c2 = c2 }
+
+let read_coverage filename =
+ let spans = ref SpanSet.empty in
+ let chan = open_in filename in
+ try
+ let rec loop () =
+ let line = input_line chan in
+ spans := SpanSet.add (Scanf.sscanf line "%c %S, %d, %d, %d, %d" mk_span) !spans;
+ loop ()
+ in
+ loop ()
+ with End_of_file ->
+ close_in chan;
+ !spans
+
+(** We color the source either red (bad) or green (good) if it's
+ covered vs uncovered. If we have nested uncovered branches, they
+ will be increasingly bad, whereas nested covered branches will be
+ increasingly good. *)
+type source_char = {
+ mutable badness : int;
+ mutable goodness : int;
+ char : char;
+ }
+
+let mark_bad_region source span =
+ source.(span.l1 - 1).(span.c1).badness <- source.(span.l1 - 1).(span.c1).badness + 1;
+ source.(span.l2 - 1).(span.c2 - 1).badness <- source.(span.l2 - 1).(span.c2 - 1).badness - 1
+
+let mark_good_region source span =
+ source.(span.l1 - 1).(span.c1).goodness <- source.(span.l1 - 1).(span.c1).goodness + 1;
+ source.(span.l2 - 1).(span.c2 - 1).goodness <- source.(span.l2 - 1).(span.c2 - 1).goodness - 1
+
+let process_line l = Array.init (String.length l) (fun n -> { badness = 0; goodness = 0; char = l.[n] })
+
+let read_source filename =
+ let lines = ref [] in
+ let chan = open_in filename in
+ try
+ let rec loop () =
+ lines := process_line (input_line chan) :: !lines;
+ loop ()
+ in
+ loop ()
+ with End_of_file ->
+ close_in chan;
+ Array.of_list (List.rev !lines)
+
+let output_html_char chan c =
+ if c == ' ' then
+ output_string chan "&nbsp;"
+ else if c == '<' then
+ output_string chan "&lt;"
+ else if c == '>' then
+ output_string chan "&gt;"
+ else if c == '"' then
+ output_string chan "&quot;"
+ else
+ output_char chan c
+
+let main () =
+ let all = read_coverage !opt_all in
+ let taken = read_coverage !opt_taken in
+ List.iter (fun file ->
+ let all = SpanSet.filter (fun s -> s.file = Filename.basename file) all in
+ let taken = SpanSet.filter (fun s -> s.file = Filename.basename file) taken in
+ let not_taken = SpanSet.diff all taken in
+
+ let source = read_source file in
+ SpanSet.iter (mark_good_region source) taken;
+ SpanSet.iter (mark_bad_region source) not_taken;
+
+ let output_file = Filename.remove_extension (Filename.basename file) ^ ".html" in
+ let chan = open_out output_file in
+
+ let current_goodness = ref 0 in
+ let current_badness = ref 0 in
+
+ let good_color () =
+ let darken = 0xE0 - (!current_goodness * 0x20) in
+ Printf.sprintf "#%xFF%x" darken darken
+ in
+ let bad_color () =
+ let darken = 0xE0 - (!current_badness * 0x20) in
+ Printf.sprintf "#FF%x%x" darken darken
+ in
+ output_string chan "<!DOCTYPE html>\n";
+ output_string chan "<html lang=\"en\">\n<head>\n<meta charset=\"utf-8\">\n";
+ output_string chan (Printf.sprintf "<title>%s</title>" (Filename.remove_extension (Filename.basename file)));
+ output_string chan "</head>\n";
+ output_string chan "<body>\n";
+ output_string chan "<code style=\"display: block\">\n";
+
+ Array.iter (fun line ->
+ Array.iter (fun loc ->
+ if loc.goodness < 0 && loc.badness < 0 then (
+ output_html_char chan loc.char;
+ current_goodness := !current_goodness + loc.goodness;
+ current_badness := !current_badness + loc.badness;
+ for _ = 1 to abs loc.goodness + abs loc.badness do
+ output_string chan (Printf.sprintf "</span>")
+ done
+ ) else if loc.goodness < 0 then (
+ assert (loc.badness >= 0);
+ output_html_char chan loc.char;
+ current_goodness := !current_goodness + loc.goodness;
+ for _ = 1 to abs loc.goodness do
+ output_string chan (Printf.sprintf "</span>")
+ done
+ ) else if loc.badness < 0 then (
+ assert (loc.goodness >= 0);
+ output_html_char chan loc.char;
+ current_badness := !current_badness + loc.badness;
+ for _ = 1 to abs loc.badness do
+ output_string chan (Printf.sprintf "</span>")
+ done
+ ) else if loc.badness > 0 then (
+ assert (loc.goodness <= 0);
+ current_badness := !current_badness + loc.badness;
+ for _ = 1 to loc.badness do
+ output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (bad_color ()));
+ done;
+ output_html_char chan loc.char
+ ) else if loc.goodness > 0 then (
+ assert (!current_badness == 0);
+ current_goodness := !current_goodness + loc.goodness;
+ for _ = 1 to loc.goodness do
+ output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (good_color ()));
+ done;
+ output_html_char chan loc.char
+ ) else (
+ output_html_char chan loc.char
+ );
+ assert (!current_goodness >= 0);
+ assert (!current_badness >= 0)
+
+ ) line;
+ output_string chan "<br>\n"
+ ) source;
+
+ output_string chan "</code>\n";
+ output_string chan "</body>\n";
+ output_string chan "</html>";
+
+ close_out chan;
+ Printf.printf "%s (%d/%d)\n" file (SpanSet.cardinal taken) (SpanSet.cardinal all)
+ ) !opt_files
+
+let usage_msg = "usage: sail-coverage-viz -c <file> -a <file> <.sail files>\n"
+
+let _ =
+ Arg.parse options
+ (fun s -> opt_files := !opt_files @ [s])
+ usage_msg;
+ try main () with
+ | Sys_error msg -> prerr_endline msg; exit 1
diff --git a/src/ast_util.ml b/src/ast_util.ml
index ac5da907..d0af5da3 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -89,7 +89,7 @@ let untyp_pat = function
| P_aux (P_typ (typ, pat), _) -> pat, Some typ
| pat -> pat, None
-let mk_pexp pexp_aux = Pat_aux (pexp_aux, no_annot)
+let mk_pexp ?loc:(l=Parse_ast.Unknown) pexp_aux = Pat_aux (pexp_aux, (l, ()))
let mk_mpat mpat_aux = MP_aux (mpat_aux, no_annot)
let mk_mpexp mpexp_aux = MPat_aux (mpexp_aux, no_annot)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 6be8ca34..1449a390 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -84,7 +84,7 @@ val mk_nexp : nexp_aux -> nexp
val mk_exp : ?loc:l -> unit exp_aux -> unit exp
val mk_pat : unit pat_aux -> unit pat
val mk_mpat : unit mpat_aux -> unit mpat
-val mk_pexp : unit pexp_aux -> unit pexp
+val mk_pexp : ?loc:l -> unit pexp_aux -> unit pexp
val mk_mpexp : unit mpexp_aux -> unit mpexp
val mk_lexp : unit lexp_aux -> unit lexp
val mk_lit : lit_aux -> lit
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 7757cd9a..c81f729c 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -525,13 +525,13 @@ let rec apat_globals (AP_aux (aux, _, _)) =
let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in
- let to_aval (AE_aux (aexp_aux, env, l) as aexp) =
- let mk_aexp aexp = AE_aux (aexp, env, l) in
+ let to_aval (AE_aux (aexp_aux, env, _) as aexp) =
+ let mk_aexp (AE_aux (_, _, l)) aexp = AE_aux (aexp, env, l) in
match aexp_aux with
| AE_val v -> (v, fun x -> x)
| AE_short_circuit (_, _, _) ->
let id = gensym () in
- (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp)))
+ (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp x (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp)))
| AE_app (_, _, typ)
| AE_let (_, _, _, _, _, typ)
| AE_return (_, typ)
@@ -544,10 +544,10 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
| AE_record_update (_, _, typ)
| AE_block (_, _, typ) ->
let id = gensym () in
- (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (Immutable, id, typ, aexp, x, typ_of exp)))
+ (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp x (AE_let (Immutable, id, typ, aexp, x, typ_of exp)))
| AE_assign _ | AE_for _ | AE_loop _ | AE_write_ref _ ->
let id = gensym () in
- (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp)))
+ (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp x (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp)))
in
match e_aux with
| E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
@@ -703,7 +703,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
| E_var (LEXP_aux (LEXP_id id, _), binding, body)
| E_var (LEXP_aux (LEXP_cast (_, id), _), binding, body)
- | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) ->
+ | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body)
+ | E_let (LB_aux (LB_val (P_aux (P_typ (_, P_aux (P_id id, _)), _), binding), _), body) ->
let env = env_of body in
let lvar = Env.lookup_id id env in
mk_aexp (AE_let (Mutable, id, lvar_typ lvar, anf binding, anf body, typ_of exp))
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 5947b500..fa4fa802 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -68,7 +68,8 @@ let opt_no_rts = ref false
let opt_prefix = ref "z"
let opt_extra_params = ref None
let opt_extra_arguments = ref None
-
+let opt_branch_coverage = ref false
+
let extra_params () =
match !opt_extra_params with
| Some str -> str ^ ", "
@@ -164,7 +165,7 @@ let literal_to_fragment (L_aux (l_aux, _) as lit) =
| L_false -> Some (V_lit (VL_bool false, CT_bool))
| _ -> None
-module C_config : Config = struct
+module C_config(Opts : sig val branch_coverage : bool end) : Config = struct
(** Convert a sail type into a C-type. This function can be quite
slow, because it uses ctx.local_env and SMT to analyse the Sail
@@ -557,107 +558,13 @@ module C_config : Config = struct
analyze_functions ctx analyze_primop (c_literals ctx aexp)
- let unroll_loops () = None
+ let unroll_loops = None
let specialize_calls = false
let ignore_64 = false
let struct_value = false
let use_real = false
- let branch_coverage = false
-end
-
-(* When compiling to a C library, we want to do things slightly
- differently. First, to ensure that functions have a predictable
- type and calling convention, we don't use the SMT solver to
- optimize types at all. Second we don't apply the analyse primitives
- step in optimize_anf for similar reasons. *)
-module Clib_config : Config = struct
- let rec convert_typ ctx typ =
- let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
- match typ_aux with
- | Typ_id id when string_of_id id = "bit" -> CT_bit
- | Typ_id id when string_of_id id = "bool" -> CT_bool
- | Typ_id id when string_of_id id = "int" -> CT_lint
- | Typ_id id when string_of_id id = "nat" -> CT_lint
- | Typ_id id when string_of_id id = "unit" -> CT_unit
- | Typ_id id when string_of_id id = "string" -> CT_string
- | Typ_id id when string_of_id id = "real" -> CT_real
-
- | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
- | Typ_app (id, _) when
- string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" || string_of_id id = "itself" ->
- begin match destruct_range Env.empty typ with
- | None -> assert false (* Checked if range type in guard *)
- | Some (kids, constr, n, m) ->
- let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env }in
- match nexp_simp n, nexp_simp m with
- | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
- when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
- CT_fint 64
- | _, _ ->
- CT_lint
- end
-
- | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
- CT_list (convert_typ ctx typ)
-
- | Typ_app (id, [A_aux (A_nexp n, _);
- A_aux (A_order ord, _)])
- when string_of_id id = "bitvector" ->
- let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
- begin match nexp_simp n with
- | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
- | _ -> CT_lbits direction
- end
-
- | Typ_app (id, [A_aux (A_nexp n, _);
- A_aux (A_order ord, _);
- A_aux (A_typ typ, _)])
- when string_of_id id = "vector" ->
- let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
- CT_vector (direction, convert_typ ctx typ)
-
- | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
- CT_ref (convert_typ ctx typ)
-
- | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> UBindings.bindings)
- | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants |> UBindings.bindings)
- | Typ_id id when Bindings.mem id ctx.enums -> CT_enum (id, Bindings.find id ctx.enums |> IdSet.elements)
-
- | Typ_tup typs -> CT_tup (List.map (convert_typ ctx) typs)
-
- | Typ_exist _ ->
- begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with
- | Some (kids, nc, typ) ->
- let env = add_existential l kids nc ctx.local_env in
- convert_typ { ctx with local_env = env } typ
- | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!")
- end
-
- | Typ_var kid -> CT_poly
-
- | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
-
- let c_literals ctx =
- let rec c_literal env l = function
- | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) ->
- begin
- match literal_to_fragment lit with
- | Some cval -> AV_cval (cval, typ)
- | None -> v
- end
- | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals)
- | v -> v
- in
- map_aval c_literal
-
- let optimize_anf ctx aexp = c_literals ctx aexp
-
- let unroll_loops () = None
- let specialize_calls = false
- let ignore_64 = false
- let struct_value = false
- let use_real = false
- let branch_coverage = false
+ let branch_coverage = Opts.branch_coverage
+ let track_throw = true
end
(** Functions that have heap-allocated return types are implemented by
@@ -2320,7 +2227,7 @@ let rec get_recursive_functions (Defs defs) =
| [] -> IdSet.empty
let jib_of_ast env ast =
- let module Jibc = Make(C_config) in
+ let module Jibc = Make(C_config(struct let branch_coverage = !opt_branch_coverage end)) in
let ctx = initial_ctx (add_special_functions env) in
Jibc.compile_ast ctx ast
@@ -2341,6 +2248,7 @@ let compile_ast env output_chan c_includes ast =
@ (if !opt_no_rts then [] else
[ string "#include \"rts.h\"";
string "#include \"elf.h\"" ])
+ @ (if !opt_branch_coverage then [string "#include \"sail_coverage.h\""] else [])
@ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes))
in
@@ -2405,22 +2313,32 @@ let compile_ast env output_chan c_includes ast =
@ [ "}" ] ))
in
- let model_default_main = separate hardline (List.map string
- [ "int model_main(int argc, char *argv[])";
- "{";
- " model_init();";
- " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);";
- Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main"));
- " model_fini();";
- " return EXIT_SUCCESS;";
- "}" ] )
+ let model_default_main =
+ ([ "int model_main(int argc, char *argv[])";
+ "{";
+ " model_init();";
+ " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);";
+ Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main"));
+ " model_fini();" ]
+ @ (if !opt_branch_coverage then
+ [ " if (sail_coverage_exit() != 0) {";
+ " fprintf(stderr, \"Could not write coverage information\\n\");";
+ " exit(EXIT_FAILURE);";
+ " }" ]
+ else
+ []
+ )
+ @ [ " return EXIT_SUCCESS;";
+ "}" ])
+ |> List.map string
+ |> separate hardline
in
let model_main = separate hardline (if (!opt_no_main) then [] else List.map string
- [ "int main(int argc, char *argv[])";
- "{";
- " return model_main(argc, argv);";
- "}" ] )
+ [ "int main(int argc, char *argv[])";
+ "{";
+ " return model_main(argc, argv);";
+ "}" ] )
in
let hlhl = hardline ^^ hardline in
@@ -2438,11 +2356,6 @@ let compile_ast env output_chan c_includes ast =
| Type_error (_, l, err) ->
c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
-let jib_of_ast_clib env ast =
- let module Jibc = Make(Clib_config) in
- let ctx = initial_ctx (add_special_functions env) in
- Jibc.compile_ast ctx ast
-
let compile_ast_clib env ast codegen =
let cdefs, ctx = jib_of_ast env ast in
let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 2334cc0e..b10e53d3 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -88,6 +88,8 @@ val opt_prefix : string ref
val opt_extra_params : string option ref
val opt_extra_arguments : string option ref
+val opt_branch_coverage : bool ref
+
(** Optimization flags *)
val optimize_primops : bool ref
@@ -100,5 +102,4 @@ val optimize_fixed_bits : bool ref
val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx
val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit
-val jib_of_ast_clib : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx
val compile_ast_clib : Env.t -> tannot Ast.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit
diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml
index 05abfe70..d5015318 100644
--- a/src/jib/c_codegen.ml
+++ b/src/jib/c_codegen.ml
@@ -213,20 +213,20 @@ let options_from_json json cdefs =
in
opts
-module type Config = sig
+module type Options = sig
val opts : codegen_options
end
-module Make(C: Config) = struct
+module Make(O: Options) = struct
let mangle str =
let mangled = Util.zencode_string str in
- match StringMap.find_opt mangled C.opts.exports_mangled with
+ match StringMap.find_opt mangled O.opts.exports_mangled with
| Some export -> export
| None -> mangled
let sgen_id id =
- match Bindings.find_opt id C.opts.exports with
+ match Bindings.find_opt id O.opts.exports with
| Some export -> export
| None -> mangle (string_of_id id)
@@ -651,7 +651,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
(sgen_function_uid f, false)
in
let sail_state_arg =
- if is_extern && StringSet.mem fname C.opts.state_primops then
+ if is_extern && StringSet.mem fname O.opts.state_primops then
"sail_state *state, "
else
""
@@ -1476,7 +1476,7 @@ let codegen_state_struct ctx cdefs =
^^ string " bool have_exception;" ^^ hardline
^^ string " sail_string *throw_location;" ^^ hardline
))
- ^^ concat_map (fun str -> string (" " ^ str) ^^ hardline) C.opts.extra_state
+ ^^ concat_map (fun str -> string (" " ^ str) ^^ hardline) O.opts.extra_state
^^ string "};"
let is_cdef_startup = function
@@ -1570,7 +1570,7 @@ let codegen ctx output_name cdefs =
let header =
stdlib_headers ^^ hardline
^^ sail_headers ^^ hardline
- ^^ concat_map add_extra_header C.opts.extra_headers ^^ hardline
+ ^^ concat_map add_extra_header O.opts.extra_headers ^^ hardline
^^ string "struct sail_state;" ^^ hardline
^^ string "typedef struct sail_state sail_state;"
^^ twice hardline
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 11bfa2fc..84705ae2 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -58,7 +58,6 @@ open Value2
open Anf
let opt_memo_cache = ref false
-let opt_track_throw = ref true
let optimize_aarch64_fast_struct = ref false
@@ -174,12 +173,13 @@ let initial_ctx env =
module type Config = sig
val convert_typ : ctx -> typ -> ctyp
val optimize_anf : ctx -> typ aexp -> typ aexp
- val unroll_loops : unit -> int option
+ val unroll_loops : int option
val specialize_calls : bool
val ignore_64 : bool
val struct_value : bool
val use_real : bool
val branch_coverage : bool
+ val track_throw : bool
end
module Make(C: Config) = struct
@@ -201,12 +201,10 @@ let coverage_branch_count = ref 0
let coverage_loc_args l =
match Reporting.simp_loc l with
- | None ->
- Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation";
- None
+ | None -> None
| Some (p1, p2) ->
Some (Printf.sprintf "\"%s\", %d, %d, %d, %d"
- p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol))
+ (String.escaped p1.pos_fname) p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol))
let coverage_branch_reached l =
let branch_id = !coverage_branch_count in
@@ -214,9 +212,7 @@ let coverage_branch_reached l =
branch_id,
if C.branch_coverage then
begin match coverage_loc_args l with
- | None ->
- Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation";
- []
+ | None -> []
| Some args ->
[iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)]
end
@@ -234,8 +230,20 @@ let coverage_branch_taken branch_id (AE_aux (_, _, l)) =
else
match coverage_loc_args l with
| None -> []
- | Some args -> [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)]
-
+ | Some args ->
+ print_endline ("B " ^ args);
+ [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)]
+
+let coverage_function_entry id l =
+ if not C.branch_coverage then
+ []
+ else
+ match coverage_loc_args l with
+ | None -> []
+ | Some args ->
+ print_endline ("F " ^ args);
+ [iraw (Printf.sprintf "sail_function_entry(\"%s\", %s);" (string_of_id id) args)]
+
let rec compile_aval l ctx = function
| AV_cval (cval, typ) ->
let ctyp = cval_ctyp cval in
@@ -668,6 +676,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| AE_case (aval, cases, typ) ->
let ctyp = ctyp_of_typ ctx typ in
let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in
+ (* Get the number of cases, because we don't want to check branch
+ coverage for matches with only a single case. *)
+ let num_cases = List.length cases in
let branch_id, on_reached = coverage_branch_reached l in
let case_return_id = ngensym () in
let finish_match_label = label "finish_match_" in
@@ -689,7 +700,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
@ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
else [])
@ body_setup
- @ coverage_branch_taken branch_id body
+ @ (if num_cases > 1 then coverage_branch_taken branch_id body else [])
@ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
@ [igoto finish_match_label]
in
@@ -698,7 +709,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
else
[iblock case_instrs; ilabel case_label]
in
- aval_setup @ on_reached @ [idecl ctyp case_return_id]
+ aval_setup
+ @ (if num_cases > 1 then on_reached else [])
+ @ [idecl ctyp case_return_id]
@ List.concat (List.map compile_case cases)
@ [imatch_failure ()]
@ [ilabel finish_match_label],
@@ -997,7 +1010,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
(* We can either generate an actual loop body for C, or unroll the body for SMT *)
let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in
let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure ()]) in
- let body = match C.unroll_loops () with Some times -> unroll times 0 | None -> actual in
+ let body = match C.unroll_loops with Some times -> unroll times 0 | None -> actual in
variable_init from_gs from_setup from_call from_cleanup
@ variable_init to_gs to_setup to_call to_cleanup
@@ -1106,7 +1119,7 @@ let fix_exception_block ?return:(return=None) ctx instrs =
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
+ @ (if C.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 [])
@@ -1307,6 +1320,7 @@ let compile_funcl ctx id pat guard exp =
let instrs = arg_setup @ destructure @ guard_instrs @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in
let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in
let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in
+ let instrs = coverage_function_entry id (exp_loc exp) @ instrs in
[CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 98ab44de..47ca6962 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -61,11 +61,6 @@ 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
-
(** (WIP) [opt_memo_cache] will store the compiled function
definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum
of the original function to be compiled. Enabled using the -memo
@@ -105,7 +100,7 @@ module type Config = sig
val optimize_anf : ctx -> typ aexp -> typ aexp
(** Unroll all for loops a bounded number of times. Used for SMT
generation. *)
- val unroll_loops : unit -> int option
+ val unroll_loops : int option
(** If false, function arguments must match the function
type exactly. If true, they can be more specific. *)
val specialize_calls : bool
@@ -119,6 +114,10 @@ module type Config = sig
val use_real : bool
(** Insert branch coverage operations *)
val branch_coverage : bool
+ (** If true 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 track_throw : bool
end
module Make(C: Config) : sig
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 734f3fe4..a299d7b9 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1397,7 +1397,7 @@ let rec generate_reg_decs ctx inits = function
let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1))
let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1))
-module SMT_config : Jib_compile.Config = struct
+module SMT_config(Opts : sig val unroll_limit : int end) : Jib_compile.Config = struct
open Jib_compile
(** Convert a sail type into a C-type. This function can be quite
@@ -1560,10 +1560,11 @@ let unroll_static_foreach ctx = function
let specialize_calls = true
let ignore_64 = true
- let unroll_loops () = Some !opt_unroll_limit
+ let unroll_loops = Some Opts.unroll_limit
let struct_value = true
let use_real = true
let branch_coverage = false
+ let track_throw = false
end
@@ -2328,7 +2329,7 @@ let rec build_register_map rmap = function
let compile env ast =
let cdefs, jib_ctx =
- let module Jibc = Jib_compile.Make(SMT_config) in
+ let module Jibc = Jib_compile.Make(SMT_config(struct let unroll_limit = !opt_unroll_limit end)) in
let ctx = Jib_compile.(initial_ctx (add_special_functions env)) in
let t = Profile.start () in
let cdefs, ctx = Jibc.compile_ast ctx ast in
diff --git a/src/lexer.mll b/src/lexer.mll
index 8000879e..40f4b470 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -288,8 +288,10 @@ rule token = parse
| "-" digit+ as i { (Num(Big_int.of_string i)) }
| "0b" (binarydigit+ as i) { (Bin(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) }
| "0x" (hexdigit+ as i) { (Hex(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) }
- | '"' { (String(
- string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+ | '"' { let startpos = Lexing.lexeme_start_p lexbuf in
+ let contents = string startpos (Buffer.create 10) lexbuf in
+ lexbuf.lex_start_p <- startpos;
+ String(contents) }
| eof { Eof }
| _ as c { raise (LexError(
Printf.sprintf "Unexpected character: %c" c,
@@ -331,10 +333,6 @@ and string pos b = parse
| '\\' '\n' ws { Lexing.new_line lexbuf; string pos b lexbuf }
| '\\' { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
"illegal backslash escape in string"*) }
- | '"' { let s = unescaped(Buffer.contents b) in
- (*try Ulib.UTF8.validate s; s
- with Ulib.UTF8.Malformed_code ->
- raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
- "String literal is not valid utf8"))) *) s }
+ | '"' { unescaped (Buffer.contents b) }
| eof { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
"String literal not terminated")))*) }
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 89f67d87..48ea78ae 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -489,6 +489,13 @@ let remove_vector_concat_pat pat =
let decls = List.fold_left (fun f g x -> f (g x)) (fun b -> b) decls in
+ (* Finally we patch up the top location for the expressions wrapped
+ by decls, otherwise this can cause the coverage instrumentation
+ to get super confused by the generated locations *)
+ let decls (E_aux (_, (l, _)) as exp) =
+ let E_aux (aux, (_, annot)) = decls exp in
+ E_aux (aux, (gen_loc l, annot)) in
+
(* at this point shouldn't have P_as patterns in P_vector_concat patterns any more,
all P_as and P_id vectors should have their declarations in decls.
Now flatten all vector_concat patterns *)
@@ -691,7 +698,7 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None
| P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2
| P_wild, _ -> Some []
- | P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) ->
+ | P_app (Id_aux (id1,_),args1), P_app (Id_aux (id2,_),args2) ->
if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None
| P_vector pats1, P_vector pats2
| P_vector_concat pats1, P_vector_concat pats2
@@ -1374,9 +1381,6 @@ let updates_vars exp =
lit vectors in patterns or expressions
*)
let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) =
- let rewrap e = E_aux (e,annot) in
- let rewrap_effects e eff =
- E_aux (e, (l,Some (env_of_annot annot, typ_of_annot annot, eff))) in
let rewrite_rec = rewriters.rewrite_exp rewriters in
let rewrite_base = rewrite_exp rewriters in
match exp with
@@ -2562,7 +2566,7 @@ let fold_typed_guards env guards =
| g :: gs -> List.fold_left (fun g g' -> annot_exp (E_app (mk_id "and_bool", [g; g'])) Parse_ast.Unknown env bool_typ) g gs
-let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot annot)) as pexp) =
+let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (l, _)) as pexp) =
let guards = ref [] in
match pexp_aux with
@@ -2572,13 +2576,13 @@ let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot anno
match !guards with
| [] -> pexp
| gs ->
- let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in
+ let unchecked_pexp = mk_pexp ~loc:l (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in
check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp)
end
| Pat_when (pat, guard, exp) ->
begin
let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in
- let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in
+ let unchecked_pexp = mk_pexp ~loc:l (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in
check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp)
end
diff --git a/src/sail.ml b/src/sail.ml
index 9dbd1f6c..772d8564 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -173,10 +173,10 @@ let options = Arg.align ([
set_target "ir",
" print intermediate representation");
( "-smt",
- Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw],
+ Arg.Tuple [set_target "smt"],
" print SMT translated version of input");
( "-smt_auto",
- Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw; Arg.Set Jib_smt.opt_auto],
+ Arg.Tuple [set_target "smt"; Arg.Set Jib_smt.opt_auto],
" generate SMT and automatically call the solver (implies -smt)");
( "-smt_ignore_overflow",
Arg.Set Jib_smt.opt_ignore_overflow,
@@ -201,7 +201,7 @@ let options = Arg.align ([
" output a C translated version of the input");
( "-c2",
Arg.Tuple [set_target "c2"; Arg.Set Initial_check.opt_undefined_gen],
- " output a C translated version of the input");
+ " output a C translated version of the input (experimental code-generation)");
( "-c_include",
Arg.String (fun i -> opt_includes_c := i::!opt_includes_c),
"<filename> provide additional include for C output");
@@ -232,6 +232,9 @@ let options = Arg.align ([
( "-c_fold_unit",
Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str),
" remove comma separated list of functions from C output, replacing them with unit");
+ ( "-c_coverage",
+ Arg.Set C_backend.opt_branch_coverage,
+ " instrument C code to track branch coverage");
( "-elf",
Arg.String (fun elf -> opt_process_elf := Some elf),
" process an ELF file so that it can be executed by compiled C code");
diff --git a/src/type_check.ml b/src/type_check.ml
index 82bc92d8..73cb8a57 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2994,7 +2994,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let checked_exp = crule check_exp env exp exc_typ in
annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape])
| E_var (lexp, bind, exp), _ ->
- let lexp, bind, env = match bind_assignment env lexp bind with
+ let lexp, bind, env = match bind_assignment l env lexp bind with
| E_aux (E_assign (lexp, bind), _), env -> lexp, bind, env
| _, _ -> assert false
in
@@ -3059,8 +3059,8 @@ and check_block l env exps ret_typ =
match Nl_flow.analyze exps with
| [] -> (match ret_typ with Some typ -> typ_equality l env typ unit_typ; [] | None -> [])
| [exp] -> [final env exp]
- | (E_aux (E_assign (lexp, bind), _) :: exps) ->
- let texp, env = bind_assignment env lexp bind in
+ | (E_aux (E_assign (lexp, bind), (assign_l, _)) :: exps) ->
+ let texp, env = bind_assignment assign_l env lexp bind in
texp :: check_block l env exps ret_typ
| ((E_aux (E_assert (constr_exp, msg), _) as exp) :: exps) ->
let msg = assert_msg msg in
@@ -3548,9 +3548,9 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (A_aux (typ_arg_au
| _, A_order _ -> typ_error env l "Cannot bind type pattern against order"
| _, _ -> typ_error env l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
-and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) =
- let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, mk_tannot env (mk_typ (Typ_id (mk_id "unit"))) no_effect)) in
- let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, mk_tannot env typ eff)) in
+and bind_assignment assign_l env (LEXP_aux (lexp_aux, (lexp_l, ())) as lexp) (E_aux (_, (exp_l, ())) as exp) =
+ let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (assign_l, mk_tannot env (mk_typ (Typ_id (mk_id "unit"))) no_effect)) in
+ let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (lexp_l, mk_tannot env typ eff)) in
let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
let has_typ v env =
match Env.lookup_id v env with
@@ -3559,7 +3559,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
in
match lexp_aux with
| LEXP_memory (f, xs) ->
- check_exp env (E_aux (E_app (f, xs @ [exp]), (l, ()))) unit_typ, env
+ check_exp env (E_aux (E_app (f, xs @ [exp]), (lexp_l, ()))) unit_typ, env
| LEXP_cast (typ_annot, v) ->
let checked_exp = crule check_exp env exp typ_annot in
let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
@@ -3817,7 +3817,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let inferred_exps = List.map (irule infer_exp env) exps in
annot_exp (E_tuple inferred_exps) (mk_typ (Typ_tup (List.map typ_of inferred_exps)))
| E_assign (lexp, bind) ->
- fst (bind_assignment env lexp bind)
+ fst (bind_assignment l env lexp bind)
| E_record_update (exp, fexps) ->
let inferred_exp = irule infer_exp env exp in
let typ = typ_of inferred_exp in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:39:35 +0000