summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorJon French2019-03-04 14:23:55 +0000
committerJon French2019-03-04 14:23:55 +0000
commit94d40fb68bb3d36159a006b93909fc3841c92d28 (patch)
tree219c6d0ae7daf47cd6c8897895d182916e8f3815 /src
parenta7a3402ce155f13234d2d3e5198e5dbf6e0e8b82 (diff)
parent9ed89583d52ccff151fb75424975f2ac4e627a1b (diff)
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.mli1
-rw-r--r--src/c_backend.ml113
-rw-r--r--src/c_backend.mli53
-rw-r--r--src/elf_loader.ml13
-rw-r--r--src/graph.ml21
-rw-r--r--src/graph.mli4
-rw-r--r--src/isail.ml9
-rw-r--r--src/monomorphise.ml43
-rw-r--r--src/pattern_completeness.ml5
-rw-r--r--src/pretty_print_coq.ml397
-rw-r--r--src/rewrites.ml6
-rw-r--r--src/rewrites.mli1
-rw-r--r--src/sail.ml26
-rw-r--r--src/slice.ml194
-rw-r--r--src/specialize.ml39
-rw-r--r--src/specialize.mli7
-rw-r--r--src/type_check.ml93
-rw-r--r--src/type_check.mli4
-rw-r--r--src/value.ml5
19 files changed, 803 insertions, 231 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ae63aca7..bef4a238 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -403,6 +403,7 @@ val ids_of_def : 'a def -> IdSet.t
val ids_of_defs : 'a defs -> IdSet.t
val pat_ids : 'a pat -> IdSet.t
+
val subst : id -> 'a exp -> 'a exp -> 'a exp
val hex_to_bin : string -> string
diff --git a/src/c_backend.ml b/src/c_backend.ml
index aff2d49e..ab388223 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -61,6 +61,7 @@ open Anf
module Big_int = Nat_big_num
let c_verbosity = ref 0
+
let opt_debug_flow_graphs = ref false
let opt_debug_function = ref ""
let opt_trace = ref false
@@ -68,6 +69,20 @@ let opt_smt_trace = ref false
let opt_static = ref false
let opt_no_main = ref false
let opt_memo_cache = ref false
+let opt_no_rts = ref false
+let opt_prefix = ref "z"
+let opt_extra_params = ref None
+let opt_extra_arguments = ref None
+
+let extra_params () =
+ match !opt_extra_params with
+ | Some str -> str ^ ", "
+ | _ -> ""
+
+let extra_arguments is_extern =
+ match !opt_extra_arguments with
+ | Some str when not is_extern -> str ^ ", "
+ | _ -> ""
(* Optimization flags *)
let optimize_primops = ref false
@@ -90,8 +105,8 @@ let zencode_id = function
(* 2. Converting sail types to C types *)
(**************************************************************************)
-let max_int64 = Big_int.of_int64 Int64.max_int
-let min_int64 = Big_int.of_int64 Int64.min_int
+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))
(** The context type contains two type-checking
environments. ctx.local_env contains the closest typechecking
@@ -111,6 +126,7 @@ type ctx =
recursive_functions : IdSet.t;
no_raw : bool;
optimize_smt : bool;
+ iterate_size : bool;
}
let initial_ctx env =
@@ -124,8 +140,17 @@ let initial_ctx env =
recursive_functions = IdSet.empty;
no_raw = false;
optimize_smt = true;
+ iterate_size = false;
}
+let rec iterate_size ctx size n m =
+ if size > 64 then
+ CT_lint
+ else if prove __POS__ ctx.local_env (nc_and (nc_lteq (nconstant (min_int size)) n) (nc_lteq m (nconstant (max_int size)))) then
+ CT_fint size
+ else
+ iterate_size ctx (size + 1) n m
+
(** 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
types and attempts to fit them into the smallest possible C
@@ -151,10 +176,15 @@ let rec ctyp_of_typ ctx typ =
| Some (kids, constr, n, m) ->
match nexp_simp n, nexp_simp m with
| Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
- when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
- CT_fint 64
+ when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
+ if ctx.iterate_size then
+ iterate_size ctx 2 (nconstant n) (nconstant m)
+ else
+ CT_fint 64
| n, m when ctx.optimize_smt ->
- if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
+ if ctx.iterate_size then
+ iterate_size ctx 2 n m
+ else if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then
CT_fint 64
else
CT_lint
@@ -264,7 +294,7 @@ let hex_char =
let literal_to_fragment (L_aux (l_aux, _) as lit) =
match l_aux with
- | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
+ | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
Some (F_lit (V_int n), CT_fint 64)
| L_hex str when String.length str <= 16 ->
let padding = 16 - String.length str in
@@ -544,9 +574,9 @@ let analyze_primop' ctx id args typ =
| Some (kids, constr, n, m) ->
match nexp_simp n, nexp_simp m with
| Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
- when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
+ when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
- | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) ->
+ | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) ->
AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
| _ -> no_change
end
@@ -717,7 +747,7 @@ let rec chunkify n xs =
let rec compile_aval l ctx = function
| AV_C_fragment (frag, typ, ctyp) ->
let ctyp' = ctyp_of_typ ctx typ in
- if not (ctyp_equal ctyp ctyp') then
+ if not (ctyp_equal ctyp ctyp' || ctx.iterate_size) then
raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp'));
[], (frag, ctyp_of_typ ctx typ), []
@@ -737,7 +767,7 @@ let rec compile_aval l ctx = function
| AV_lit (L_aux (L_string str, _), typ) ->
[], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), []
- | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
+ | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
let gs = gensym () in
[iinit CT_lint gs (F_lit (V_int n), CT_fint 64)],
(F_id gs, CT_lint),
@@ -941,8 +971,7 @@ let compile_funcall l ctx id args typ =
ifuncall clexp id setup_args
else
let gs = gensym () in
- iblock [icomment "copy call";
- idecl ret_ctyp gs;
+ iblock [idecl ret_ctyp gs;
ifuncall (CL_id (gs, ret_ctyp)) id setup_args;
icopy l clexp (F_id gs, ret_ctyp);
iclear ret_ctyp gs]
@@ -2405,7 +2434,8 @@ let optimize ctx cdefs =
|> (if !optimize_alias then concatMap unique_names else nothing)
|> (if !optimize_alias then concatMap (remove_alias ctx) else nothing)
|> (if !optimize_alias then concatMap (combine_variables ctx) else nothing)
- |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing)
+ (* We need the runtime to initialize hoisted allocations *)
+ |> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations ctx) else nothing)
|> (if !optimize_hoist_allocations && !optimize_experimental then concatMap (hoist_alias ctx) else nothing)
(**************************************************************************)
@@ -2415,6 +2445,12 @@ let optimize ctx cdefs =
let sgen_id id = Util.zencode_string (string_of_id id)
let codegen_id id = string (sgen_id id)
+let sgen_function_id id =
+ let str = Util.zencode_string (string_of_id id) in
+ !opt_prefix ^ String.sub str 1 (String.length str - 1)
+
+let codegen_function_id id = string (sgen_function_id id)
+
let rec sgen_ctyp = function
| CT_unit -> "unit"
| CT_bit -> "fbits"
@@ -2564,13 +2600,14 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
| I_funcall (x, 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 f ctx.tc_env "c" || extern in
let fname =
if Env.is_extern f ctx.tc_env "c" then
Env.get_extern f ctx.tc_env "c"
else if extern then
string_of_id f
else
- sgen_id f
+ sgen_function_id f
in
let fname =
match fname, ctyp with
@@ -2625,9 +2662,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
else
if is_stack_ctyp ctyp then
- string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args)
+ string (Printf.sprintf " %s = %s(%s%s);" (sgen_clexp_pure x) fname (extra_arguments is_extern) c_args)
else
- string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args)
+ string (Printf.sprintf " %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp x) c_args)
| I_clear (ctyp, id) when is_stack_ctyp ctyp ->
empty
@@ -2843,7 +2880,7 @@ let codegen_type_def ctx = function
in
Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty
in
- string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_id ctor_id) (sgen_id id) ctor_args) ^^ hardline
+ string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_id ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline
^^ surround 2 0 lbrace
(tuple
^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline
@@ -2994,7 +3031,7 @@ let codegen_list_set id ctyp =
let codegen_cons id ctyp =
let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in
- string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
+ string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
^^ string (Printf.sprintf " *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id))
^^ (if is_stack_ctyp ctyp then
string " (*rop)->hd = x;\n"
@@ -3159,9 +3196,9 @@ let codegen_def' ctx = function
if Env.is_extern id ctx.tc_env "c" then
empty
else if is_stack_ctyp ret_ctyp then
- string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+ string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
else
- string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+ string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
| CDEF_fundef (id, ret_arg, args, instrs) as def ->
if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else ();
@@ -3202,12 +3239,12 @@ let codegen_def' ctx = function
| None ->
assert (is_stack_ctyp ret_ctyp);
(if !opt_static then string "static " else empty)
- ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline
+ ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline
| Some gs ->
assert (not (is_stack_ctyp ret_ctyp));
(if !opt_static then string "static " else empty)
- ^^ string "void" ^^ space ^^ codegen_id id
- ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
+ ^^ string "void" ^^ space ^^ codegen_function_id id
+ ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
^^ hardline
in
function_header
@@ -3220,7 +3257,7 @@ let codegen_def' ctx = function
| CDEF_startup (id, instrs) ->
let static = if !opt_static then "static " else "" in
- let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_id id)) in
+ let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_function_id id)) in
separate_map hardline codegen_decl instrs
^^ twice hardline
^^ startup_header ^^ hardline
@@ -3230,7 +3267,7 @@ let codegen_def' ctx = function
| CDEF_finish (id, instrs) ->
let static = if !opt_static then "static " else "" in
- let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_id id)) in
+ let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_function_id id)) in
separate_map hardline codegen_decl (List.filter is_decl instrs)
^^ twice hardline
^^ finish_header ^^ hardline
@@ -3484,7 +3521,7 @@ let smt_trace ctx =
| cdef -> cdef
-let compile_ast ctx c_includes (Defs defs) =
+let compile_ast ctx output_chan c_includes (Defs defs) =
try
c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions"));
let recursive_functions = Spec_analysis.top_sort_defs (Defs defs) |> get_recursive_functions in
@@ -3521,9 +3558,10 @@ let compile_ast ctx c_includes (Defs defs) =
let docs = List.map (codegen_def ctx) cdefs in
let preamble = separate hardline
- ([ string "#include \"sail.h\"";
- string "#include \"rts.h\"";
- string "#include \"elf.h\"" ]
+ ([ string "#include \"sail.h\"" ]
+ @ (if !opt_no_rts then [] else
+ [ string "#include \"rts.h\"";
+ string "#include \"elf.h\"" ])
@ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes))
in
@@ -3567,7 +3605,7 @@ let compile_ast ctx c_includes (Defs defs) =
@ fst exn_boilerplate
@ startup cdefs
@ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
- @ (if regs = [] then [] else [ " zinitializze_registers(UNIT);" ])
+ @ (if regs = [] then [] else [ Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "initialize_registers")) ])
@ letbind_initializers
@ [ "}" ] ))
in
@@ -3588,7 +3626,7 @@ let compile_ast ctx c_includes (Defs defs) =
"{";
" model_init();";
" if (process_arguments(argc, argv)) exit(EXIT_FAILURE);";
- " zmain(UNIT);";
+ Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main"));
" model_fini();";
" return EXIT_SUCCESS;";
"}" ] )
@@ -3604,10 +3642,13 @@ let compile_ast ctx c_includes (Defs defs) =
let hlhl = hardline ^^ hardline in
Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl
- ^^ model_init ^^ hlhl
- ^^ model_fini ^^ hlhl
- ^^ model_default_main ^^ hlhl
- ^^ model_main)
- |> print_endline
+ ^^ (if not !opt_no_rts then
+ model_init ^^ hlhl
+ ^^ model_fini ^^ hlhl
+ ^^ model_default_main ^^ hlhl
+ else
+ empty)
+ ^^ model_main ^^ hardline)
+ |> output_string output_chan
with
Type_error (_, l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
diff --git a/src/c_backend.mli b/src/c_backend.mli
index 10bf9f40..3b26acdf 100644
--- a/src/c_backend.mli
+++ b/src/c_backend.mli
@@ -53,16 +53,54 @@ open Type_check
(** Global compilation options *)
+(** Output a dataflow graph for each generated function in Graphviz
+ (dot) format. *)
val opt_debug_flow_graphs : bool ref
+
+(** Print the ANF and IR representations of a specific function. *)
val opt_debug_function : string ref
+
+(** Instrument generated code to output a trace. opt_smt_trace is WIP
+ but intended to enable generating traces suitable for concolic
+ execution with SMT. *)
val opt_trace : bool ref
val opt_smt_trace : bool ref
+
+(** Define generated functions as static *)
val opt_static : bool ref
+
+(** Do not generate a main function *)
val opt_no_main : bool ref
-(** [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
+(** (WIP) Do not include rts.h (the runtime), and do not generate code
+ that requires any setup or teardown routines to be run by a runtime
+ before executing any instruction semantics. *)
+val opt_no_rts : bool ref
+
+(** Ordinarily we use plain z-encoding to name-mangle generated Sail
+ identifiers into a form suitable for C. If opt_prefix is set, then
+ the "z" which is added on the front of each generated C function
+ will be replaced by opt_prefix. E.g. opt_prefix := "sail_" would
+ give sail_my_function rather than zmy_function. *)
+val opt_prefix : string ref
+
+(** opt_extra_params and opt_extra_arguments allow additional state to
+ be threaded through the generated C code by adding an additional
+ parameter to each function type, and then giving an extra argument
+ to each function call. For example we could have
+
+ opt_extra_params := Some "CPUMIPSState *env"
+ opt_extra_arguments := Some "env"
+
+ and every generated function will take a pointer to a QEMU MIPS
+ processor state, and each function will be passed the env argument
+ when it is called. *)
+val opt_extra_params : string option ref
+val opt_extra_arguments : string option 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
flag. Uses Marshal so it's quite picky about the exact version of
the Sail version. This cache can obviously become stale if the C
backend changes - it'll load an old version compiled without said
@@ -80,16 +118,17 @@ val optimize_experimental : bool ref
(** The compilation context. *)
type ctx
-(** Convert a typ to a IR ctyp *)
-val ctyp_of_typ : ctx -> Ast.typ -> ctyp
-
(** Create a context from a typechecking environment. This environment
should be the environment returned by typechecking the full AST. *)
val initial_ctx : Env.t -> ctx
+(** Convert a typ to a IR ctyp *)
+val ctyp_of_typ : ctx -> Ast.typ -> ctyp
+
+
val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list
-val compile_ast : ctx -> string list -> tannot Ast.defs -> unit
+val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit
val bytecode_ast : ctx -> (cdef list -> cdef list) -> tannot Ast.defs -> cdef list
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index abe935b2..99407393 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -47,9 +47,10 @@ let opt_elf_threads = ref 1
let opt_elf_entry = ref Big_int.zero
let opt_elf_tohost = ref Big_int.zero
-(* the type of elf last loaded *)
+(* the type of elf last loaded, and its symbol map *)
type elf_class = ELF_Class_64 | ELF_Class_32
let opt_elf_class = ref ELF_Class_64 (* default *)
+let opt_symbol_map = ref ([] : Elf_file.global_symbol_init_info)
type word8 = int
@@ -144,6 +145,7 @@ let load_segment ?writer:(writer=write_sail_lib) bs paddr base offset size memsz
let load_elf ?writer:(writer=write_sail_lib) name =
let segments, e_entry, symbol_map = read name in
opt_elf_entry := e_entry;
+ opt_symbol_map := symbol_map;
(if List.mem_assoc "tohost" symbol_map then
let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
opt_elf_tohost := tohost_addr);
@@ -199,3 +201,12 @@ let elf_entry () = !opt_elf_entry
let elf_tohost () = !opt_elf_tohost
(* Used to check last loaded elf class. *)
let elf_class () = !opt_elf_class
+(* Lookup the address for a symbol *)
+let elf_symbol symbol =
+ if List.mem_assoc symbol !opt_symbol_map then
+ let (_, _, addr, _, _) = List.assoc symbol !opt_symbol_map in
+ Some addr
+ else None
+(* Get all symbols *)
+let elf_symbols () =
+ !opt_symbol_map
diff --git a/src/graph.ml b/src/graph.ml
index 2fc09014..e3af0b97 100644
--- a/src/graph.ml
+++ b/src/graph.ml
@@ -88,6 +88,8 @@ module type S =
(** Topologically sort a graph. Throws Not_a_DAG if the graph is
not directed acyclic. *)
val topsort : graph -> node list
+
+ val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit
end
module Make(Ord: OrderedType) = struct
@@ -152,7 +154,9 @@ module Make(Ord: OrderedType) = struct
let prune roots cuts cg =
let rs = reachable roots cuts cg in
- fix_leaves (NM.filter (fun fn _ -> NS.mem fn rs) cg)
+ let cg = NM.filter (fun fn _ -> NS.mem fn rs) cg in
+ let cg = NM.mapi (fun fn children -> if NS.mem fn cuts then NS.empty else children) cg in
+ fix_leaves cg
let remove_self_loops cg =
NM.mapi (fun fn callees -> NS.remove fn callees) cg
@@ -206,4 +210,19 @@ module Make(Ord: OrderedType) = struct
in topsort' (); !list
+ let make_dot node_color edge_color string_of_node out_chan graph =
+ Util.opt_colors := false;
+ let to_string node = String.escaped (string_of_node node) in
+ output_string out_chan "digraph DEPS {\n";
+ let make_node from_node =
+ output_string out_chan (Printf.sprintf " \"%s\" [fillcolor=%s;style=filled];\n" (to_string from_node) (node_color from_node))
+ in
+ let make_line from_node to_node =
+ output_string out_chan (Printf.sprintf " \"%s\" -> \"%s\" [color=%s];\n" (to_string from_node) (to_string to_node) (edge_color from_node to_node))
+ in
+ NM.bindings graph |> List.iter (fun (from_node, _) -> make_node from_node);
+ NM.bindings graph |> List.iter (fun (from_node, to_nodes) -> NS.iter (make_line from_node) to_nodes);
+ output_string out_chan "}\n";
+ Util.opt_colors := true;
+
end
diff --git a/src/graph.mli b/src/graph.mli
index 11ea63dc..09b78304 100644
--- a/src/graph.mli
+++ b/src/graph.mli
@@ -90,9 +90,11 @@ module type S =
(** Topologically sort a graph. Throws Not_a_DAG if the graph is
not directed acyclic. *)
val topsort : graph -> node list
+
+ val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit
end
module Make(Ord: OrderedType) : S
with type node = Ord.t
and type node_set = Set.Make(Ord).t
- and type graph = Set.Make(Ord).t Map.Make(Ord).t
+ and type graph = Set.Make(Ord).t Map.Make(Ord).t
diff --git a/src/isail.ml b/src/isail.ml
index 9a300673..30e02b36 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -374,15 +374,6 @@ let handle_input' input =
":(c)ommand can be called as either :c or :command." ]
in
List.iter print_endline commands
- | ":poly" ->
- let is_kopt = match arg with
- | "Int" -> is_int_kopt
- | "Type" -> is_typ_kopt
- | "Order" -> is_order_kopt
- | _ -> failwith "Invalid kind"
- in
- let ids = Specialize.polymorphic_functions is_kopt !Interactive.ast in
- List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements ids)
| ":option" ->
begin
try
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index c67b4fcb..9b954611 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -199,10 +199,9 @@ let rec is_value (E_aux (e,(l,annot))) =
(* TODO: more? *)
| _ -> false
-let is_pure (Effect_opt_aux (e,_)) =
+let is_pure e =
match e with
- | Effect_opt_none -> true
- | Effect_opt_effect (Effect_aux (Effect_set [],_)) -> true
+ | Effect_aux (Effect_set [],_) -> true
| _ -> false
let rec list_extract f = function
@@ -345,6 +344,7 @@ and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) =
match ta with
| A_nexp _
| A_order _
+ | A_bool _
-> insts, tyarg
| A_typ typ ->
let insts', typ' = inst_src_type insts typ in
@@ -365,6 +365,7 @@ and contains_exist_arg (A_aux (arg,_)) =
match arg with
| A_nexp _
| A_order _
+ | A_bool _
-> false
| A_typ typ -> contains_exist typ
@@ -1507,14 +1508,19 @@ let split_defs all_errors splits defs =
if not (List.for_all is_value args) then
None
else
+ let (tq,typ) = Env.get_val_spec_orig id env in
+ let eff = match typ with
+ | Typ_aux (Typ_fn (_,_,eff),_) -> Some eff
+ | _ -> None
+ in
let Defs ds = defs in
- match list_extract (function
+ match eff, list_extract (function
| (DEF_fundef (FD_aux (FD_function (_,_,eff,((FCL_aux (FCL_Funcl (id',_),_))::_ as fcls)),_)))
- -> if Id.compare id id' = 0 then Some (eff,fcls) else None
+ -> if Id.compare id id' = 0 then Some fcls else None
| _ -> None) ds with
- | None -> None
- | Some (eff,_) when not (is_pure eff) -> None
- | Some (_,fcls) ->
+ | None,_ | _,None -> None
+ | Some eff,_ when not (is_pure eff) -> None
+ | Some _,Some fcls ->
let arg = match args with
| [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot))
| [e] -> e
@@ -2081,19 +2087,26 @@ let split_defs all_errors splits defs =
| LEXP_vector_concat les -> re (LEXP_vector_concat (List.map map_lexp les))
| LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id))
| LEXP_deref e -> re (LEXP_deref (map_exp e))
- in map_pexp, map_letbind
- in
+ in map_exp, map_pexp, map_letbind
+ in
+ let map_exp r = let (f,_,_) = map_fns r in f in
+ let map_pexp r = let (_,f,_) = map_fns r in f in
+ let map_letbind r = let (_,_,f) = map_fns r in f in
+ let map_exp exp =
+ let ref_vars = referenced_vars exp in
+ map_exp ref_vars exp
+ in
let map_pexp top_pexp =
(* Construct the set of referenced variables so that we don't accidentally
make false assumptions about them during constant propagation. Note that
we assume there aren't any in the guard. *)
let (_,_,body,_) = destruct_pexp top_pexp in
let ref_vars = referenced_vars body in
- fst (map_fns ref_vars) top_pexp
+ map_pexp ref_vars top_pexp
in
let map_letbind (LB_aux (LB_val (_,e),_) as lb) =
let ref_vars = referenced_vars e in
- snd (map_fns ref_vars) lb
+ map_letbind ref_vars lb
in
let map_funcl (FCL_aux (FCL_Funcl (id,pexp),annot)) =
@@ -2124,6 +2137,7 @@ let split_defs all_errors splits defs =
| DEF_mapdef (MD_aux (_, (l, _))) -> Reporting.unreachable l __POS__ "mappings should be gone by now"
| DEF_val lb -> [DEF_val (map_letbind lb)]
| DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd)
+ | DEF_measure (id,pat,exp) -> [DEF_measure (id,pat,map_exp exp)]
in
Defs (List.concat (List.map map_def defs))
in
@@ -2206,6 +2220,7 @@ and sizes_of_typarg (A_aux (ta,_)) =
match ta with
A_nexp _
| A_order _
+ | A_bool _
-> KidSet.empty
| A_typ typ -> sizes_of_typ typ
@@ -4375,7 +4390,9 @@ let replace_nexp_in_typ env typ orig new_nexp =
| A_typ typ ->
let f, typ = aux typ in
f, A_aux (A_typ typ,l)
- | A_order _ -> false, typ_arg
+ | A_order _
+ | A_bool _
+ -> false, typ_arg
in aux typ
let fresh_nexp_kid nexp =
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 514eb5c0..79fc93ee 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -89,7 +89,7 @@ let is_wild = function
| GP_wild -> true
| _ -> false
-let rec generalize ctx (P_aux (p_aux, _) as pat) =
+let rec generalize ctx (P_aux (p_aux, (l, _)) as pat) =
match p_aux with
| P_lit (L_aux (L_unit, _)) ->
(* Unit pattern always matches on unit, so generalize to wildcard *)
@@ -105,7 +105,8 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) =
match ctx.lookup_id id with
| Unbound -> GP_wild
| Local (Immutable, _) -> GP_wild
- | Register _ | Local (Mutable, _) -> Util.warn "Matching on register or mutable variable"; GP_wild
+ | Register _ | Local (Mutable, _) ->
+ Util.warn ("Matching on register or mutable variable at " ^ Reporting.loc_to_string l); GP_wild
| Enum _ -> GP_app (Bindings.singleton id GP_wild)
end
| P_var (pat, _) -> generalize ctx pat
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index adb00a77..4553de56 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -356,7 +356,8 @@ match nc1, nc2 with
| _, NC_aux (NC_true,_) -> nc1
| NC_aux (NC_false,_), _ -> nc_not nc2
| _, NC_aux (NC_false,_) -> nc_not nc1
-| _,_ -> nc_or (nc_and nc1 nc2) (nc_and (nc_not nc1) (nc_not nc2))
+ (* TODO: replace this hacky iff with a proper NC_ constructor *)
+| _,_ -> mk_nc (NC_app (mk_id "iff",[arg_bool nc1; arg_bool nc2]))
(* n_constraint functions are currently just Z3 functions *)
let doc_nc_fn_prop id =
@@ -370,33 +371,123 @@ let doc_nc_fn id =
| "not" -> string "negb"
| s -> string s
-type ex_atom_bool = ExBool_simple | ExBool_val of bool | ExBool_complex
+let merge_bool_count = KBindings.union (fun _ m n -> Some (m+n))
-let non_trivial_ex_atom_bool l kopts nc atom_nc =
- let vars = KOptSet.union (kopts_of_constraint nc) (kopts_of_constraint atom_nc) in
- let exists = KOptSet.of_list kopts in
- if KOptSet.subset vars exists then
- let kenv = List.fold_left (fun kenv kopt -> KBindings.add (kopt_kid kopt) (unaux_kind (kopt_kind kopt)) kenv) KBindings.empty kopts in
- match Constraint.call_smt l kenv (nc_and nc atom_nc),
- Constraint.call_smt l kenv (nc_and nc (nc_not atom_nc)) with
- | Sat, Sat -> ExBool_simple
- | Sat, Unsat -> ExBool_val true
- | Unsat, Sat -> ExBool_val false
- | _ -> ExBool_complex
- else ExBool_complex
-
-type ex_kind = ExNone | ExBool | ExGeneral
-
-let classify_ex_type (Typ_aux (t,l) as t0) =
+let rec count_bool_vars (NC_aux (nc,_)) =
+ let count_arg (A_aux (arg,_)) =
+ match arg with
+ | A_bool nc -> count_bool_vars nc
+ | A_nexp _ | A_typ _ | A_order _ -> KBindings.empty
+ in
+ match nc with
+ | NC_or (nc1,nc2)
+ | NC_and (nc1,nc2)
+ -> merge_bool_count (count_bool_vars nc1) (count_bool_vars nc2)
+ | NC_var kid -> KBindings.singleton kid 1
+ | NC_equal _ | NC_bounded_ge _ | NC_bounded_le _ | NC_not_equal _
+ | NC_set _ | NC_true | NC_false
+ -> KBindings.empty
+ | NC_app (_,args) ->
+ List.fold_left merge_bool_count KBindings.empty (List.map count_arg args)
+
+type atom_bool_prop =
+ Bool_boring
+| Bool_complex of kinded_id list * n_constraint * n_constraint
+
+let simplify_atom_bool l kopts nc atom_nc =
+(*prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*)
+ let counter = ref 0 in
+ let is_bound kid = List.exists (fun kopt -> Kid.compare kid (kopt_kid kopt) == 0) kopts in
+ let bool_vars = merge_bool_count (count_bool_vars nc) (count_bool_vars atom_nc) in
+ let lin_bool_vars = KBindings.filter (fun kid n -> is_bound kid && n = 1) bool_vars in
+ let rec simplify (NC_aux (nc,l) as nc_full) =
+ let is_ex_var news (NC_aux (nc,_)) =
+ match nc with
+ | NC_var kid when KBindings.mem kid lin_bool_vars -> Some kid
+ | NC_var kid when KidSet.mem kid news -> Some kid
+ | _ -> None
+ in
+ let replace kills vars =
+ let v = mk_kid ("simp#" ^ string_of_int !counter) in
+ let kills = KidSet.union kills (KidSet.of_list vars) in
+ counter := !counter + 1;
+ KidSet.singleton v, kills, NC_aux (NC_var v,l)
+ in
+ match nc with
+ | NC_or (nc1,nc2) -> begin
+ let new1, kill1, nc1 = simplify nc1 in
+ let new2, kill2, nc2 = simplify nc2 in
+ let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in
+ match is_ex_var news nc1, is_ex_var news nc2 with
+ | Some kid1, Some kid2 -> replace kills [kid1;kid2]
+ | _ -> news, kills, NC_aux (NC_or (nc1,nc2),l)
+ end
+ | NC_and (nc1,nc2) -> begin
+ let new1, kill1, nc1 = simplify nc1 in
+ let new2, kill2, nc2 = simplify nc2 in
+ let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in
+ match is_ex_var news nc1, is_ex_var news nc2 with
+ | Some kid1, Some kid2 -> replace kills [kid1;kid2]
+ | _ -> news, kills, NC_aux (NC_and (nc1,nc2),l)
+ end
+ | NC_app (Id_aux (Id "not",_) as id,[A_aux (A_bool nc1,al)]) -> begin
+ let new1, kill1, nc1 = simplify nc1 in
+ match is_ex_var new1 nc1 with
+ | Some kid -> replace kill1 [kid]
+ | None -> new1, kill1, NC_aux (NC_app (id,[A_aux (A_bool nc1,al)]),l)
+ end
+ (* We don't currently recurse into general uses of NC_app, but the
+ "boring" cases we really want to get rid of won't contain
+ those. *)
+ | _ -> KidSet.empty, KidSet.empty, nc_full
+ in
+ let new_nc, kill_nc, nc = simplify nc in
+ let new_atom, kill_atom, atom_nc = simplify atom_nc in
+ let new_kids = KidSet.union new_nc new_atom in
+ let kill_kids = KidSet.union kill_nc kill_atom in
+ let kopts =
+ List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @
+ List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts
+ in
+(*prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*)
+ match atom_nc with
+ | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring
+ | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring
+ | _ -> Bool_complex (kopts, nc, atom_nc)
+
+
+type ex_kind = ExNone | ExGeneral
+
+(* Should a Sail type be turned into a dependent pair in Coq?
+ Optionally takes a variable that we're binding (to avoid trivial cases where
+ the type is exactly the boolean we're binding), and whether to turn bools
+ with interesting type-expressions into dependent pairs. *)
+let classify_ex_type ctxt env ?binding ?(rawbools=false) (Typ_aux (t,l) as t0) =
+ let is_binding kid =
+ match binding, KBindings.find_opt kid ctxt.kid_id_renames with
+ | Some id, Some id' when Id.compare id id' == 0 -> true
+ | _ -> false
+ in
+ let simplify_atom_bool l kopts nc atom_nc =
+ match simplify_atom_bool l kopts nc atom_nc with
+ | Bool_boring -> Bool_boring
+ | Bool_complex (_,_,NC_aux (NC_var kid,_)) when is_binding kid -> Bool_boring
+ | Bool_complex (x,y,z) -> Bool_complex (x,y,z)
+ in
match t with
- | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin
- match non_trivial_ex_atom_bool l kopts nc atom_nc with
- | ExBool_simple -> ExNone, t1
- | ExBool_val _ -> ExBool, t1
- | ExBool_complex -> ExGeneral, t1
+ | Typ_exist (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_)) -> begin
+ match simplify_atom_bool l kopts nc atom_nc with
+ | Bool_boring -> ExNone, [], bool_typ
+ | Bool_complex _ -> ExGeneral, [], bool_typ
end
- | Typ_exist (_,_,t1) -> ExGeneral,t1
- | _ -> ExNone,t0
+ | Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]) -> begin
+ match rawbools, simplify_atom_bool l [] nc_true atom_nc with
+ | false, _ -> ExNone, [], bool_typ
+ | _,Bool_boring -> ExNone, [], bool_typ
+ | _,Bool_complex _ -> ExGeneral, [], bool_typ
+ end
+ | Typ_exist (kopts,_,t1) -> ExGeneral,kopts,t1
+ | _ -> ExNone,[],t0
(* When making changes here, check whether they affect coq_nvars_of_typ *)
let rec doc_typ_fns ctx =
@@ -441,10 +532,17 @@ let rec doc_typ_fns ctx =
(string "Z")
| Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
(string "Z")
- | Typ_app(Id_aux (Id "atom_bool", _), [_]) -> string "bool"
- | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool nc,_)]) ->
- let tpp = string "Bool" ^^ space ^^ doc_nc_prop ~top:false ctx nc in
- if atyp_needed then parens tpp else tpp
+ | Typ_app(Id_aux (Id "atom_bool", _), [A_aux (A_bool atom_nc,_)]) ->
+ begin match simplify_atom_bool l [] nc_true atom_nc with
+ | Bool_boring -> string "bool"
+ | Bool_complex (_,_,atom_nc) -> (* simplify won't introduce new kopts *)
+ let var = mk_kid "_bool" in (* TODO collision avoid *)
+ let nc = nice_iff (nc_var var) atom_nc in
+ braces (separate space
+ [doc_var ctx var; colon; string "bool";
+ ampersand;
+ doc_arithfact ctx nc])
+ end
| Typ_app(id,args) ->
let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in
if atyp_needed then parens tpp else tpp
@@ -505,10 +603,9 @@ let rec doc_typ_fns ctx =
ampersand;
doc_arithfact ctx ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc])
| Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin
- match non_trivial_ex_atom_bool l kopts nc atom_nc with
- | ExBool_simple -> string "bool"
- | ExBool_val t -> string "Bool(" ^^ if t then string "True)" else string "False)"
- | ExBool_complex ->
+ match simplify_atom_bool l kopts nc atom_nc with
+ | Bool_boring -> string "bool"
+ | Bool_complex (kopts,nc,atom_nc) ->
let var = mk_kid "_bool" in (* TODO collision avoid *)
let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in
braces (separate space
@@ -814,11 +911,11 @@ let is_ctor env id = match Env.lookup_id id env with
| Enum _ -> true
| _ -> false
-let is_auto_decomposed_exist env typ =
+let is_auto_decomposed_exist ctxt env ?(rawbools=false) typ =
let typ = expand_range_type typ in
- match destruct_exist_plain (Env.expand_synonyms env typ) with
- | Some (_, _, typ') -> Some typ'
- | _ -> None
+ match classify_ex_type ctxt env ~rawbools (Env.expand_synonyms env typ) with
+ | ExGeneral, kopts, typ' -> Some (kopts, typ')
+ | ExNone, _, _ -> None
(*Note: vector concatenation, literal vectors, indexed vectors, and record should
be removed prior to pp. The latter two have never yet been seen
@@ -826,9 +923,11 @@ let is_auto_decomposed_exist env typ =
let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, typ) =
let env = env_of_annot (l,annot) in
let typ = Env.expand_synonyms env typ in
- match exists_as_pairs, is_auto_decomposed_exist env typ with
- | true, Some typ' ->
- let pat_pp = doc_pat ctxt true true (pat, typ') in
+ match exists_as_pairs, is_auto_decomposed_exist ctxt env typ with
+ | true, Some (kopts,typ') ->
+ debug ctxt (lazy ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ'));
+ let ctxt' = { ctxt with bound_nvars = List.fold_left (fun s kopt -> KidSet.add (kopt_kid kopt) s) ctxt.bound_nvars kopts } in
+ let pat_pp = doc_pat ctxt' true true (pat, typ') in
let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in
if apat_needed then parens pat_pp else pat_pp
| _ ->
@@ -997,7 +1096,7 @@ let condition_produces_constraint exp =
dependent pair with a proof that the result is the expected integer. This
is redundant for basic arithmetic functions and functions which we unfold
in the constraint solver. *)
-let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"; "length";
+let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "Z.rem"; "length_mword"; "length";
"negb"; "andb"; "orb";
"Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"]
@@ -1014,10 +1113,8 @@ let replace_atom_return_type ret_typ =
| Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),l) ->
let kid = mk_kid "_retval" in (* TODO: collision avoidance *)
Some "build_ex", Typ_aux (Typ_exist ([mk_kopt K_int kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Parse_ast.Generated l)
- (* For informative booleans tweak the type name so that doc_typ knows that the
- constraint should be output. *)
| Typ_aux (Typ_app (Id_aux (Id "atom_bool",il), ([A_aux (A_bool _,_)] as args)),l) ->
- Some "build_Bool", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l)
+ Some "build_ex", ret_typ
| _ -> None, ret_typ
let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) =
@@ -1042,6 +1139,33 @@ let is_prefix s s' =
String.length s' >= l &&
String.sub s' 0 l = s
+let merge_new_tyvars ctxt old_env pat new_env =
+ let is_new_binding id =
+ match Env.lookup_id ~raw:true id old_env with
+ | Unbound -> true
+ | _ -> false
+ in
+ let new_ids = IdSet.filter is_new_binding (pat_ids pat) in
+ let merge_new_kids id m =
+ let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in
+ debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ ));
+ match destruct_numeric typ, destruct_atom_bool new_env typ with
+ | Some ([],_,Nexp_aux (Nexp_var kid,_)), _
+ | _, Some (NC_aux (NC_var kid,_)) ->
+ begin try
+ let _ = Env.get_typ_var kid old_env in
+ debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env"));
+ m
+ with _ ->
+ debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id));
+ KBindings.add kid id m
+ end
+ | _ ->
+ debug ctxt (lazy (" not suitable type"));
+ m
+ in
+ { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames }
+
let prefix_recordtype = true
let report = Reporting.err_unreachable
let doc_exp, doc_let =
@@ -1068,15 +1192,14 @@ let doc_exp, doc_let =
match destruct_exist_plain typ with
| None -> epp
| Some (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l)) -> begin
- match non_trivial_ex_atom_bool l kopts nc atom_nc with
- | ExBool_simple -> epp
- | ExBool_val t -> wrap_parens (string "build_Bool" ^/^ epp)
- | ExBool_complex -> wrap_parens (string "build_ex" ^/^ epp)
+ match simplify_atom_bool l kopts nc atom_nc with
+ | Bool_boring -> epp
+ | Bool_complex _ -> wrap_parens (string "build_ex" ^/^ epp)
end
| Some _ ->
wrap_parens (string "build_ex" ^/^ epp)
in
- let rec construct_dep_pairs env =
+ let construct_dep_pairs ?(rawbools=false) env =
let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) =
match e,t with
| E_tuple exps, Typ_tup typs
@@ -1085,16 +1208,11 @@ let doc_exp, doc_let =
parens (separate (string ", ") (List.map2 (aux false) exps typs))
| _ ->
let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in
+ debug ctxt (lazy ("Constructing " ^ string_of_exp exp ^ " at type " ^ string_of_typ typ));
let build_ex, out_typ =
- match destruct_exist_plain typ' with
- | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin
- match non_trivial_ex_atom_bool l kopts nc atom_nc with
- | ExBool_simple -> None, t
- | ExBool_val _ -> Some "build_Bool", t
- | ExBool_complex -> Some "build_ex", t
- end
- | Some (_,_,t) -> Some "build_ex", t
- | None -> None, typ'
+ match classify_ex_type ctxt (env_of exp) ~rawbools typ' with
+ | ExNone, _, _ -> None, typ'
+ | ExGeneral, _, typ' -> Some "build_ex", typ'
in
let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in
let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in
@@ -1115,7 +1233,7 @@ let doc_exp, doc_let =
else exp_pp
in match build_ex with
| Some s ->
- let exp_pp = string s ^^ space ^^ exp_pp in
+ let exp_pp = string s ^/^ exp_pp in
if want_parens then parens exp_pp else exp_pp
| None -> exp_pp
in aux
@@ -1197,14 +1315,31 @@ let doc_exp, doc_let =
| E_loop _ ->
raise (report l __POS__ "E_loop should have been rewritten before pretty-printing")
| E_let(leb,e) ->
- let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+ let pat = match leb with LB_aux (LB_val (p,_),_) -> p in
+ let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e) in
+ let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ top_exp new_ctxt false e in
if aexp_needed then parens epp else epp
| E_app(f,args) ->
begin match f with
| Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _)
when effectful (effect_of full_exp) ->
- let call = doc_id (append_id f "M") in
- wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
+ let informative = Util.is_some (is_auto_decomposed_exist ctxt (env_of full_exp) (general_typ_of full_exp)) in
+ let suffix = if informative then "MP" else "M" in
+ let call = doc_id (append_id f suffix) in
+ let doc_arg exp =
+ let epp = expY exp in
+ match is_auto_decomposed_exist ctxt (env_of exp) ~rawbools:true (general_typ_of exp) with
+ | Some _ ->
+ if informative then parens (epp ^^ doc_tannot ctxt (env_of exp) true (general_typ_of exp)) else
+ let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in
+ parens (string proj ^/^ epp)
+ | None ->
+ if informative then parens (string "build_trivial_ex" ^/^ epp)
+ else epp
+ in
+ let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in
+ let epp = if informative then epp ^^ doc_tannot ctxt (env_of full_exp) true (general_typ_of full_exp) else epp in
+ wrap_parens epp
(* temporary hack to make the loop body a function of the temporary variables *)
| Id_aux (Id "None", _) as none -> doc_id_ctor none
| Id_aux (Id "foreach#", _) ->
@@ -1435,21 +1570,22 @@ let doc_exp, doc_let =
let ret_typ_inst =
subst_unifiers inst ret_typ
in
- let packeff,unpack,autocast,projbool =
+ let packeff,unpack,autocast =
let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in
let ann_typ = expand_range_type ann_typ in
let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in
let ret_typ_inst =
if is_no_proof_fn env f then ret_typ_inst
else snd (replace_atom_return_type ret_typ_inst) in
- let () =
+ let () =
debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst));
debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ))
in
let unpack, in_typ =
- match ret_typ_inst with
- | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
- | t1 -> false,t1
+ if is_no_proof_fn env f then false, ret_typ_inst else
+ match classify_ex_type ctxt env ~rawbools:true ret_typ_inst with
+ | ExGeneral, _, t1 -> true,t1
+ | ExNone, _, t1 -> false,t1
in
let pack,out_typ =
match ann_typ with
@@ -1464,23 +1600,17 @@ let doc_exp, doc_let =
Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
not (similar_nexps ctxt env n1 n2)
| _ -> false
- in
- let projbool =
- match in_typ with
- | Typ_aux (Typ_app (Id_aux (Id "atom#bool",_),_),_) -> true
- | _ -> false
- in pack,unpack,autocast,projbool
+ in pack,unpack,autocast
in
let autocast_id, proj_id =
if effectful eff
then "autocast_m", "projT1_m"
else "autocast", "projT1" in
- let epp = if unpack && not (effectful eff) then string proj_id ^^ space ^^ parens epp else epp in
- let epp = if projbool && not (effectful eff) then string "projBool" ^^ space ^^ parens epp else epp in
+ let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in
let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in
let epp =
if effectful eff && packeff && not unpack
- then string "build_ex_m" ^^ space ^^ parens epp
+ then string "build_ex_m" ^^ break 1 ^^ parens epp
else epp
in
liftR (if aexp_needed then parens (align epp) else epp)
@@ -1545,9 +1675,9 @@ let doc_exp, doc_let =
debug ctxt (lazy (" on expr of type " ^ string_of_typ inner_typ));
debug ctxt (lazy (" where type expected is " ^ string_of_typ outer_typ))
in
- let outer_ex,outer_typ' = classify_ex_type outer_typ in
- let cast_ex,cast_typ' = classify_ex_type cast_typ in
- let inner_ex,inner_typ' = classify_ex_type inner_typ in
+ let outer_ex,_,outer_typ' = classify_ex_type ctxt env outer_typ in
+ let cast_ex,_,cast_typ' = classify_ex_type ctxt env ~rawbools:true cast_typ in
+ let inner_ex,_,inner_typ' = classify_ex_type ctxt env inner_typ in
let autocast =
(* Avoid using helper functions which simplify the nexps *)
is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' &&
@@ -1566,27 +1696,24 @@ let doc_exp, doc_let =
otherwise derive the new type from the old one. *)
if alpha_equivalent env inner_typ cast_typ
then epp
- else string "derive_m" ^^ space ^^ epp
+ else string "derive_m" ^/^ epp
| ExGeneral, ExNone ->
- string "projT1_m" ^^ space ^^ epp
+ string "projT1_m" ^/^ epp
| ExNone, ExGeneral ->
- string "build_ex_m" ^^ space ^^ epp
+ string "build_ex_m" ^/^ epp
| ExNone, ExNone -> epp
else match cast_ex with
- | ExGeneral -> string "build_ex" ^^ space ^^ epp
- | ExBool -> string "build_Bool" ^^ space ^^ epp
+ | ExGeneral -> string "build_ex" ^/^ epp
| ExNone -> epp
in
let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in
let epp =
if effects then
match cast_ex, outer_ex with
- | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp
- | ExBool, ExNone -> string "projBool_m" ^^ space ^^ parens epp
+ | ExGeneral, ExNone -> string "projT1_m" ^/^ parens epp
| _ -> epp
else match cast_ex with
- | ExGeneral -> string "projT1" ^^ space ^^ parens epp
- | ExBool -> string "projBool" ^^ space ^^ parens epp
+ | ExGeneral -> string "projT1" ^/^ parens epp
| ExNone -> epp
in
let epp =
@@ -1676,7 +1803,7 @@ let doc_exp, doc_let =
let only_integers e = expY e in
let epp =
group ((separate space [string "match"; only_integers e; string "with"]) ^/^
- (separate_map (break 1) (doc_case ctxt (typ_of e)) pexps) ^/^
+ (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) (typ_of e)) pexps) ^/^
(string "end")) in
if aexp_needed then parens (align epp) else align epp
| E_try (e, pexps) ->
@@ -1685,7 +1812,7 @@ let doc_exp, doc_let =
let epp =
(* TODO capture avoidance for __catch_val *)
group ((separate space [string try_catch; expY e; string "(fun __catch_val => match __catch_val with "]) ^/^
- (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^
+ (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) exc_typ) pexps) ^/^
(string "end)")) in
if aexp_needed then parens (align epp) else align epp
else
@@ -1708,11 +1835,12 @@ let doc_exp, doc_let =
debug ctxt (lazy ("Internal plet, pattern " ^ string_of_pat pat));
debug ctxt (lazy (" type of e1 " ^ string_of_typ (typ_of e1)))
in
+ let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e2) in
match pat, e1, e2 with
| (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)),
(E_aux (E_assert (assert_e1,assert_e2),_)), _ ->
let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in
- let epp = infix 0 1 (string ">>= fun _ =>") epp (expN e2) in
+ let epp = infix 0 1 (string ">>= fun _ =>") epp (top_exp new_ctxt false e2) in
if aexp_needed then parens (align epp) else align epp
(* Special case because we don't handle variables with nested existentials well yet.
TODO: check that id1 is not used in e2' *)
@@ -1727,45 +1855,60 @@ let doc_exp, doc_let =
let middle =
match pat' with
| P_aux (P_id id,_)
- when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) &&
+ when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) &&
not (is_enum (env_of e1) id) ->
separate space [string ">>= fun"; doc_id id; bigarrow]
| P_aux (P_typ (typ, P_aux (P_id id,_)),_)
- when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) &&
+ when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) &&
not (is_enum (env_of e1) id) ->
separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ ->
separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow]
in
- infix 0 1 middle e1_pp (expN e2')
+ infix 0 1 middle e1_pp (top_exp new_ctxt false e2')
| _ ->
let epp =
let middle =
+ let env1 = env_of e1 in
match pat with
| P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
string ">>"
| P_aux (P_id id,_)
- when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) &&
+ when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) &&
not (is_enum (env_of e1) id) ->
separate space [string ">>= fun"; doc_id id; bigarrow]
| P_aux (P_typ (typ, P_aux (P_id id,_)),_)
- when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) &&
+ when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) &&
not (is_enum (env_of e1) id) ->
separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]
| P_aux (P_typ (typ, P_aux (P_id id,_)),_)
| P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id,_),_),_)),_)
| P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_)
- when not (is_enum (env_of e1) id) ->
+ when not (is_enum env1 id) ->
let full_typ = (expand_range_type typ) in
- let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with
- | ExGeneral, _ ->
+ let binder = match classify_ex_type ctxt env1 (Env.expand_synonyms env1 full_typ) with
+ | ExGeneral, _, _ ->
squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
- | (ExBool | ExNone), _ ->
+ | ExNone, _, _ ->
parens (separate space [doc_id id; colon; doc_typ ctxt typ])
in separate space [string ">>= fun"; binder; bigarrow]
+ | P_aux (P_id id,_) ->
+ let typ = typ_of e1 in
+ let plain_binder = squote ^^ doc_pat ctxt true true (pat, typ_of e1) in
+ let binder = match classify_ex_type ctxt env1 ~binding:id (Env.expand_synonyms env1 typ) with
+ | ExGeneral, _, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') ->
+ squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
+ | ExNone, _, typ' -> begin
+ match typ' with
+ | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) ->
+ squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
+ | _ -> plain_binder
+ end
+ | _ -> plain_binder
+ in separate space [string ">>= fun"; binder; bigarrow]
| _ ->
separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow]
in
- infix 0 1 middle (expY e1) (expN e2)
+ infix 0 1 middle (expY e1) (top_exp new_ctxt false e2)
in
if aexp_needed then parens (align epp) else epp
end
@@ -1779,7 +1922,7 @@ let doc_exp, doc_let =
in
let valpp =
let env = env_of e1 in
- construct_dep_pairs env true e1 ret_typ
+ construct_dep_pairs env true e1 ret_typ ~rawbools:true
in
wrap_parens (align (separate space [string "returnm"; valpp]))
| E_sizeof nexp ->
@@ -1830,13 +1973,13 @@ let doc_exp, doc_let =
(* Prefer simple lets over patterns, because I've found Coq can struggle to
work out return types otherwise *)
| LB_val(P_aux (P_id id,_),e)
- when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) &&
+ when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) (typ_of e)) &&
not (is_enum (env_of e) id) ->
prefix 2 1
(separate space [string "let"; doc_id id; coloneq])
(top_exp ctxt false e)
| LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e)
- when Util.is_none (is_auto_decomposed_exist (env_of e) typ) &&
+ when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) typ) &&
not (is_enum (env_of e) id) ->
prefix 2 1
(separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq])
@@ -1857,10 +2000,11 @@ let doc_exp, doc_let =
else doc_id id in
group (doc_op coloneq fname (top_exp ctxt true e))
- and doc_case ctxt typ = function
+ and doc_case ctxt old_env typ = function
| Pat_aux(Pat_exp(pat,e),_) ->
- group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow])
- (group (top_exp ctxt false e)))
+ let new_ctxt = merge_new_tyvars ctxt old_env pat (env_of e) in
+ group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow])
+ (group (top_exp new_ctxt false e)))
| Pat_aux(Pat_when(_,_,_),(l,_)) ->
raise (Reporting.err_unreachable l __POS__
"guarded pattern expression should have been rewritten before pretty-printing")
@@ -2118,7 +2262,7 @@ let pat_is_plain_binder env (P_aux (p,_)) =
let demote_all_patterns env i (P_aux (p,p_annot) as pat,typ) =
match pat_is_plain_binder env pat with
| Some id ->
- if Util.is_none (is_auto_decomposed_exist env typ)
+ if Util.is_none (is_auto_decomposed_exist empty_ctxt env typ)
then (pat,typ), fun e -> e
else
(P_aux (P_id id, p_annot),typ),
@@ -2241,12 +2385,6 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
| Typ_aux (Typ_fn (arg_typs, ret_typ, eff),_) -> arg_typs, ret_typ, eff
| _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type")
in
- let build_ex, ret_typ = replace_atom_return_type ret_typ in
- let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with
- | ExGeneral, _ -> Some "build_ex"
- | ExBool, _ -> Some "build_Bool"
- | ExNone, _ -> build_ex
- in
let ids_to_avoid = all_ids pexp in
let bound_kids = tyvars_of_typquant tq in
let pat,guard,exp,(l,_) = destruct_pexp pexp in
@@ -2268,15 +2406,23 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
| Rec_aux (Rec_measure _,_) -> true, IdSet.singleton id
| _ -> false, IdSet.empty
in
- let ctxt =
+ let ctxt0 =
{ early_ret = contains_early_return exp;
kid_renames = mk_kid_renames ids_to_avoid kids_used;
kid_id_renames = kid_to_arg_rename;
bound_nvars = bound_kids;
- build_at_return = if effectful eff then build_ex else None;
+ build_at_return = None; (* filled in below *)
recursive_ids = recursive_ids;
debug = List.mem (string_of_id id) (!opt_debug_on)
} in
+ let build_ex, ret_typ = replace_atom_return_type ret_typ in
+ let build_ex = match classify_ex_type ctxt0 env (Env.expand_synonyms env (expand_range_type ret_typ)) with
+ | ExGeneral, _, _ -> Some "build_ex"
+ | ExNone, _, _ -> build_ex
+ in
+ let ctxt = { ctxt0 with
+ build_at_return = if effectful eff then build_ex else None;
+ } in
let () =
debug ctxt (lazy ("Function " ^ string_of_id id));
debug ctxt (lazy (" return type " ^ string_of_typ ret_typ));
@@ -2299,19 +2445,21 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ))
in
match pat_is_plain_binder env pat with
- | Some id ->
- if Util.is_none (is_auto_decomposed_exist env exp_typ) then
- parens (separate space [doc_id id; colon; doc_typ ctxt typ])
- else begin
+ | Some id -> begin
+ match classify_ex_type ctxt env ~binding:id exp_typ with
+ | ExNone, _, typ' ->
+ parens (separate space [doc_id id; colon; doc_typ ctxt typ'])
+ | ExGeneral, _, _ ->
let full_typ = (expand_range_type exp_typ) in
match destruct_exist_plain (Env.expand_synonyms env full_typ) with
| Some ([kopt], NC_aux (NC_true,_),
- Typ_aux (Typ_app (Id_aux (Id "atom",_),
+ Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool" as tyname),_),
[A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_))
when Kid.compare (kopt_kid kopt) kid == 0 ->
- parens (separate space [doc_id id; colon; string "Z"])
+ let coqty = if tyname = "atom" then "Z" else "bool" in
+ parens (separate space [doc_id id; colon; string coqty])
| Some ([kopt], nc,
- Typ_aux (Typ_app (Id_aux (Id "atom",_),
+ Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool"),_),
[A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_))
when Kid.compare (kopt_kid kopt) kid == 0 && not is_measured ->
(used_a_pattern := true;
@@ -2596,6 +2744,9 @@ let rec doc_def unimplemented generic_eq_types def =
| DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point"
| DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings"
| DEF_pragma _ -> empty
+ | DEF_measure (id,_,_) -> unreachable (id_loc id) __POS__
+ ("Termination measure for " ^ string_of_id id ^
+ " should have been rewritten before backend")
let find_exc_typ defs =
let is_exc_typ_def = function
diff --git a/src/rewrites.ml b/src/rewrites.ml
index d4601fa6..0be6825a 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5170,6 +5170,11 @@ let rewrite_defs_ocaml = [
(* ("separate_numbs", rewrite_defs_separate_numbs) *)
]
+let opt_separate_execute = ref false
+
+let if_separate f env defs =
+ if !opt_separate_execute then f env defs else defs
+
let rewrite_defs_c = [
("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
@@ -5196,6 +5201,7 @@ let rewrite_defs_c = [
("simple_assignments", rewrite_simple_assignments);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
+ ("split_execute", if_separate (rewrite_split_fun_constr_pats "execute"));
("exp_lift_assign", rewrite_defs_exp_lift_assign);
("merge_function_clauses", merge_funcls);
("recheck_defs", fun _ -> Optimize.recheck)
diff --git a/src/rewrites.mli b/src/rewrites.mli
index cea227a5..811d52e8 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -59,6 +59,7 @@ val opt_dmono_analysis : int ref
val opt_auto_mono : bool ref
val opt_dall_split_errors : bool ref
val opt_dmono_continue : bool ref
+val opt_separate_execute : bool ref
(* Generate a fresh id with the given prefix *)
val fresh_id : string -> l -> id
diff --git a/src/sail.ml b/src/sail.ml
index a801ad81..eb25f56d 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -135,7 +135,7 @@ let options = Arg.align ([
" pretty print the input to LaTeX");
( "-latex_prefix",
Arg.String (fun prefix -> Latex.opt_prefix := prefix),
- " set a custom prefix for generated LaTeX macro command (default sail)");
+ "<prefix> set a custom prefix for generated LaTeX macro command (default sail)");
( "-latex_full_valspecs",
Arg.Clear Latex.opt_simple_val,
" print full valspecs in LaTeX output");
@@ -151,6 +151,21 @@ let options = Arg.align ([
( "-c_no_main",
Arg.Set C_backend.opt_no_main,
" do not generate the main() function" );
+ ( "-c_no_rts",
+ Arg.Set C_backend.opt_no_rts,
+ " do not include the Sail runtime" );
+ ( "-c_separate_execute",
+ Arg.Set Rewrites.opt_separate_execute,
+ " separate execute scattered function into multiple functions");
+ ( "-c_prefix",
+ Arg.String (fun prefix -> C_backend.opt_prefix := prefix),
+ "<prefix> prefix generated C functions" );
+ ( "-c_extra_params",
+ Arg.String (fun params -> C_backend.opt_extra_params := Some params),
+ "<parameters> generate C functions with additional parameters" );
+ ( "-c_extra_args",
+ Arg.String (fun args -> C_backend.opt_extra_arguments := Some args),
+ "<arguments> supply extra argument to every generated C function call" );
( "-elf",
Arg.String (fun elf -> opt_process_elf := Some elf),
" process an ELF file so that it can be executed by compiled C code");
@@ -428,10 +443,11 @@ let main() =
then
let ast_c = rewrite_ast_c type_envs ast in
let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
- (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization ast_c type_envs) in *)
- (* let ast_c = Spec_analysis.top_sort_defs ast_c in *)
+ (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *)
+ let output_chan = match !opt_file_out with Some f -> open_out (f ^ ".c") | None -> stdout in
Util.opt_warnings := true;
- C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
+ C_backend.compile_ast (C_backend.initial_ctx type_envs) output_chan (!opt_includes_c) ast_c;
+ close_out output_chan
else ());
(if !(opt_print_cgen)
then Cgen_backend.output type_envs ast
@@ -457,7 +473,7 @@ let main() =
begin
try
if not (Sys.is_directory latex_dir) then begin
- prerr_endline ("Failure: latex output directory exists but is not a directory: " ^ latex_dir);
+ prerr_endline ("Failure: latex output location exists and is not a directory: " ^ latex_dir);
exit 1
end
with Sys_error(_) -> Unix.mkdir latex_dir 0o755
diff --git a/src/slice.ml b/src/slice.ml
new file mode 100644
index 00000000..cbf8ee5d
--- /dev/null
+++ b/src/slice.ml
@@ -0,0 +1,194 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Rewriter
+
+type node =
+ (* In the graph we have a node Register that represents the actual
+ register, but functions get only get transitive dependencies on
+ that through Register_read, Register_write, and Register_ref
+ nodes. *)
+ | Register of id
+ | Function of id
+ | Letbind of id
+ | Type of id
+ | Overload of id
+
+let node_id = function
+ | Register id -> id
+ | Function id -> id
+ | Letbind id -> id
+ | Type id -> id
+ | Overload id -> id
+
+let node_kind = function
+ | Register _ -> 0
+ | Function _ -> 1
+ | Letbind _ -> 3
+ | Type _ -> 4
+ | Overload _ -> 5
+
+module Node = struct
+ type t = node
+ let compare n1 n2 =
+ let lex_ord c1 c2 = if c1 = 0 then c2 else c1 in
+ lex_ord (compare (node_kind n1) (node_kind n2)) (Id.compare (node_id n1) (node_id n2))
+end
+
+let node_color cuts =
+ let module NodeSet = Set.Make(Node) in
+ function
+ | node when NodeSet.mem node cuts -> "red"
+ | Register _ -> "lightpink"
+ | Function _ -> "white"
+ | Letbind _ -> "yellow"
+ | Type _ -> "springgreen"
+ | Overload _ -> "peachpuff"
+
+let node_string n = node_id n |> string_of_id |> String.escaped
+
+let edge_color from_node to_node = "black"
+
+let builtins =
+ let open Type_check in
+ IdSet.of_list (List.map fst (Bindings.bindings Env.builtin_typs))
+
+let typ_ids typ =
+ let rec typ_ids (Typ_aux (aux, _)) =
+ match aux with
+ | Typ_var _ | Typ_internal_unknown -> IdSet.empty
+ | Typ_id id -> IdSet.singleton id
+ | Typ_app (id, typs) ->
+ IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map typ_arg_ids typs))
+ | Typ_fn (typs, typ, _) ->
+ IdSet.union (typ_ids typ) (List.fold_left IdSet.union IdSet.empty (List.map typ_ids typs))
+ | Typ_bidir (typ1, typ2) ->
+ IdSet.union (typ_ids typ1) (typ_ids typ2)
+ | Typ_tup typs ->
+ List.fold_left IdSet.union IdSet.empty (List.map typ_ids typs)
+ | Typ_exist (_, _, typ) -> typ_ids typ
+ and typ_arg_ids (A_aux (aux, _)) =
+ match aux with
+ | A_typ typ -> typ_ids typ
+ | _ -> IdSet.empty
+ in
+ IdSet.diff (typ_ids typ) builtins
+
+let add_def_to_graph graph def =
+ let open Type_check in
+ let module G = Graph.Make(Node) in
+ let graph = ref graph in
+
+ let scan_exp self e_aux annot =
+ let env = env_of_annot annot in
+ begin match e_aux with
+ | E_id id ->
+ begin match Env.lookup_id id env with
+ | Register _ -> graph := G.add_edge self (Register id) !graph
+ | _ ->
+ if IdSet.mem id (Env.get_toplevel_lets env) then
+ graph := G.add_edge self (Letbind id) !graph
+ else ()
+ end
+ | E_app (id, _) ->
+ graph := G.add_edge self (Function id) !graph
+ | E_ref id ->
+ graph := G.add_edge self (Register id) !graph
+ | E_cast (typ, _) ->
+ IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
+ | _ -> ()
+ end;
+ E_aux (e_aux, annot)
+ in
+ let rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot) } in
+
+ let rewriters self =
+ { rewriters_base with
+ rewrite_exp = (fun _ -> fold_exp (rw_exp self));
+ rewrite_let = (fun _ -> fold_letbind (rw_exp self));
+ }
+ in
+
+ begin match def with
+ | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _, _), _)) ->
+ graph := G.add_edges (Function id) [] !graph;
+ IdSet.iter (fun typ_id -> graph := G.add_edge (Function id) (Type typ_id) !graph) (typ_ids typ)
+ | DEF_fundef fdef ->
+ let id = id_of_fundef fdef in
+ graph := G.add_edges (Function id) [] !graph;
+ ignore (rewrite_fun (rewriters (Function id)) fdef)
+ | DEF_val (LB_aux (LB_val (pat, exp), _) as lb) ->
+ let ids = pat_ids pat in
+ IdSet.iter (fun id -> graph := G.add_edges (Letbind id) [] !graph) ids;
+ IdSet.iter (fun id -> ignore (rewrite_let (rewriters (Letbind id)) lb)) ids
+ | _ -> ()
+ end;
+ !graph
+
+let rec graph_of_ast (Defs defs) =
+ let module G = Graph.Make(Node) in
+
+ match defs with
+ | def :: defs ->
+ let g = graph_of_ast (Defs defs) in
+ add_def_to_graph g def
+
+ | [] -> G.empty
+
+let dot_of_ast ast =
+ let module G = Graph.Make(Node) in
+ let module NodeSet = Set.Make(Node) in
+ let g = graph_of_ast ast in
+ let roots = NodeSet.of_list (List.map (fun str -> Function (mk_id str)) ["execute_CGetPerm"; "execute_CSeal"]) in
+ let cuts = NodeSet.of_list (List.map (fun str -> Function (mk_id str)) ["readCapReg"; "writeCapReg"; "rGPR"; "wGPR"; "SignalException"]) in
+ let g = G.prune roots cuts g in
+ G.make_dot (node_color cuts) edge_color node_string stdout g
diff --git a/src/specialize.ml b/src/specialize.ml
index 591a415a..19c5df7a 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -59,17 +59,26 @@ let is_typ_ord_arg = function
type specialization = {
is_polymorphic : kinded_id -> bool;
- instantiation_filter : kid -> typ_arg -> bool
+ instantiation_filter : kid -> typ_arg -> bool;
+ extern_filter : (string -> string option) -> bool
}
let typ_ord_specialization = {
is_polymorphic = (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt);
- instantiation_filter = (fun _ -> is_typ_ord_arg)
+ instantiation_filter = (fun _ -> is_typ_ord_arg);
+ extern_filter = (fun _ -> false)
}
let int_specialization = {
is_polymorphic = is_int_kopt;
- instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false)
+ instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false);
+ extern_filter = (fun externs -> match externs "c" with Some _ -> true | None -> false)
+ }
+
+let int_specialization_with_externs = {
+ is_polymorphic = is_int_kopt;
+ instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false);
+ extern_filter = (fun _ -> false)
}
let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
@@ -105,15 +114,15 @@ let fix_instantiation spec instantiation =
for some set of kinded-identifiers, specified by the is_kopt
predicate. For example, polymorphic_functions is_int_kopt will
return all Int-polymorphic functions. *)
-let rec polymorphic_functions is_kopt (Defs defs) =
+let rec polymorphic_functions ctx (Defs defs) =
match defs with
- | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, _, externs), _)) :: defs ->
- let is_polymorphic = List.exists is_kopt (quant_kopts typq) in
- if is_polymorphic then
- IdSet.add id (polymorphic_functions is_kopt (Defs defs))
+ | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, externs, _), _)) :: defs ->
+ let is_polymorphic = List.exists ctx.is_polymorphic (quant_kopts typq) in
+ if is_polymorphic && not (ctx.extern_filter externs) then
+ IdSet.add id (polymorphic_functions ctx (Defs defs))
else
- polymorphic_functions is_kopt (Defs defs)
- | _ :: defs -> polymorphic_functions is_kopt (Defs defs)
+ polymorphic_functions ctx (Defs defs)
+ | _ :: defs -> polymorphic_functions ctx (Defs defs)
| [] -> IdSet.empty
(* When we specialize a function, we need to generate new name. To do
@@ -548,7 +557,13 @@ let reorder_typedefs (Defs defs) =
Defs (List.rev !tdefs @ others)
let specialize_ids spec ids ast =
- let ast = List.fold_left (fun ast id -> specialize_id spec id ast) ast (IdSet.elements ids) in
+ let total = IdSet.cardinal ids in
+ let _, ast =
+ List.fold_left
+ (fun (n, ast) id ->
+ Util.progress "Specializing " (string_of_id id) n total; (n + 1, specialize_id spec id ast))
+ (1, ast) (IdSet.elements ids)
+ in
let ast = reorder_typedefs ast in
let ast, _ = Type_error.check Type_check.initial_env ast in
let ast =
@@ -562,7 +577,7 @@ let rec specialize' n spec ast env =
if n = 0 then
ast, env
else
- let ids = polymorphic_functions spec.is_polymorphic ast in
+ let ids = polymorphic_functions spec ast in
if IdSet.is_empty ids then
ast, env
else
diff --git a/src/specialize.mli b/src/specialize.mli
index 93dec239..6ec8c2aa 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -62,12 +62,15 @@ val typ_ord_specialization : specialization
(** (experimental) specialise Int-kinded definitions *)
val int_specialization : specialization
+(** (experimental) specialise Int-kinded definitions, including externs *)
+val int_specialization_with_externs : specialization
+
(** Returns an IdSet with the function ids that have X-kinded
parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first
argument specifies what X should be - it should be one of:
[is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
or some combination of those. *)
-val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
+val polymorphic_functions : specialization -> 'a defs -> IdSet.t
(** specialize returns an AST with all the Order and Type polymorphism
removed, as well as the environment produced by type checking that
@@ -76,6 +79,8 @@ val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
which case specialize returns the AST unmodified. *)
val specialize : specialization -> tannot defs -> Env.t -> tannot defs * Env.t
+(** specialize' n performs at most n specialization passes. Useful for
+ int_specialization which is not guaranteed to terminate. *)
val specialize' : int -> specialization -> tannot defs -> Env.t -> tannot defs * Env.t
(** return all instantiations of a function id, with the
diff --git a/src/type_check.ml b/src/type_check.ml
index 1923a885..a69d24cf 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -105,6 +105,7 @@ type env =
{ top_val_specs : (typquant * typ) Bindings.t;
defined_val_specs : IdSet.t;
locals : (mut * typ) Bindings.t;
+ top_letbinds : IdSet.t;
union_ids : (typquant * typ) Bindings.t;
registers : (effect * effect * typ) Bindings.t;
variants : (typquant * type_union list) Bindings.t;
@@ -250,6 +251,25 @@ and strip_kinded_id_aux = function
and strip_kind = function
| K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown)
+let rec typ_constraints (Typ_aux (typ_aux, l)) =
+ match typ_aux with
+ | Typ_internal_unknown -> []
+ | Typ_id v -> []
+ | Typ_var kid -> []
+ | Typ_tup typs -> List.concat (List.map typ_constraints typs)
+ | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
+ | Typ_exist (kids, nc, typ) -> typ_constraints typ
+ | Typ_fn (arg_typs, ret_typ, _) ->
+ List.concat (List.map typ_constraints arg_typs) @ typ_constraints ret_typ
+ | Typ_bidir (typ1, typ2) ->
+ typ_constraints typ1 @ typ_constraints typ2
+and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
+ match typ_arg_aux with
+ | A_nexp n -> []
+ | A_typ typ -> typ_constraints typ
+ | A_bool nc -> [nc]
+ | A_order ord -> []
+
let rec typ_nexps (Typ_aux (typ_aux, l)) =
match typ_aux with
| Typ_internal_unknown -> []
@@ -389,6 +409,8 @@ module Env : sig
val get_accessor : id -> id -> t -> typquant * typ * typ * effect
val add_local : id -> mut * typ -> t -> t
val get_locals : t -> (mut * typ) Bindings.t
+ val add_toplevel_lets : IdSet.t -> t -> t
+ val get_toplevel_lets : t -> IdSet.t
val add_variant : id -> typquant * type_union list -> t -> t
val add_scattered_variant : id -> typquant -> t -> t
val add_variant_clause : id -> type_union -> t -> t
@@ -465,6 +487,7 @@ end = struct
{ top_val_specs = Bindings.empty;
defined_val_specs = IdSet.empty;
locals = Bindings.empty;
+ top_letbinds = IdSet.empty;
union_ids = Bindings.empty;
registers = Bindings.empty;
variants = Bindings.empty;
@@ -1035,15 +1058,19 @@ end = struct
| Mutable -> "ref<" ^ string_of_typ typ ^ ">"
let add_local id mtyp env =
- begin
- if not env.allow_bindings then typ_error env (id_loc id) "Bindings are not allowed in this context" else ();
- wf_typ env (snd mtyp);
- if Bindings.mem id env.top_val_specs then
- typ_error env (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
- else ();
- typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp));
- { env with locals = Bindings.add id mtyp env.locals }
- end
+ if not env.allow_bindings then typ_error env (id_loc id) "Bindings are not allowed in this context" else ();
+ wf_typ env (snd mtyp);
+ if Bindings.mem id env.top_val_specs then
+ typ_error env (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
+ else ();
+ typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp));
+ { env with locals = Bindings.add id mtyp env.locals;
+ top_letbinds = IdSet.remove id env.top_letbinds }
+
+ let add_toplevel_lets ids env =
+ { env with top_letbinds = IdSet.union ids env.top_letbinds }
+
+ let get_toplevel_lets env = env.top_letbinds
let add_variant id variant env =
typ_print (lazy (adding ^ "variant " ^ string_of_id id));
@@ -1287,6 +1314,15 @@ let bind_existential l name typ env =
| Some (kids, nc, typ) -> typ, add_existential l kids nc env
| None -> typ, env
+let bind_tuple_existentials l name (Typ_aux (aux, annot) as typ) env =
+ match aux with
+ | Typ_tup typs ->
+ let typs, env =
+ List.fold_right (fun typ (typs, env) -> let typ, env = bind_existential l name typ env in typ :: typs, env) typs ([], env)
+ in
+ Typ_aux (Typ_tup typs, annot), env
+ | _ -> typ, env
+
let destruct_range env typ =
let kopts, constr, (Typ_aux (typ_aux, _)) =
Util.option_default ([], nc_true, typ) (destruct_exist (Env.expand_synonyms env typ))
@@ -1550,6 +1586,8 @@ let merge_uvars l unifiers1 unifiers2 =
KBindings.merge (merge_unifiers l) unifiers1 unifiers2
let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as typ2) =
+ typ_debug (lazy (Util.("Unify type " |> magenta |> clear) ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2
+ ^ " goals " ^ string_of_list ", " string_of_kid (KidSet.elements goals)));
match aux1, aux2 with
| Typ_internal_unknown, _ | _, Typ_internal_unknown
when Env.allow_unknowns env ->
@@ -1557,10 +1595,24 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as
| Typ_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_typ typ2)
+ (* We need special cases for unifying range(n, m), nat, and int vs atom('n) *)
+ | Typ_id int, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id int = "int" -> KBindings.empty
+
+ | Typ_id nat, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id nat = "nat" ->
+ if prove __POS__ env (nc_gteq n (nint 0)) then KBindings.empty
+ else unify_error l (string_of_typ typ2 ^ " must be a natural number")
+
| Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]),
Typ_app (atom, [A_aux (A_nexp m, _)])
when string_of_id range = "range" && string_of_id atom = "atom" ->
- merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m)
+ let n1, n2 = nexp_simp n1, nexp_simp n2 in
+ begin match n1, n2 with
+ | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) ->
+ if prove __POS__ env (nc_and (nc_lteq n1 m) (nc_lteq m n2)) then KBindings.empty
+ else unify_error l (string_of_typ typ1 ^ " is not contained within " ^ string_of_typ typ1)
+ | _, _ ->
+ merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m)
+ end
| Typ_app (id1, args1), Typ_app (id2, args2) when List.length args1 = List.length args2 && Id.compare id1 id2 = 0 ->
List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2)
@@ -1776,7 +1828,7 @@ and ambiguous_nexp_vars (Nexp_aux (aux, _)) =
let destruct_atom_nexp env typ =
match Env.expand_synonyms env typ with
| Typ_aux (Typ_app (f, [A_aux (A_nexp n, _)]), _)
- when string_of_id f = "atom" -> Some n
+ when string_of_id f = "atom" || string_of_id f = "implicit" -> Some n
| Typ_aux (Typ_app (f, [A_aux (A_nexp n, _); A_aux (A_nexp m, _)]), _)
when string_of_id f = "range" && nexp_identical n m -> Some n
| _ -> None
@@ -1994,7 +2046,7 @@ let rec subtyp l env typ1 typ2 =
let env = add_existential l kopts nc env in subtyp l env typ1 typ2
| None, Some (kopts, nc, typ2) ->
typ_debug (lazy "Subtype check with unification");
- let typ1 = canonicalize env typ1 in
+ let typ1, env = bind_existential l None (canonicalize env typ1) env in
let env = add_typ_vars l kopts env in
let kids' = KidSet.elements (KidSet.diff (KidSet.of_list (List.map kopt_kid kopts)) (tyvars_of_typ typ2)) in
if not (kids' = []) then typ_error env l "Universally quantified constraint generated" else ();
@@ -2915,6 +2967,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ =
try
typ_debug (lazy ("Coercing unification: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ));
let atyp, env = bind_existential l None (typ_of annotated_exp) env in
+ let atyp, env = bind_tuple_existentials l None atyp env in
annotated_exp, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ atyp, env
with
| Unification_error (_, m) when Env.allow_casts env ->
@@ -3223,13 +3276,15 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _)
| TP_wild, _ -> env
| TP_var kid, _ ->
begin
- match typ_nexps typ with
- | [nexp] ->
+ match typ_nexps typ, typ_constraints typ with
+ | [nexp], [] ->
Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l (mk_kopt K_int kid) env)
- | [] ->
+ | [], [nc] ->
+ Env.add_constraint (nc_and (nc_or (nc_not nc) (nc_var kid)) (nc_or nc (nc_not (nc_var kid)))) (Env.add_typ_var l (mk_kopt K_bool kid) env)
+ | [], [] ->
typ_error env l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to")
- | nexps ->
- typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid)
+ | _, _ ->
+ typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric or boolean expressions. Cannot bind " ^ string_of_kid kid)
end
| TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0 ->
List.fold_left2 bind_typ_pat_arg env tpats typs
@@ -4496,14 +4551,14 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) =
let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in
if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects)
then
- [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], env
+ [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], Env.add_toplevel_lets (pat_ids tpat) env
else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind))
| LB_val (pat, bind) ->
let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in
let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) (typ_of inferred_bind) in
if (BESet.is_empty (effect_set (effect_of inferred_bind)) || !opt_no_effects)
then
- [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
+ [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], Env.add_toplevel_lets (pat_ids tpat) env
else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of inferred_bind))
end
diff --git a/src/type_check.mli b/src/type_check.mli
index ba7521fa..bd4c88dc 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -171,6 +171,8 @@ module Env : sig
up the type without any flow typing modifiers. *)
val lookup_id : ?raw:bool -> id -> t -> typ lvar
+ val get_toplevel_lets : t -> IdSet.t
+
val is_union_constructor : id -> t -> bool
(** Check if the id is both a constructor, and the only constructor of that
@@ -189,7 +191,7 @@ module Env : sig
val expand_constraint_synonyms : t -> n_constraint -> n_constraint
val expand_nexp_synonyms : t -> nexp -> nexp
-
+
val expand_synonyms : t -> typ -> typ
(** Expand type synonyms and remove register annotations (i.e. register<t> -> t)) *)
diff --git a/src/value.ml b/src/value.ml
index 261b0f4e..843a943b 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -343,6 +343,10 @@ let value_modulus = function
| [v1; v2] -> V_int (Sail_lib.modulus (coerce_int v1, coerce_int v2))
| _ -> failwith "value modulus"
+let value_abs_int = function
+ | [v] -> V_int (Big_int.abs (coerce_int v))
+ | _ -> failwith "value abs_int"
+
let value_add_vec_int = function
| [v1; v2] -> mk_vector (Sail_lib.add_vec_int (coerce_bv v1, coerce_int v2))
| _ -> failwith "value add_vec_int"
@@ -668,6 +672,7 @@ let primops =
("shl_int", value_shl_int);
("max_int", value_max_int);
("min_int", value_min_int);
+ ("abs_int", value_abs_int);
("add_vec_int", value_add_vec_int);
("sub_vec_int", value_sub_vec_int);
("add_vec", value_add_vec);
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:26:03 +0000