diff options
Diffstat (limited to 'src')
32 files changed, 2330 insertions, 1200 deletions
diff --git a/src/Makefile b/src/Makefile index 97b87d4b..3e9d6f63 100644 --- a/src/Makefile +++ b/src/Makefile @@ -102,7 +102,7 @@ isail: ast.ml bytecode.ml share_directory.ml sail.native: sail -sail.byte: +sail.byte: ast.ml bytecode.ml share_directory.ml ocamlbuild -use-ocamlfind -cflag -g sail.byte interpreter: lem_interp/interp_ast.lem diff --git a/src/ast_util.ml b/src/ast_util.ml index 2b275f35..fbbe274b 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -708,7 +708,7 @@ let rec string_of_exp (E_aux (exp, _)) = | E_exit exp -> "exit " ^ string_of_exp exp | E_throw exp -> "throw " ^ string_of_exp exp | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs - | E_list xs -> "[||" ^ string_of_list ", " string_of_exp xs ^ "||]" + | E_list xs -> "[|" ^ string_of_list ", " string_of_exp xs ^ "|]" | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> "{ " ^ string_of_exp exp ^ " with " ^ string_of_list "; " string_of_fexp fexps ^ " }" | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml new file mode 100644 index 00000000..96513d7f --- /dev/null +++ b/src/bytecode_util.ml @@ -0,0 +1,471 @@ +(**************************************************************************) +(* 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 Bytecode +open Value2 +open PPrint + +(* Define wrappers for creating bytecode instructions. Each function + uses a counter to assign each instruction a unique identifier. *) + +let instr_counter = ref 0 + +let instr_number () = + let n = !instr_counter in + incr instr_counter; + n + +let idecl ?loc:(l=Parse_ast.Unknown) ctyp id = + I_aux (I_decl (ctyp, id), (instr_number (), l)) + +let ialloc ?loc:(l=Parse_ast.Unknown) ctyp id = + I_aux (I_alloc (ctyp, id), (instr_number (), l)) + +let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval = + I_aux (I_init (ctyp, id, cval), (instr_number (), l)) + +let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp = + I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l)) + +let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp = + I_aux (I_funcall (clexp, false, id, cvals, ctyp), (instr_number (), l)) + +let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp = + I_aux (I_funcall (clexp, true, id, cvals, ctyp), (instr_number (), l)) + +let icopy ?loc:(l=Parse_ast.Unknown) clexp cval = + I_aux (I_copy (clexp, cval), (instr_number (), l)) + +let iconvert ?loc:(l=Parse_ast.Unknown) clexp ctyp1 id ctyp2 = + I_aux (I_convert (clexp, ctyp1, id, ctyp2), (instr_number (), l)) + +let iclear ?loc:(l=Parse_ast.Unknown) ctyp id = + I_aux (I_clear (ctyp, id), (instr_number (), l)) + +let ireturn ?loc:(l=Parse_ast.Unknown) cval = + I_aux (I_return cval, (instr_number (), l)) + +let iblock ?loc:(l=Parse_ast.Unknown) instrs = + I_aux (I_block instrs, (instr_number (), l)) + +let itry_block ?loc:(l=Parse_ast.Unknown) instrs = + I_aux (I_try_block instrs, (instr_number (), l)) + +let ithrow ?loc:(l=Parse_ast.Unknown) cval = + I_aux (I_throw cval, (instr_number (), l)) +let icomment ?loc:(l=Parse_ast.Unknown) str = + I_aux (I_comment str, (instr_number (), l)) + +let ilabel ?loc:(l=Parse_ast.Unknown) label = + I_aux (I_label label, (instr_number (), l)) +let igoto ?loc:(l=Parse_ast.Unknown) label = + I_aux (I_goto label, (instr_number (), l)) + +let imatch_failure ?loc:(l=Parse_ast.Unknown) () = + I_aux (I_match_failure, (instr_number (), l)) + +let iraw ?loc:(l=Parse_ast.Unknown) str = + I_aux (I_raw str, (instr_number (), l)) + +let ijump ?loc:(l=Parse_ast.Unknown) cval label = + I_aux (I_jump (cval, label), (instr_number (), l)) + +(**************************************************************************) +(* 1. Instruction pretty printer *) +(**************************************************************************) + +let string_of_value = function + | V_bits bs -> Sail_values.show_bitlist bs ^ "ul" + | V_int i -> Big_int.to_string i ^ "l" + | V_bool true -> "true" + | V_bool false -> "false" + | V_null -> "NULL" + | V_unit -> "UNIT" + | V_bit Sail_values.B0 -> "0ul" + | V_bit Sail_values.B1 -> "1ul" + | V_string str -> "\"" ^ str ^ "\"" + | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str + | _ -> failwith "Cannot convert value to string" + +let rec string_of_fragment ?zencode:(zencode=true) = function + | F_id id when zencode -> Util.zencode_string (string_of_id id) + | F_id id -> string_of_id id + | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id) + | F_ref id -> "&" ^ string_of_id id + | F_lit v -> string_of_value v + | F_call (str, frags) -> + Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags) + | F_field (f, field) -> + Printf.sprintf "%s.%s" (string_of_fragment' ~zencode:zencode f) field + | F_op (f1, op, f2) -> + Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2) + | F_unary (op, f) -> + op ^ string_of_fragment' ~zencode:zencode f + | F_have_exception -> "have_exception" + | F_current_exception -> "(*current_exception)" + | F_raw raw -> raw +and string_of_fragment' ?zencode:(zencode=true) f = + match f with + | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")" + | _ -> string_of_fragment ~zencode:zencode f + +(* String representation of ctyps here is only for debugging and + intermediate language pretty-printer. *) +let rec string_of_ctyp = function + | CT_mpz -> "mpz_t" + | CT_bv true -> "bv_t(dec)" + | CT_bv false -> "bv_t(inc)" + | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)" + | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)" + | CT_int64 -> "int64_t" + | CT_bit -> "bit" + | CT_unit -> "unit" + | CT_bool -> "bool" + | CT_real -> "real" + | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")" + | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id + | CT_string -> "string" + | CT_vector (true, ctyp) -> "vector(dec, " ^ string_of_ctyp ctyp ^ ")" + | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")" + | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")" + | CT_ref ctyp -> "ref(" ^ string_of_ctyp ctyp ^ ")" + +let pp_id id = + string (string_of_id id) + +let pp_ctyp ctyp = + string (string_of_ctyp ctyp |> Util.yellow |> Util.clear) + +let pp_keyword str = + string ((str |> Util.red |> Util.clear) ^ " ") + +let pp_cval (frag, ctyp) = + string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp + +let rec pp_clexp = function + | CL_id id -> pp_id id + | CL_field (id, field) -> pp_id id ^^ string "." ^^ string field + | CL_addr id -> string "*" ^^ pp_id id + | CL_addr_field (id, field) -> pp_id id ^^ string "->" ^^ string field + | CL_current_exception -> string "current_exception" + | CL_have_exception -> string "have_exception" + +let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = + match instr with + | I_decl (ctyp, id) -> + pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | I_if (cval, then_instrs, else_instrs, ctyp) -> + let pp_if_block = function + | [] -> string "{}" + | instrs -> surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace + in + parens (pp_ctyp ctyp) ^^ space + ^^ pp_keyword "if" ^^ pp_cval cval + ^^ if short then + empty + else + pp_keyword " then" ^^ pp_if_block then_instrs + ^^ pp_keyword " else" ^^ pp_if_block else_instrs + | I_jump (cval, label) -> + pp_keyword "jump" ^^ pp_cval cval ^^ space ^^ string (label |> Util.blue |> Util.clear) + | I_block instrs -> + surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace + | I_try_block instrs -> + pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace + | I_alloc (ctyp, id) -> + pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | I_reset (ctyp, id) -> + pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | I_init (ctyp, id, cval) -> + pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval + | I_reinit (ctyp, id, cval) -> + pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval + | I_funcall (x, _, f, args, ctyp2) -> + separate space [ pp_clexp x; string "="; + string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args); + string ":"; pp_ctyp ctyp2 ] + | I_convert (x, ctyp1, y, ctyp2) -> + separate space [ pp_clexp x; colon; pp_ctyp ctyp1; string "="; + pp_keyword "convert" ^^ pp_id y; colon; pp_ctyp ctyp2 ] + | I_copy (clexp, cval) -> + separate space [pp_clexp clexp; string "="; pp_cval cval] + | I_clear (ctyp, id) -> + pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | I_return cval -> + pp_keyword "return" ^^ pp_cval cval + | I_throw cval -> + pp_keyword "throw" ^^ pp_cval cval + | I_comment str -> + string ("// " ^ str |> Util.magenta |> Util.clear) + | I_label str -> + string (str |> Util.blue |> Util.clear) ^^ string ":" + | I_goto str -> + pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear) + | I_match_failure -> + pp_keyword "match_failure" + | I_raw str -> + pp_keyword "C" ^^ string (str |> Util.cyan |> Util.clear) + +let pp_ctype_def = function + | CTD_enum (id, ids) -> + pp_keyword "enum" ^^ pp_id id ^^ string " = " + ^^ separate_map (string " | ") pp_id ids + | CTD_struct (id, fields) -> + pp_keyword "struct" ^^ pp_id id ^^ string " = " + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) fields) rbrace + | CTD_variant (id, ctors) -> + pp_keyword "union" ^^ pp_id id ^^ string " = " + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) ctors) rbrace + +let pp_cdef = function + | CDEF_spec (id, ctyps, ctyp) -> + pp_keyword "val" ^^ pp_id id ^^ string " : " ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp + ^^ hardline + | CDEF_fundef (id, ret, args, instrs) -> + let ret = match ret with + | None -> empty + | Some id -> space ^^ pp_id id + in + pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace + ^^ hardline + | CDEF_reg_dec (id, ctyp) -> + pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + ^^ hardline + | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline + | CDEF_let (n, bindings, instrs, cleanup) -> + let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in + pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr cleanup) rbrace ^^ space + ^^ hardline + | CDEF_startup (id, instrs)-> + pp_keyword "startup" ^^ pp_id id ^^ space + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace + ^^ hardline + | CDEF_finish (id, instrs)-> + pp_keyword "finish" ^^ pp_id id ^^ space + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace + ^^ hardline + +(**************************************************************************) +(* 2. Dependency Graphs *) +(**************************************************************************) + +type graph_node = + | G_id of id + | G_label of string + | G_instr of int * instr + | G_start + +let string_of_node = function + | G_id id -> string_of_id id + | G_label label -> label + | G_instr (n, instr) -> string_of_int n ^ ": " ^ Pretty_print_sail.to_string (pp_instr ~short:true instr) + | G_start -> "START" + +module Node = struct + type t = graph_node + let compare gn1 gn2 = + match gn1, gn2 with + | G_id id1, G_id id2 -> Id.compare id1 id2 + | G_label str1, G_label str2 -> String.compare str1 str2 + | G_instr (n1, _), G_instr (n2, _) -> compare n1 n2 + | G_start , _ -> 1 + | _ , G_start -> -1 + | G_instr _, _ -> 1 + | _ , G_instr _ -> -1 + | G_id _ , _ -> 1 + | _ , G_id _ -> -1 +end + +module NM = Map.Make(Node) +module NS = Set.Make(Node) + +type dep_graph = NS.t NM.t + +let rec fragment_deps = function + | F_id id | F_ref id -> NS.singleton (G_id id) + | F_lit _ -> NS.empty + | F_field (frag, _) | F_unary (_, frag) -> fragment_deps frag + | F_call (_, frags) -> List.fold_left NS.union NS.empty (List.map fragment_deps frags) + | F_op (frag1, _, frag2) -> NS.union (fragment_deps frag1) (fragment_deps frag2) + | F_current_exception -> NS.empty + | F_have_exception -> NS.empty + | F_raw _ -> NS.empty + +let cval_deps = function (frag, _) -> fragment_deps frag + +let rec clexp_deps = function + | CL_id id -> NS.singleton (G_id id) + | CL_field (id, _) -> NS.singleton (G_id id) + | CL_addr id -> NS.singleton (G_id id) + | CL_addr_field (id, _) -> NS.singleton (G_id id) + | CL_have_exception -> NS.empty + | CL_current_exception -> NS.empty + +(** Return the direct, non program-order dependencies of a single + instruction **) +let instr_deps = function + | I_decl (ctyp, id) -> NS.empty, NS.singleton (G_id id) + | I_alloc (ctyp, id) | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id) + | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id) + | I_if (cval, _, _, _) -> cval_deps cval, NS.empty + | I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label) + | I_funcall (clexp, _, _, cvals, _) -> List.fold_left NS.union NS.empty (List.map cval_deps cvals), clexp_deps clexp + | I_convert (clexp, _, id, _) -> NS.singleton (G_id id), clexp_deps clexp + | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp + | I_clear (_, id) -> NS.singleton (G_id id), NS.singleton (G_id id) + | I_throw cval | I_return cval -> cval_deps cval, NS.empty + | I_block _ | I_try_block _ -> NS.empty, NS.empty + | I_comment _ | I_raw _ -> NS.empty, NS.empty + | I_label label -> NS.singleton (G_label label), NS.empty + | I_goto label -> NS.empty, NS.singleton (G_label label) + | I_match_failure -> NS.empty, NS.empty + +let add_link from_node to_node graph = + try + NM.add from_node (NS.add to_node (NM.find from_node graph)) graph + with + | Not_found -> NM.add from_node (NS.singleton to_node) graph + +let leaves graph = + List.fold_left (fun acc (from_node, to_nodes) -> NS.filter (fun to_node -> Node.compare to_node from_node != 0) (NS.union acc to_nodes)) + NS.empty + (NM.bindings graph) + +(* Ensure that all leaves exist in the graph *) +let fix_leaves graph = + NS.fold (fun leaf graph -> if NM.mem leaf graph then graph else NM.add leaf NS.empty graph) (leaves graph) graph + +let instrs_graph instrs = + let icounter = ref 0 in + let graph = ref NM.empty in + + let rec add_instr last_instr (I_aux (instr, _) as iaux) = + incr icounter; + let node = G_instr (!icounter, iaux) in + match instr with + | I_block instrs | I_try_block instrs -> + List.fold_left add_instr last_instr instrs + | I_if (_, then_instrs, else_instrs, _) -> + begin + let inputs, _ = instr_deps instr in (* if has no outputs *) + graph := add_link last_instr node !graph; + NS.iter (fun input -> graph := add_link input node !graph) inputs; + let n1 = List.fold_left add_instr node then_instrs in + let n2 = List.fold_left add_instr node else_instrs in + incr icounter; + let join = G_instr (!icounter, icomment "join") in + graph := add_link n1 join !graph; + graph := add_link n2 join !graph; + join + end + | I_goto label -> + begin + let _, outputs = instr_deps instr in + graph := add_link last_instr node !graph; + NS.iter (fun output -> graph := add_link node output !graph) outputs; + incr icounter; + G_instr (!icounter, icomment "after goto") + end + | _ -> + begin + let inputs, outputs = instr_deps instr in + graph := add_link last_instr node !graph; + NS.iter (fun input -> graph := add_link input node !graph) inputs; + NS.iter (fun output -> graph := add_link node output !graph) outputs; + node + end + in + ignore (List.fold_left add_instr G_start instrs); + fix_leaves !graph + +let make_dot id graph = + Util.opt_colors := false; + let to_string node = String.escaped (string_of_node node) in + let node_color = function + | G_start -> "lightpink" + | G_id _ -> "yellow" + | G_instr (_, I_aux (I_decl _, _)) -> "olivedrab1" + | G_instr (_, I_aux (I_init _, _)) -> "springgreen" + | G_instr (_, I_aux (I_alloc _, _)) -> "palegreen" + | G_instr (_, I_aux (I_clear _, _)) -> "peachpuff" + | G_instr (_, I_aux (I_goto _, _)) -> "orange1" + | G_instr (_, I_aux (I_label _, _)) -> "white" + | G_instr (_, I_aux (I_raw _, _)) -> "khaki" + | G_instr _ -> "azure" + | G_label _ -> "lightpink" + in + let edge_color from_node to_node = + match from_node, to_node with + | G_start , _ -> "goldenrod4" + | G_label _, _ -> "darkgreen" + | _ , G_label _ -> "goldenrod4" + | G_instr _, G_instr _ -> "black" + | G_id _ , G_instr _ -> "blue3" + | G_instr _, G_id _ -> "red3" + | _ , _ -> "coral3" + in + let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") 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; + close_out out_chan diff --git a/src/c_backend.ml b/src/c_backend.ml index 23a8c92e..06e92f3a 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -51,6 +51,7 @@ open Ast open Ast_util open Bytecode +open Bytecode_util open Type_check open PPrint open Value2 @@ -61,13 +62,12 @@ let opt_ddump_flow_graphs = ref false (* Optimization flags *) let optimize_primops = ref false +let optimize_z3 = ref false let optimize_hoist_allocations = ref false -let optimize_struct_undefined = ref false let optimize_struct_updates = ref false -let optimize_enum_undefined = ref false let c_debug str = - if !c_verbosity > 0 then prerr_endline str else () + if !c_verbosity > 0 then prerr_endline (Lazy.force str) else () let c_error ?loc:(l=Parse_ast.Unknown) message = raise (Reporting_basic.err_general l ("\nC backend: " ^ message)) @@ -82,40 +82,6 @@ let lvar_typ = function | Enum typ -> typ | _ -> assert false -let string_of_value = function - | V_bits bs -> Sail_values.show_bitlist bs ^ "ul" - | V_int i -> Big_int.to_string i ^ "l" - | V_bool true -> "true" - | V_bool false -> "false" - | V_null -> "NULL" - | V_unit -> "UNIT" - | V_bit Sail_values.B0 -> "0ul" - | V_bit Sail_values.B1 -> "1ul" - | V_string str -> "\"" ^ str ^ "\"" - | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str - | _ -> failwith "Cannot convert value to string" - -let rec string_of_fragment ?zencode:(zencode=true) = function - | F_id id when zencode -> Util.zencode_string (string_of_id id) - | F_id id -> string_of_id id - | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id) - | F_ref id -> "&" ^ string_of_id id - | F_lit v -> string_of_value v - | F_call (str, frags) -> - Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags) - | F_field (f, field) -> - Printf.sprintf "%s.%s" (string_of_fragment' ~zencode:zencode f) field - | F_op (f1, op, f2) -> - Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2) - | F_unary (op, f) -> - op ^ string_of_fragment' ~zencode:zencode f - | F_have_exception -> "have_exception" - | F_current_exception -> "(*current_exception)" -and string_of_fragment' ?zencode:(zencode=true) f = - match f with - | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")" - | _ -> string_of_fragment ~zencode:zencode f - (**************************************************************************) (* 1. Conversion to A-normal form (ANF) *) (**************************************************************************) @@ -132,21 +98,22 @@ and string_of_fragment' ?zencode:(zencode=true) f = while/until loops). The aexp datatype represents these expressions, while aval represents the trivial values. - The X_aux construct in ast.ml isn't used here, but the typing - information is collapsed into the aexp and aval types. The - convention is that the type of an aexp is given by last argument to - a constructor. It is omitted where it is obvious - for example all - for loops have unit as their type. If some constituent part of the - aexp has an annotation, the it refers to the previous argument, so - in + The convention is that the type of an aexp is given by last + argument to a constructor. It is omitted where it is obvious - for + example all for loops have unit as their type. If some constituent + part of the aexp has an annotation, the it refers to the previous + argument, so in AE_let (id, typ1, _, body, typ2) typ1 is the type of the bound identifer, whereas typ2 is the type of the whole let expression (and therefore also the body). - See Flanagan et al's 'The Essence of Compiling with Continuations' *) -type aexp = + See Flanagan et al's 'The Essence of Compiling with Continuations' + *) +type aexp = AE_aux of aexp_aux * Env.t * l + +and aexp_aux = | AE_val of aval | AE_app of id * aval list * typ | AE_cast of aexp * typ @@ -166,7 +133,9 @@ type aexp = and sc_op = SC_and | SC_or -and apat = +and apat = AP_aux of apat_aux * Env.t * l + +and apat_aux = | AP_tup of apat list | AP_id of id * typ | AP_global of id * typ @@ -191,7 +160,7 @@ let rec frag_rename from_id to_id = function | F_id id when Id.compare id from_id = 0 -> F_id to_id | F_id id -> F_id id | F_ref id when Id.compare id from_id = 0 -> F_ref to_id - | F_ref id -> F_id id + | F_ref id -> F_ref id | F_lit v -> F_lit v | F_have_exception -> F_have_exception | F_current_exception -> F_current_exception @@ -199,8 +168,10 @@ let rec frag_rename from_id to_id = function | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2) | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f) | F_field (f, field) -> F_field (frag_rename from_id to_id f, field) + | F_raw raw -> F_raw raw -let rec apat_bindings = function +let rec apat_bindings (AP_aux (apat_aux, _, _)) = + match apat_aux with | AP_tup apats -> List.fold_left IdSet.union IdSet.empty (List.map apat_bindings apats) | AP_id (id, _) -> IdSet.singleton id | AP_global (id, _) -> IdSet.empty @@ -209,15 +180,18 @@ let rec apat_bindings = function | AP_nil -> IdSet.empty | AP_wild -> IdSet.empty -let rec apat_rename from_id to_id = function - | AP_tup apats -> AP_tup (List.map (apat_rename from_id to_id) apats) - | AP_id (id, typ) when Id.compare id from_id = 0 -> AP_id (to_id, typ) - | AP_id (id, typ) -> AP_id (id, typ) - | AP_global (id, typ) -> AP_global (id, typ) - | AP_app (ctor, apat) -> AP_app (ctor, apat_rename from_id to_id apat) - | AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2) - | AP_nil -> AP_nil - | AP_wild -> AP_wild +let rec apat_rename from_id to_id (AP_aux (apat_aux, env, l)) = + let apat_aux = match apat_aux with + | AP_tup apats -> AP_tup (List.map (apat_rename from_id to_id) apats) + | AP_id (id, typ) when Id.compare id from_id = 0 -> AP_id (to_id, typ) + | AP_id (id, typ) -> AP_id (id, typ) + | AP_global (id, typ) -> AP_global (id, typ) + | AP_app (ctor, apat) -> AP_app (ctor, apat_rename from_id to_id apat) + | AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2) + | AP_nil -> AP_nil + | AP_wild -> AP_wild + in + AP_aux (apat_aux, env, l) let rec aval_rename from_id to_id = function | AV_lit (lit, typ) -> AV_lit (lit, typ) @@ -231,28 +205,30 @@ let rec aval_rename from_id to_id = function | AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ) | AV_C_fragment (fragment, typ) -> AV_C_fragment (frag_rename from_id to_id fragment, typ) -let rec aexp_rename from_id to_id aexp = +let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = let recur = aexp_rename from_id to_id in - match aexp with - | AE_val aval -> AE_val (aval_rename from_id to_id aval) - | AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ) - | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ) - | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ) - | AE_return (aval, typ) -> AE_return (aval_rename from_id to_id aval, typ) - | AE_throw (aval, typ) -> AE_throw (aval_rename from_id to_id aval, typ) - | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval_rename from_id to_id aval, recur then_aexp, recur else_aexp, typ) - | AE_field (aval, id, typ) -> AE_field (aval_rename from_id to_id aval, id, typ) - | AE_case (aval, apexps, typ) -> AE_case (aval_rename from_id to_id aval, List.map (apexp_rename from_id to_id) apexps, typ) - | AE_try (aexp, apexps, typ) -> AE_try (aexp_rename from_id to_id aexp, List.map (apexp_rename from_id to_id) apexps, typ) - | AE_record_update (aval, avals, typ) -> AE_record_update (aval_rename from_id to_id aval, Bindings.map (aval_rename from_id to_id) avals, typ) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when Id.compare from_id to_id = 0 -> AE_for (id, aexp1, aexp2, aexp3, order, aexp4) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, recur aexp1, recur aexp2, recur aexp3, order, recur aexp4) - | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp) + let aexp = match aexp with + | AE_val aval -> AE_val (aval_rename from_id to_id aval) + | AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ) + | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ) + | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp) + | AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ) + | AE_return (aval, typ) -> AE_return (aval_rename from_id to_id aval, typ) + | AE_throw (aval, typ) -> AE_throw (aval_rename from_id to_id aval, typ) + | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval_rename from_id to_id aval, recur then_aexp, recur else_aexp, typ) + | AE_field (aval, id, typ) -> AE_field (aval_rename from_id to_id aval, id, typ) + | AE_case (aval, apexps, typ) -> AE_case (aval_rename from_id to_id aval, List.map (apexp_rename from_id to_id) apexps, typ) + | AE_try (aexp, apexps, typ) -> AE_try (aexp_rename from_id to_id aexp, List.map (apexp_rename from_id to_id) apexps, typ) + | AE_record_update (aval, avals, typ) -> AE_record_update (aval_rename from_id to_id aval, Bindings.map (aval_rename from_id to_id) avals, typ) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when Id.compare from_id to_id = 0 -> AE_for (id, aexp1, aexp2, aexp3, order, aexp4) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, recur aexp1, recur aexp2, recur aexp3, order, recur aexp4) + | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp) + in + AE_aux (aexp, env, l) and apexp_rename from_id to_id (apat, aexp1, aexp2) = if IdSet.mem from_id (apat_bindings apat) then @@ -267,32 +243,41 @@ let new_shadow id = incr shadow_counter; shadow_id -let rec no_shadow ids aexp = - match aexp with - | AE_val aval -> AE_val aval - | AE_app (id, avals, typ) -> AE_app (id, avals, typ) - | AE_cast (aexp, typ) -> AE_cast (no_shadow ids aexp, typ) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, no_shadow ids aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) when IdSet.mem id ids -> - let shadow_id = new_shadow id in - let aexp1 = no_shadow ids aexp1 in - let ids = IdSet.add shadow_id ids in - AE_let (shadow_id, typ1, aexp1, no_shadow ids (aexp_rename id shadow_id aexp2), typ2) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> - AE_let (id, typ1, no_shadow ids aexp1, no_shadow (IdSet.add id ids) aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map (no_shadow ids) aexps, no_shadow ids aexp, typ) - | AE_return (aval, typ) -> AE_return (aval, typ) - | AE_throw (aval, typ) -> AE_throw (aval, typ) - | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval, no_shadow ids then_aexp, no_shadow ids else_aexp, typ) - | AE_field (aval, id, typ) -> AE_field (aval, id, typ) - | AE_case (aval, apexps, typ) -> AE_case (aval, List.map (no_shadow_apexp ids) apexps, typ) - | AE_try (aexp, apexps, typ) -> AE_try (no_shadow ids aexp, List.map (no_shadow_apexp ids) apexps, typ) - | AE_record_update (aval, avals, typ) -> AE_record_update (aval, avals, typ) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> - let ids = IdSet.add id ids in - AE_for (id, no_shadow ids aexp1, no_shadow ids aexp2, no_shadow ids aexp3, order, no_shadow ids aexp4) - | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp) +let rec no_shadow ids (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_val aval -> AE_val aval + | AE_app (id, avals, typ) -> AE_app (id, avals, typ) + | AE_cast (aexp, typ) -> AE_cast (no_shadow ids aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, no_shadow ids aexp) + | AE_let (id, typ1, aexp1, aexp2, typ2) when IdSet.mem id ids -> + let shadow_id = new_shadow id in + let aexp1 = no_shadow ids aexp1 in + let ids = IdSet.add shadow_id ids in + AE_let (shadow_id, typ1, aexp1, no_shadow ids (aexp_rename id shadow_id aexp2), typ2) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> + AE_let (id, typ1, no_shadow ids aexp1, no_shadow (IdSet.add id ids) aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (no_shadow ids) aexps, no_shadow ids aexp, typ) + | AE_return (aval, typ) -> AE_return (aval, typ) + | AE_throw (aval, typ) -> AE_throw (aval, typ) + | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval, no_shadow ids then_aexp, no_shadow ids else_aexp, typ) + | AE_field (aval, id, typ) -> AE_field (aval, id, typ) + | AE_case (aval, apexps, typ) -> AE_case (aval, List.map (no_shadow_apexp ids) apexps, typ) + | AE_try (aexp, apexps, typ) -> AE_try (no_shadow ids aexp, List.map (no_shadow_apexp ids) apexps, typ) + | AE_record_update (aval, avals, typ) -> AE_record_update (aval, avals, typ) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when IdSet.mem id ids -> + let shadow_id = new_shadow id in + let aexp1 = no_shadow ids aexp1 in + let aexp2 = no_shadow ids aexp2 in + let aexp3 = no_shadow ids aexp3 in + let ids = IdSet.add shadow_id ids in + AE_for (shadow_id, aexp1, aexp2, aexp3, order, no_shadow ids (aexp_rename id shadow_id aexp4)) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let ids = IdSet.add id ids in + AE_for (id, no_shadow ids aexp1, no_shadow ids aexp2, no_shadow ids aexp3, order, no_shadow ids aexp4) + | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp) + in + AE_aux (aexp, env, l) and no_shadow_apexp ids (apat, aexp1, aexp2) = let shadows = IdSet.inter (apat_bindings apat) ids in @@ -303,55 +288,58 @@ and no_shadow_apexp ids (apat, aexp1, aexp2) = (rename_apat apat, no_shadow ids (rename aexp1), no_shadow ids (rename aexp2)) (* Map over all the avals in an aexp. *) -let rec map_aval f = function - | AE_val v -> AE_val (f v) - | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_aval f aexp) - | AE_app (id, vs, typ) -> AE_app (id, List.map f vs, typ) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> - AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) - | AE_return (aval, typ) -> AE_return (f aval, typ) - | AE_throw (aval, typ) -> AE_throw (f aval, typ) - | AE_if (aval, aexp1, aexp2, typ2) -> - AE_if (f aval, map_aval f aexp1, map_aval f aexp2, typ2) - | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_aval f aexp1, map_aval f aexp2) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> - AE_for (id, map_aval f aexp1, map_aval f aexp2, map_aval f aexp3, order, map_aval f aexp4) - | AE_record_update (aval, updates, typ) -> - AE_record_update (f aval, Bindings.map f updates, typ) - | AE_field (aval, field, typ) -> - AE_field (f aval, field, typ) - | AE_case (aval, cases, typ) -> - AE_case (f aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) - | AE_try (aexp, cases, typ) -> - AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f aval, map_aval f aexp) +let rec map_aval f (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_val v -> AE_val (f env l v) + | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_aval f aexp) + | AE_app (id, vs, typ) -> AE_app (id, List.map (f env l) vs, typ) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> + AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) + | AE_return (aval, typ) -> AE_return (f env l aval, typ) + | AE_throw (aval, typ) -> AE_throw (f env l aval, typ) + | AE_if (aval, aexp1, aexp2, typ2) -> + AE_if (f env l aval, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_aval f aexp1, map_aval f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_aval f aexp1, map_aval f aexp2, map_aval f aexp3, order, map_aval f aexp4) + | AE_record_update (aval, updates, typ) -> + AE_record_update (f env l aval, Bindings.map (f env l) updates, typ) + | AE_field (aval, field, typ) -> + AE_field (f env l aval, field, typ) + | AE_case (aval, cases, typ) -> + AE_case (f env l aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) + | AE_try (aexp, cases, typ) -> + AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f env l aval, map_aval f aexp) + in + AE_aux (aexp, env, l) (* Map over all the functions in an aexp. *) -let rec map_functions f = function - | AE_app (id, vs, typ) -> f id vs typ - | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) - | AE_if (aval, aexp1, aexp2, typ) -> - AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) - | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_functions f aexp1, map_functions f aexp2) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> - AE_for (id, map_functions f aexp1, map_functions f aexp2, map_functions f aexp3, order, map_functions f aexp4) - | AE_case (aval, cases, typ) -> - AE_case (aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) - | AE_try (aexp, cases, typ) -> - AE_try (map_functions f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) - | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v +let rec map_functions f (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_app (id, vs, typ) -> f env l id vs typ + | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) + | AE_if (aval, aexp1, aexp2, typ) -> + AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_functions f aexp1, map_functions f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_functions f aexp1, map_functions f aexp2, map_functions f aexp3, order, map_functions f aexp4) + | AE_case (aval, cases, typ) -> + AE_case (aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) + | AE_try (aexp, cases, typ) -> + AE_try (map_functions f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) + | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v + in + AE_aux (aexp, env, l) (* For debugging we provide a pretty printer for ANF expressions. *) -let pp_id id = - string (string_of_id id) - let pp_lvar lvar doc = match lvar with | Register typ -> @@ -372,7 +360,8 @@ let pp_order = function | Ord_aux (Ord_dec, _) -> string "dec" | _ -> assert false (* Order types have been specialised, so no polymorphism in C backend. *) -let rec pp_aexp = function +let rec pp_aexp (AE_aux (aexp, _, _)) = + match aexp with | AE_val v -> pp_aval v | AE_cast (aexp, typ) -> pp_annot typ (string "$" ^^ pp_aexp aexp) @@ -387,7 +376,7 @@ let rec pp_aexp = function | AE_let (id, id_typ, binding, body, typ) -> group begin match binding with - | AE_let _ -> + | AE_aux (AE_let _, _, _) -> (pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="]) ^^ hardline ^^ nest 2 (pp_aexp binding)) ^^ hardline ^^ string "in" ^^ space ^^ pp_aexp body @@ -428,7 +417,8 @@ let rec pp_aexp = function ^^ separate (string ", ") (List.map (fun (id, aval) -> pp_id id ^^ string " = " ^^ pp_aval aval) (Bindings.bindings updates))) -and pp_apat = function +and pp_apat (AP_aux (apat_aux, _, _)) = + match apat_aux with | AP_wild -> string "_" | AP_id (id, typ) -> pp_annot typ (pp_id id) | AP_global (id, _) -> pp_id id @@ -481,33 +471,39 @@ let rec split_block = function exp :: exps, last | [] -> c_error "empty block" -let rec anf_pat ?global:(global=false) (P_aux (p_aux, (l, _)) as pat) = +let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = + let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in match p_aux with - | P_id id when global -> AP_global (id, pat_typ_of pat) - | P_id id -> AP_id (id, pat_typ_of pat) - | P_wild -> AP_wild - | P_tup pats -> AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats) - | P_app (id, [pat]) -> AP_app (id, anf_pat ~global:global pat) - | P_app (id, pats) -> AP_app (id, AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)) + | P_id id when global -> mk_apat (AP_global (id, pat_typ_of pat)) + | P_id id -> mk_apat (AP_id (id, pat_typ_of pat)) + | P_wild -> mk_apat AP_wild + | P_tup pats -> mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)) + | P_app (id, [pat]) -> mk_apat (AP_app (id, anf_pat ~global:global pat)) + | P_app (id, pats) -> mk_apat (AP_app (id, mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)))) | P_typ (_, pat) -> anf_pat ~global:global pat | P_var (pat, _) -> anf_pat ~global:global pat - | P_cons (hd_pat, tl_pat) -> AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat) - | P_list pats -> List.fold_right (fun pat apat -> AP_cons (anf_pat ~global:global pat, apat)) pats AP_nil - | _ -> c_error ~loc:l ("Could not convert pattern to ANF: " ^ string_of_pat pat) + | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat)) + | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat AP_nil) + | _ -> c_error ~loc:(fst annot) ("Could not convert pattern to ANF: " ^ string_of_pat pat) -let rec apat_globals = function +let rec apat_globals (AP_aux (aux, _, _)) = + match aux with | AP_nil | AP_wild | AP_id _ -> [] | AP_global (id, typ) -> [(id, typ)] | AP_tup apats -> List.concat (List.map apat_globals apats) | AP_app (_, apat) -> apat_globals apat | AP_cons (hd_apat, tl_apat) -> apat_globals hd_apat @ apat_globals tl_apat -let rec anf (E_aux (e_aux, exp_annot) as exp) = - let to_aval = function +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 + match aexp_aux with | AE_val v -> (v, fun x -> x) - | AE_short_circuit (_, _, _) as aexp -> + | AE_short_circuit (_, _, _) -> let id = gensym () in - (AV_id (id, Local (Immutable, bool_typ)), fun x -> AE_let (id, bool_typ, aexp, x, typ_of exp)) + (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (id, bool_typ, aexp, x, typ_of exp))) | AE_app (_, _, typ) | AE_let (_, _, _, _, typ) | AE_return (_, typ) @@ -517,31 +513,30 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | AE_field (_, _, typ) | AE_case (_, _, typ) | AE_try (_, _, typ) - | AE_record_update (_, _, typ) - as aexp -> + | AE_record_update (_, _, typ) -> let id = gensym () in - (AV_id (id, Local (Immutable, typ)), fun x -> AE_let (id, typ, aexp, x, typ_of exp)) - | AE_assign _ | AE_block _ | AE_for _ | AE_loop _ as aexp -> + (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (id, typ, aexp, x, typ_of exp))) + | AE_assign _ | AE_block _ | AE_for _ | AE_loop _ -> let id = gensym () in - (AV_id (id, Local (Immutable, unit_typ)), fun x -> AE_let (id, unit_typ, aexp, x, typ_of exp)) + (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (id, unit_typ, aexp, x, typ_of exp))) in match e_aux with - | E_lit lit -> ae_lit lit (typ_of exp) + | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) | E_block exps -> let exps, last = split_block exps in let aexps = List.map anf exps in let alast = anf last in - AE_block (aexps, alast, typ_of exp) + mk_aexp (AE_block (aexps, alast, typ_of exp)) | E_assign (LEXP_aux (LEXP_deref dexp, _), exp) -> let gs = gensym () in - AE_let (gs, typ_of dexp, anf dexp, AE_assign (gs, typ_of dexp, anf exp), unit_typ) + mk_aexp (AE_let (gs, typ_of dexp, anf dexp, mk_aexp (AE_assign (gs, typ_of dexp, anf exp)), unit_typ)) | E_assign (LEXP_aux (LEXP_id id, _), exp) - | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> + | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> let aexp = anf exp in - AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp) + mk_aexp (AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp)) | E_assign (lexp, _) -> failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") @@ -549,17 +544,17 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | E_loop (loop_typ, cond, exp) -> let acond = anf cond in let aexp = anf exp in - AE_loop (loop_typ, acond, aexp) + mk_aexp (AE_loop (loop_typ, acond, aexp)) | E_for (id, exp1, exp2, exp3, order, body) -> let aexp1, aexp2, aexp3, abody = anf exp1, anf exp2, anf exp3, anf body in - AE_for (id, aexp1, aexp2, aexp3, order, abody) + mk_aexp (AE_for (id, aexp1, aexp2, aexp3, order, abody)) | E_if (cond, then_exp, else_exp) -> let cond_val, wrap = to_aval (anf cond) in let then_aexp = anf then_exp in let else_aexp = anf else_exp in - wrap (AE_if (cond_val, then_aexp, else_aexp, typ_of then_exp)) + wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of then_exp))) | E_app_infix (x, Id_aux (Id op, l), y) -> anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot)) @@ -570,85 +565,85 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_val (AV_vector (List.map fst avals, typ_of exp))) + wrap (mk_aexp (AE_val (AV_vector (List.map fst avals, typ_of exp)))) | E_list exps -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_val (AV_list (List.map fst avals, typ_of exp))) + wrap (mk_aexp (AE_val (AV_list (List.map fst avals, typ_of exp)))) | E_field (field_exp, id) -> let aval, wrap = to_aval (anf field_exp) in - wrap (AE_field (aval, id, typ_of exp)) + wrap (mk_aexp (AE_field (aval, id, typ_of exp))) | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> - let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = - let aval, wrap = to_aval (anf exp) in - (id, aval), wrap - in - let aval, exp_wrap = to_aval (anf exp) in - let fexps = List.map anf_fexp fexps in - let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in - let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in - exp_wrap (wrap (AE_record_update (aval, record, typ_of exp))) + let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = + let aval, wrap = to_aval (anf exp) in + (id, aval), wrap + in + let aval, exp_wrap = to_aval (anf exp) in + let fexps = List.map anf_fexp fexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in + let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in + exp_wrap (wrap (mk_aexp (AE_record_update (aval, record, typ_of exp)))) | E_app (id, [exp1; exp2]) when string_of_id id = "and_bool" -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap = to_aval aexp1 in - wrap (AE_short_circuit (SC_and, aval1, aexp2)) + wrap (mk_aexp (AE_short_circuit (SC_and, aval1, aexp2))) | E_app (id, [exp1; exp2]) when string_of_id id = "or_bool" -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap = to_aval aexp1 in - wrap (AE_short_circuit (SC_or, aval1, aexp2)) + wrap (mk_aexp (AE_short_circuit (SC_or, aval1, aexp2))) | E_app (id, exps) -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_app (id, List.map fst avals, typ_of exp)) + wrap (mk_aexp (AE_app (id, List.map fst avals, typ_of exp))) | E_throw exn_exp -> let aexp = anf exn_exp in let aval, wrap = to_aval aexp in - wrap (AE_throw (aval, typ_of exp)) + wrap (mk_aexp (AE_throw (aval, typ_of exp))) | E_exit exp -> let aexp = anf exp in let aval, wrap = to_aval aexp in - wrap (AE_app (mk_id "sail_exit", [aval], unit_typ)) + wrap (mk_aexp (AE_app (mk_id "sail_exit", [aval], unit_typ))) | E_return ret_exp -> let aexp = anf ret_exp in let aval, wrap = to_aval aexp in - wrap (AE_return (aval, typ_of exp)) + wrap (mk_aexp (AE_return (aval, typ_of exp))) | E_assert (exp1, exp2) -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ)))) | E_cons (exp1, exp2) -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (AE_app (mk_id "cons", [aval1; aval2], unit_typ))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "cons", [aval1; aval2], unit_typ)))) | E_id id -> let lvar = Env.lookup_id id (env_of exp) in begin match lvar with - | _ -> AE_val (AV_id (id, lvar)) + | _ -> mk_aexp (AE_val (AV_id (id, lvar))) end | E_ref id -> let lvar = Env.lookup_id id (env_of exp) in - AE_val (AV_ref (id, lvar)) + mk_aexp (AE_val (AV_ref (id, lvar))) | E_case (match_exp, pexps) -> let match_aval, match_wrap = to_aval (anf match_exp) in @@ -657,9 +652,9 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | Pat_when (pat, guard, body) -> (anf_pat pat, anf guard, anf body) | Pat_exp (pat, body) -> - (anf_pat pat, AE_val (AV_lit (mk_lit (L_true), bool_typ)), anf body) + (anf_pat pat, mk_aexp (AE_val (AV_lit (mk_lit (L_true), bool_typ))), anf body) in - match_wrap (AE_case (match_aval, List.map anf_pexp pexps, typ_of exp)) + match_wrap (mk_aexp (AE_case (match_aval, List.map anf_pexp pexps, typ_of exp))) | E_try (match_exp, pexps) -> let match_aexp = anf match_exp in @@ -668,16 +663,16 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | Pat_when (pat, guard, body) -> (anf_pat pat, anf guard, anf body) | Pat_exp (pat, body) -> - (anf_pat pat, AE_val (AV_lit (mk_lit (L_true), bool_typ)), anf body) + (anf_pat pat, mk_aexp (AE_val (AV_lit (mk_lit (L_true), bool_typ))), anf body) in - AE_try (match_aexp, List.map anf_pexp pexps, typ_of exp) + mk_aexp (AE_try (match_aexp, List.map anf_pexp pexps, typ_of 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_var (LEXP_aux (LEXP_cast (_, id), _), binding, body) + | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> let env = env_of body in let lvar = Env.lookup_id id env in - AE_let (id, lvar_typ lvar, anf binding, anf body, typ_of exp) + mk_aexp (AE_let (id, lvar_typ lvar, anf binding, anf body, typ_of exp)) | E_var (lexp, _, _) -> failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") @@ -689,7 +684,7 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_val (AV_tuple (List.map fst avals))) + wrap (mk_aexp (AE_val (AV_tuple (List.map fst avals)))) | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = @@ -699,9 +694,9 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let fexps = List.map anf_fexp fexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in - wrap (AE_val (AV_record (record, typ_of exp))) + wrap (mk_aexp (AE_val (AV_record (record, typ_of exp)))) - | E_cast (typ, exp) -> AE_cast (anf exp, typ) + | E_cast (typ, exp) -> mk_aexp (AE_cast (anf exp, typ)) | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ -> (* Should be re-written by type checker *) @@ -738,7 +733,9 @@ type ctx = enums : IdSet.t Bindings.t; variants : (ctyp Bindings.t) Bindings.t; tc_env : Env.t; - letbinds : int list + local_env : Env.t; + letbinds : int list; + recursive_functions : IdSet.t } let initial_ctx env = @@ -746,7 +743,9 @@ let initial_ctx env = enums = Bindings.empty; variants = Bindings.empty; tc_env = env; - letbinds = [] + local_env = env; + letbinds = []; + recursive_functions = IdSet.empty } let rec ctyp_equal ctyp1 ctyp2 = @@ -770,27 +769,6 @@ let rec ctyp_equal ctyp1 ctyp2 = | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_equal ctyp1 ctyp2 | _, _ -> false -(* String representation of ctyps here is only for debugging and - intermediate language pretty-printer. *) -let rec string_of_ctyp = function - | CT_mpz -> "mpz_t" - | CT_bv true -> "bv_t(dec)" - | CT_bv false -> "bv_t(inc)" - | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)" - | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)" - | CT_int64 -> "int64_t" - | CT_bit -> "bit" - | CT_unit -> "unit" - | CT_bool -> "bool" - | CT_real -> "real" - | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")" - | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id - | CT_string -> "string" - | CT_vector (true, ctyp) -> "vector(dec, " ^ string_of_ctyp ctyp ^ ")" - | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")" - | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")" - | CT_ref ctyp -> "ref(" ^ string_of_ctyp ctyp ^ ")" - (** Convert a sail type into a C-type **) let rec ctyp_of_typ ctx typ = let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in @@ -808,6 +786,12 @@ let rec ctyp_of_typ ctx typ = | 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_int64 + | n, m when !optimize_z3 -> + prerr_endline ("optimize atom " ^ string_of_nexp n ^ ", " ^ string_of_nexp m ^ " in context " ^ (Util.string_of_list ", " string_of_n_constraint (Env.get_constraints ctx.local_env))); + if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then + (prerr_endline "yes"; CT_int64) + else + (prerr_endline "no"; CT_mpz) | _ -> CT_mpz end @@ -844,6 +828,18 @@ let rec ctyp_of_typ ctx typ = | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs) + | Typ_exist _ when !optimize_z3 -> + (* Use Type_check.destruct_exist when optimising with z3, to ensure that we + don't cause any type variable clashes in local_env. *) + begin match destruct_exist ctx.local_env typ with + | Some (kids, nc, typ) -> + c_debug (lazy ("optimize existential: " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ + ^ " in context " ^ (Util.string_of_list ", " string_of_n_constraint (Env.get_constraints ctx.local_env)))); + let env = add_existential l kids nc ctx.local_env in + ctyp_of_typ { ctx with local_env = env } typ + | None -> c_error "Existential cannot be destructured. This should be impossible!" + end + | Typ_exist (_, _, typ) -> ctyp_of_typ ctx typ | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ) @@ -900,14 +896,14 @@ let literal_to_fragment (L_aux (l_aux, _) as lit) = | _ -> None let c_literals ctx = - let rec c_literal = function - | AV_lit (lit, typ) as v when is_stack_ctyp (ctyp_of_typ ctx typ) -> + let rec c_literal env l = function + | AV_lit (lit, typ) as v when is_stack_ctyp (ctyp_of_typ { ctx with local_env = env } typ) -> begin match literal_to_fragment lit with | Some frag -> AV_C_fragment (frag, typ) | None -> v end - | AV_tuple avals -> AV_tuple (List.map c_literal avals) + | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals) | v -> v in map_aval c_literal @@ -964,21 +960,39 @@ let c_fragment = function | AV_C_fragment (frag, _) -> frag | _ -> assert false -let analyze_primop' ctx id args typ = +let analyze_primop' ctx env l id args typ = + let ctx = { ctx with local_env = env } in let no_change = AE_app (id, args, typ) in let args = List.map (c_aval ctx) args in let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in (* prerr_endline ("Analysing: " ^ string_of_typ typ ^ " " ^ extern ^ Pretty_print_sail.to_string (separate_map (string ", ") pp_aval args)); *) let v_one = F_lit (V_int (Big_int.of_int 1)) in + let v_int n = F_lit (V_int (Big_int.of_int n)) in match extern, args with | "eq_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "==", v2), typ)) + | "eq_int", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> + AE_val (AV_C_fragment (F_op (v1, "==", v2), typ)) + + (* + | "add_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> + AE_val (AV_C_fragment (F_op (v1, "+", v2), typ)) *) + + | "xor_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> + AE_val (AV_C_fragment (F_op (v1, "^", v2), typ)) + + | "or_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> + AE_val (AV_C_fragment (F_op (v1, "|", v2), typ)) + + | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> + AE_val (AV_C_fragment (F_op (v1, "&", v2), typ)) + | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> let len = F_op (f, "-", F_op (t, "-", v_one)) in - AE_val (AV_C_fragment (F_op (F_op (F_op (v_one, "<<", len), "-", v_one), "&", F_op (vec, ">>", t)), typ)) + AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ)) | "vector_access", [AV_C_fragment (vec, _); AV_C_fragment (n, _)] -> AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ)) @@ -987,7 +1001,7 @@ let analyze_primop' ctx id args typ = AE_val (AV_C_fragment (F_op (a, "==", b), typ)) | "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] -> - AE_val (AV_C_fragment (F_op (F_op (F_op (v_one, "<<", len), "-", v_one), "&", F_op (vec, ">>", start)), typ)) + AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", start)), typ)) | "undefined_bit", _ -> AE_val (AV_C_fragment (F_lit (V_bit Sail_values.B0), typ)) @@ -1022,10 +1036,10 @@ let analyze_primop' ctx id args typ = | _, _ -> no_change -let analyze_primop ctx id args typ = +let analyze_primop ctx env l id args typ = let no_change = AE_app (id, args, typ) in - if !optimize_primops then - try analyze_primop' ctx id args typ with + if !optimize_primops then + try analyze_primop' ctx env l id args typ with | Failure _ -> no_change else no_change @@ -1056,52 +1070,6 @@ let analyze_primop ctx id args typ = expression), cleanup instructions (to deallocate that memory) and possibly typing information about what has been translated. **) -let instr_counter = ref 0 - -let instr_number () = - let n = !instr_counter in - incr instr_counter; - n - -let idecl ?loc:(l=Parse_ast.Unknown) ctyp id = - I_aux (I_decl (ctyp, id), (instr_number (), l)) -let ialloc ?loc:(l=Parse_ast.Unknown) ctyp id = - I_aux (I_alloc (ctyp, id), (instr_number (), l)) -let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval = - I_aux (I_init (ctyp, id, cval), (instr_number (), l)) -let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp = - I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l)) -let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp = - I_aux (I_funcall (clexp, false, id, cvals, ctyp), (instr_number (), l)) -let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp = - I_aux (I_funcall (clexp, true, id, cvals, ctyp), (instr_number (), l)) -let icopy ?loc:(l=Parse_ast.Unknown) clexp cval = - I_aux (I_copy (clexp, cval), (instr_number (), l)) -let iconvert ?loc:(l=Parse_ast.Unknown) clexp ctyp1 id ctyp2 = - I_aux (I_convert (clexp, ctyp1, id, ctyp2), (instr_number (), l)) -let iclear ?loc:(l=Parse_ast.Unknown) ctyp id = - I_aux (I_clear (ctyp, id), (instr_number (), l)) -let ireturn ?loc:(l=Parse_ast.Unknown) cval = - I_aux (I_return cval, (instr_number (), l)) -let iblock ?loc:(l=Parse_ast.Unknown) instrs = - I_aux (I_block instrs, (instr_number (), l)) -let itry_block ?loc:(l=Parse_ast.Unknown) instrs = - I_aux (I_try_block instrs, (instr_number (), l)) -let ithrow ?loc:(l=Parse_ast.Unknown) cval = - I_aux (I_throw cval, (instr_number (), l)) -let icomment ?loc:(l=Parse_ast.Unknown) str = - I_aux (I_comment str, (instr_number (), l)) -let ilabel ?loc:(l=Parse_ast.Unknown) label = - I_aux (I_label label, (instr_number (), l)) -let igoto ?loc:(l=Parse_ast.Unknown) label = - I_aux (I_goto label, (instr_number (), l)) -let imatch_failure ?loc:(l=Parse_ast.Unknown) () = - I_aux (I_match_failure, (instr_number (), l)) -let iraw ?loc:(l=Parse_ast.Unknown) str = - I_aux (I_raw str, (instr_number (), l)) -let ijump ?loc:(l=Parse_ast.Unknown) cval label = - I_aux (I_jump (cval, label), (instr_number (), l)) - let ctype_def_ctyps = function | CTD_enum _ -> [] | CTD_struct (_, fields) -> List.map snd fields @@ -1162,121 +1130,6 @@ let cdef_ctyps ctx = function @ List.concat (List.map instr_ctyps instrs) @ List.concat (List.map instr_ctyps cleanup) -(* For debugging we define a pretty printer for Sail IR instructions *) - -let pp_ctyp ctyp = - string (string_of_ctyp ctyp |> Util.yellow |> Util.clear) - -let pp_keyword str = - string ((str |> Util.red |> Util.clear) ^ " ") - -let pp_cval (frag, ctyp) = string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp - -let rec pp_clexp = function - | CL_id id -> pp_id id - | CL_field (id, field) -> pp_id id ^^ string "." ^^ string field - | CL_addr id -> string "*" ^^ pp_id id - | CL_current_exception -> string "current_exception" - | CL_have_exception -> string "have_exception" - -let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = - match instr with - | I_decl (ctyp, id) -> - pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | I_if (cval, then_instrs, else_instrs, ctyp) -> - let pp_if_block = function - | [] -> string "{}" - | instrs -> surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - in - parens (pp_ctyp ctyp) ^^ space - ^^ pp_keyword "if" ^^ pp_cval cval - ^^ if short then - empty - else - pp_keyword " then" ^^ pp_if_block then_instrs - ^^ pp_keyword " else" ^^ pp_if_block else_instrs - | I_jump (cval, label) -> - pp_keyword "jump" ^^ pp_cval cval ^^ space ^^ string (label |> Util.blue |> Util.clear) - | I_block instrs -> - surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - | I_try_block instrs -> - pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - | I_alloc (ctyp, id) -> - pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | I_reset (ctyp, id) -> - pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | I_init (ctyp, id, cval) -> - pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval - | I_reinit (ctyp, id, cval) -> - pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval - | I_funcall (x, _, f, args, ctyp2) -> - separate space [ pp_clexp x; string "="; - string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args); - string ":"; pp_ctyp ctyp2 ] - | I_convert (x, ctyp1, y, ctyp2) -> - separate space [ pp_clexp x; colon; pp_ctyp ctyp1; string "="; - pp_keyword "convert" ^^ pp_id y; colon; pp_ctyp ctyp2 ] - | I_copy (clexp, cval) -> - separate space [pp_clexp clexp; string "="; pp_cval cval] - | I_clear (ctyp, id) -> - pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | I_return cval -> - pp_keyword "return" ^^ pp_cval cval - | I_throw cval -> - pp_keyword "throw" ^^ pp_cval cval - | I_comment str -> - string ("// " ^ str |> Util.magenta |> Util.clear) - | I_label str -> - string (str |> Util.blue |> Util.clear) ^^ string ":" - | I_goto str -> - pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear) - | I_match_failure -> - pp_keyword "match_failure" - | I_raw str -> - pp_keyword "C" ^^ string (str |> Util.cyan |> Util.clear) - -let pp_ctype_def = function - | CTD_enum (id, ids) -> - pp_keyword "enum" ^^ pp_id id ^^ string " = " - ^^ separate_map (string " | ") pp_id ids - | CTD_struct (id, fields) -> - pp_keyword "struct" ^^ pp_id id ^^ string " = " - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) fields) rbrace - | CTD_variant (id, ctors) -> - pp_keyword "union" ^^ pp_id id ^^ string " = " - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) ctors) rbrace - -let pp_cdef = function - | CDEF_spec (id, ctyps, ctyp) -> - pp_keyword "val" ^^ pp_id id ^^ string " : " ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp - ^^ hardline - | CDEF_fundef (id, ret, args, instrs) -> - let ret = match ret with - | None -> empty - | Some id -> space ^^ pp_id id - in - pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_reg_dec (id, ctyp) -> - pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - ^^ hardline - | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline - | CDEF_let (n, bindings, instrs, cleanup) -> - let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in - pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr cleanup) rbrace ^^ space - ^^ hardline - | CDEF_startup (id, instrs)-> - pp_keyword "startup" ^^ pp_id id ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_finish (id, instrs)-> - pp_keyword "finish" ^^ pp_id id ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - let is_ct_enum = function | CT_enum _ -> true | _ -> false @@ -1493,17 +1346,22 @@ let rec compile_aval ctx = function (F_id gs, CT_list ctyp), [iclear (CT_list ctyp) gs] -let compile_funcall ctx id args typ = +let compile_funcall l ctx id args typ = let setup = ref [] in let cleanup = ref [] in - let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + let quant, Typ_aux (fn_typ, _) = + try Env.get_val_spec id ctx.local_env + with Type_error _ -> + c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env + in let arg_typs, ret_typ = match fn_typ with | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ | _ -> assert false in - let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in let final_ctyp = ctyp_of_typ ctx typ in let setup_arg ctyp aval = @@ -1520,7 +1378,7 @@ let compile_funcall ctx id args typ = cleanup := iclear ctyp gs :: !cleanup; (F_id gs, ctyp) else - c_error ~loc:(id_loc id) + c_error ~loc:l (Printf.sprintf "Failure when setting up function %s arguments: %s and %s." (string_of_id id) (string_of_ctyp have_ctyp) (string_of_ctyp ctyp)) in @@ -1537,15 +1395,20 @@ let compile_funcall ctx id args typ = setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; cleanup := iclear ret_ctyp gs :: !cleanup; fun ret -> iconvert ret final_ctyp gs ret_ctyp + else if is_stack_ctyp ret_ctyp && not (is_stack_ctyp final_ctyp) then + let gs = gensym () in + setup := idecl ret_ctyp gs :: !setup; + setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; + fun ret -> iconvert ret final_ctyp gs ret_ctyp else - assert false + c_error (Printf.sprintf "Funcall call type mismatch between %s and %s" (string_of_ctyp ret_ctyp) (string_of_ctyp final_ctyp)) in (List.rev !setup, final_ctyp, call, !cleanup) -let rec compile_match ctx apat cval case_label = - prerr_endline ("Compiling match " ^ Pretty_print_sail.to_string (pp_apat apat) ^ " cval " ^ Pretty_print_sail.to_string (pp_cval cval)); - match apat, cval with +let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = + let ctx = { ctx with local_env = env } in + match apat_aux, cval with | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], [] @@ -1620,7 +1483,9 @@ let label str = incr label_counter; str -let rec compile_aexp ctx = function +let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = + let ctx = { ctx with local_env = env } in + match aexp_aux with | AE_let (id, _, binding, body, typ) -> let setup, ctyp, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = @@ -1644,7 +1509,7 @@ let rec compile_aexp ctx = function end | AE_app (id, vs, typ) -> - compile_funcall ctx id vs typ + compile_funcall l ctx id vs typ | AE_val aval -> let setup, cval, cleanup = compile_aval ctx aval in @@ -1658,12 +1523,14 @@ let rec compile_aexp ctx = function let finish_match_label = label "finish_match_" in let compile_case (apat, guard, body) = let trivial_guard = match guard with - | AE_val (AV_lit (L_aux (L_true, _), _)) - | AE_val (AV_C_fragment (F_lit (V_bool true), _)) -> true + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _)), _, _) -> true | _ -> false in let case_label = label "case_" in + c_debug (lazy ("Compiling match")); let destructure, destructure_cleanup = compile_match ctx apat cval case_label in + c_debug (lazy ("Compiled match")); let guard_setup, _, guard_call, guard_cleanup = compile_aexp ctx guard in let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in @@ -1697,8 +1564,8 @@ let rec compile_aexp ctx = function let handled_exception_label = label "handled_exception_" in let compile_case (apat, guard, body) = let trivial_guard = match guard with - | AE_val (AV_lit (L_aux (L_true, _), _)) - | AE_val (AV_C_fragment (F_lit (V_bool true), _)) -> true + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _)), _, _) -> true | _ -> false in let try_label = label "try_" in @@ -1719,27 +1586,48 @@ let rec compile_aexp ctx = function in [iblock case_instrs; ilabel try_label] in + assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [icomment "begin try catch"; - idecl ctyp try_return_id], - ctyp, - (fun clexp -> itry_block (aexp_setup @ [aexp_call clexp] @ aexp_cleanup)), - [ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label] + idecl ctyp try_return_id; + itry_block (aexp_setup @ [aexp_call (CL_id try_return_id)] @ aexp_cleanup); + ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label] @ List.concat (List.map compile_case cases) - @ [imatch_failure ()] - @ [ilabel handled_exception_label] - @ [icopy CL_have_exception (F_lit (V_bool false), CT_bool)] + @ [imatch_failure (); + ilabel handled_exception_label; + icopy CL_have_exception (F_lit (V_bool false), CT_bool)], + ctyp, + (fun clexp -> icopy clexp (F_id try_return_id, ctyp)), + [] | AE_if (aval, then_aexp, else_aexp, if_typ) -> let if_ctyp = ctyp_of_typ ctx if_typ in let compile_branch aexp = let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - fun clexp -> setup @ [call clexp] @ cleanup + if ctyp_equal if_ctyp ctyp then + fun clexp -> setup @ [call clexp] @ cleanup + else if is_stack_ctyp ctyp then + fun clexp -> + let gs = gensym() in + setup + @ [idecl ctyp gs; + call (CL_id gs); + iconvert clexp if_ctyp gs ctyp] + @ cleanup + else + fun clexp -> + let gs = gensym () in + setup + @ [idecl ctyp gs; + ialloc ctyp gs; + call (CL_id gs); + iconvert clexp if_ctyp gs ctyp; + iclear ctyp gs] + @ cleanup in - let setup, ctyp, call, cleanup = compile_aexp ctx (AE_val aval) in - let gs = gensym () in - setup @ [idecl ctyp gs; call (CL_id gs)], + let setup, cval, cleanup = compile_aval ctx aval in + setup, if_ctyp, - (fun clexp -> iif (F_id gs, ctyp) + (fun clexp -> iif cval (compile_branch then_aexp clexp) (compile_branch else_aexp clexp) if_ctyp), @@ -1792,8 +1680,9 @@ let rec compile_aexp ctx = function (* This is a faster assignment rule for updating fields of a struct. Turned on by !optimize_struct_updates. *) - | AE_assign (id, assign_typ, AE_record_update (AV_id (rid, _), fields, typ)) + | AE_assign (id, assign_typ, AE_aux (AE_record_update (AV_id (rid, _), fields, typ), _, _)) when Id.compare id rid = 0 && !optimize_struct_updates -> + c_debug (lazy ("Optimizing struct update")); let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup @@ -1869,7 +1758,7 @@ let rec compile_aexp ctx = function let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let unit_gs = gensym () in - let loop_test = (F_unary ("!", F_id gs), CT_bool) in + let loop_test = (F_id gs, CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (body_setup @@ -1888,9 +1777,28 @@ let rec compile_aexp ctx = function | AE_cast (aexp, typ) -> compile_aexp ctx aexp | AE_return (aval, typ) -> + let fn_return_ctyp = match Env.get_ret_typ env with + | Some typ -> ctyp_of_typ ctx typ + | None -> c_error ~loc:l "No function return type found when compiling return statement" + in (* Cleanup info will be re-added by fix_early_return *) let return_setup, cval, _ = compile_aval ctx aval in - return_setup @ [ireturn cval], + let creturn = + if ctyp_equal fn_return_ctyp (cval_ctyp cval) then + [ireturn cval] + else if is_stack_ctyp (cval_ctyp cval) && not (is_stack_ctyp fn_return_ctyp) then + let gs1 = gensym () in + let gs2 = gensym () in + [idecl (cval_ctyp cval) gs1; + icopy (CL_id gs1) cval; + idecl fn_return_ctyp gs2; + ialloc fn_return_ctyp gs2; + iconvert (CL_id gs2) fn_return_ctyp gs1 (cval_ctyp cval); + ireturn (F_id gs2, fn_return_ctyp)] + else + c_error ~loc:l "Can only do return type conversion from stack to heap" + in + return_setup @ creturn, ctyp_of_typ ctx typ, (fun clexp -> icomment "unreachable after return"), [] @@ -1911,10 +1819,62 @@ let rec compile_aexp ctx = function (fun clexp -> icopy clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), cleanup - | AE_for _ -> - [], + | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) -> + (* This is a bit of a hack, we force loop_var to be CT_int64 by + forcing it's type to be a known nexp that will map to + CT_int64. *) + let make_small _ _ = function + | AV_id (id, Local (Immutable, typ)) when Id.compare id loop_var = 0 -> AV_id (id, Local (Immutable, atom_typ (nint 0))) + | aval -> aval + in + let body = map_aval make_small body in + + let is_inc = match ord with + | Ord_inc -> true + | Ord_dec -> false + | Ord_var _ -> c_error "Polymorphic loop direction in C backend" + in + + (* Loop variables *) + let from_setup, from_ctyp, from_call, from_cleanup = compile_aexp ctx loop_from in + let from_gs = gensym () in + let to_setup, to_ctyp, to_call, to_cleanup = compile_aexp ctx loop_to in + let to_gs = gensym () in + let step_setup, step_ctyp, step_call, step_cleanup = compile_aexp ctx loop_step in + let step_gs = gensym () in + let variable_init gs setup ctyp call cleanup = + [idecl CT_int64 gs; + if is_stack_ctyp ctyp then + iblock (setup @ [call (CL_id gs)] @ cleanup) + else + let gs' = gensym () in + iblock (setup + @ [idecl ctyp gs'; ialloc ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs'] + @ cleanup)] + in + + let loop_start_label = label "for_start_" in + let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in + let body_gs = gensym () in + + variable_init from_gs from_setup from_ctyp from_call from_cleanup + @ variable_init to_gs to_setup to_ctyp to_call to_cleanup + @ variable_init step_gs step_setup step_ctyp step_call step_cleanup + @ [iblock ([idecl CT_int64 loop_var; + icopy (CL_id loop_var) (F_id from_gs, CT_int64); + ilabel loop_start_label; + idecl CT_unit body_gs; + iblock (body_setup + @ [body_call (CL_id body_gs)] + @ body_cleanup + @ if is_inc then + [icopy (CL_id loop_var) (F_op (F_id loop_var, "+", F_id step_gs), CT_int64); + ijump (F_op (F_id loop_var, "<=", F_id to_gs), CT_bool) loop_start_label] + else + [icopy (CL_id loop_var) (F_op (F_id loop_var, "-", F_id step_gs), CT_int64); + ijump (F_op (F_id loop_var, ">=", F_id to_gs), CT_bool) loop_start_label])])], CT_unit, - (fun clexp -> icomment "for loop"), + (fun clexp -> icopy clexp unit_fragment), [] (* @@ -2008,7 +1968,7 @@ let fix_early_return ret ctx instrs = | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_return (generate_cleanup (historic @ before)) instrs)] + @ [iblock (rewrite_return (historic @ before) instrs)] @ rewrite_return (historic @ before) after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let historic = historic @ before in @@ -2045,7 +2005,7 @@ let fix_early_stack_return ctx instrs = | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_return (generate_cleanup (historic @ before)) instrs)] + @ [iblock (rewrite_return (historic @ before) instrs)] @ rewrite_return (historic @ before) after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let historic = historic @ before in @@ -2053,9 +2013,8 @@ let fix_early_stack_return ctx instrs = @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp] @ rewrite_return historic after | before, (I_aux (I_return cval, _) as ret) :: after -> - let cleanup_label = label "cleanup_" in - let end_cleanup_label = label "end_cleanup_" in before + @ [icomment "early return cleanup"] @ generate_cleanup (historic @ before) @ [ret] (* There could be jumps into here *) @@ -2080,7 +2039,7 @@ let fix_exception_block ctx instrs = | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_exception (generate_cleanup (historic @ before)) instrs)] + @ [iblock (rewrite_exception (historic @ before) instrs)] @ rewrite_exception (historic @ before) after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let historic = historic @ before in @@ -2166,19 +2125,23 @@ let rec compile_def ctx = function | DEF_reg_dec _ -> failwith "Unsupported register declaration" (* FIXME *) | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> - let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + c_debug (lazy "Compiling VS"); + let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in let arg_typs, ret_typ = match fn_typ with | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ | _ -> assert false in - let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in [CDEF_spec (id, arg_ctyps, ret_ctyp)], ctx | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> + c_debug (lazy ("Compiling function " ^ string_of_id id)); let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)); let setup, ctyp, call, cleanup = compile_aexp ctx aexp in + c_debug (lazy "Compiled aexp"); let fundef_label = label "fundef_fail_" in let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in let arg_typ, ret_typ = match fn_typ with @@ -2215,6 +2178,7 @@ let rec compile_def ctx = function [CDEF_type tdef], ctx | DEF_val (LB_aux (LB_val (pat, exp), _)) -> + c_debug (lazy ("Compiling letbind " ^ string_of_pat pat)); let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let apat = anf_pat ~global:true pat in @@ -2291,178 +2255,7 @@ let add_local_labels instrs = | _ -> assert false (**************************************************************************) -(* 5. Dependency Graphs *) -(**************************************************************************) - -type graph_node = - | G_id of id - | G_label of string - | G_instr of int * instr - | G_start - -let string_of_node = function - | G_id id -> string_of_id id - | G_label label -> label - | G_instr (n, instr) -> string_of_int n ^ ": " ^ Pretty_print_sail.to_string (pp_instr ~short:true instr) - | G_start -> "START" - -module Node = struct - type t = graph_node - let compare gn1 gn2 = - match gn1, gn2 with - | G_id id1, G_id id2 -> Id.compare id1 id2 - | G_label str1, G_label str2 -> String.compare str1 str2 - | G_instr (n1, _), G_instr (n2, _) -> compare n1 n2 - | G_start , _ -> 1 - | _ , G_start -> -1 - | G_instr _, _ -> 1 - | _ , G_instr _ -> -1 - | G_id _ , _ -> 1 - | _ , G_id _ -> -1 -end - -module NM = Map.Make(Node) -module NS = Set.Make(Node) - -type dep_graph = NS.t NM.t - -let rec fragment_deps = function - | F_id id | F_ref id -> NS.singleton (G_id id) - | F_lit _ -> NS.empty - | F_field (frag, _) | F_unary (_, frag) -> fragment_deps frag - | F_call (_, frags) -> List.fold_left NS.union NS.empty (List.map fragment_deps frags) - | F_op (frag1, _, frag2) -> NS.union (fragment_deps frag1) (fragment_deps frag2) - | F_current_exception -> NS.empty - | F_have_exception -> NS.empty - -let cval_deps = function (frag, _) -> fragment_deps frag - -let rec clexp_deps = function - | CL_id id -> NS.singleton (G_id id) - | CL_field (id, _) -> NS.singleton (G_id id) - | CL_addr id -> NS.singleton (G_id id) - | CL_have_exception -> NS.empty - | CL_current_exception -> NS.empty - -(** Return the direct, non program-order dependencies of a single - instruction **) -let instr_deps = function - | I_decl (ctyp, id) -> NS.empty, NS.singleton (G_id id) - | I_alloc (ctyp, id) | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id) - | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id) - | I_if (cval, _, _, _) -> cval_deps cval, NS.empty - | I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label) - | I_funcall (clexp, _, _, cvals, _) -> List.fold_left NS.union NS.empty (List.map cval_deps cvals), clexp_deps clexp - | I_convert (clexp, _, id, _) -> NS.singleton (G_id id), clexp_deps clexp - | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp - | I_clear (_, id) -> NS.singleton (G_id id), NS.singleton (G_id id) - | I_throw cval | I_return cval -> cval_deps cval, NS.empty - | I_block _ | I_try_block _ -> NS.empty, NS.empty - | I_comment _ | I_raw _ -> NS.empty, NS.empty - | I_label label -> NS.singleton (G_label label), NS.empty - | I_goto label -> NS.empty, NS.singleton (G_label label) - | I_match_failure -> NS.empty, NS.empty - -let add_link from_node to_node graph = - try - NM.add from_node (NS.add to_node (NM.find from_node graph)) graph - with - | Not_found -> NM.add from_node (NS.singleton to_node) graph - -let leaves graph = - List.fold_left (fun acc (from_node, to_nodes) -> NS.filter (fun to_node -> Node.compare to_node from_node != 0) (NS.union acc to_nodes)) - NS.empty - (NM.bindings graph) - -(* Ensure that all leaves exist in the graph *) -let fix_leaves graph = - NS.fold (fun leaf graph -> if NM.mem leaf graph then graph else NM.add leaf NS.empty graph) (leaves graph) graph - -let instrs_graph instrs = - let icounter = ref 0 in - let graph = ref NM.empty in - - let rec add_instr last_instr (I_aux (instr, _) as iaux) = - incr icounter; - let node = G_instr (!icounter, iaux) in - match instr with - | I_block instrs | I_try_block instrs -> - List.fold_left add_instr last_instr instrs - | I_if (_, then_instrs, else_instrs, _) -> - begin - let inputs, _ = instr_deps instr in (* if has no outputs *) - graph := add_link last_instr node !graph; - NS.iter (fun input -> graph := add_link input node !graph) inputs; - let n1 = List.fold_left add_instr node then_instrs in - let n2 = List.fold_left add_instr node else_instrs in - incr icounter; - let join = G_instr (!icounter, icomment "join") in - graph := add_link n1 join !graph; - graph := add_link n2 join !graph; - join - end - | I_goto label -> - begin - let _, outputs = instr_deps instr in - graph := add_link last_instr node !graph; - NS.iter (fun output -> graph := add_link node output !graph) outputs; - incr icounter; - G_instr (!icounter, icomment "after goto") - end - | _ -> - begin - let inputs, outputs = instr_deps instr in - graph := add_link last_instr node !graph; - NS.iter (fun input -> graph := add_link input node !graph) inputs; - NS.iter (fun output -> graph := add_link node output !graph) outputs; - node - end - in - ignore (List.fold_left add_instr G_start instrs); - fix_leaves !graph - -let make_dot id graph = - Util.opt_colors := false; - let to_string node = String.escaped (string_of_node node) in - let node_color = function - | G_start -> "lightpink" - | G_id _ -> "yellow" - | G_instr (_, I_aux (I_decl _, _)) -> "olivedrab1" - | G_instr (_, I_aux (I_init _, _)) -> "springgreen" - | G_instr (_, I_aux (I_alloc _, _)) -> "palegreen" - | G_instr (_, I_aux (I_clear _, _)) -> "peachpuff" - | G_instr (_, I_aux (I_goto _, _)) -> "orange1" - | G_instr (_, I_aux (I_label _, _)) -> "white" - | G_instr (_, I_aux (I_raw _, _)) -> "khaki" - | G_instr _ -> "azure" - | G_label _ -> "lightpink" - in - let edge_color from_node to_node = - match from_node, to_node with - | G_start , _ -> "goldenrod4" - | G_label _, _ -> "darkgreen" - | _ , G_label _ -> "goldenrod4" - | G_instr _, G_instr _ -> "black" - | G_id _ , G_instr _ -> "blue3" - | G_instr _, G_id _ -> "red3" - | _ , _ -> "coral3" - in - let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") 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; - close_out out_chan - -(**************************************************************************) -(* 6. Optimizations *) +(* 5. Optimizations *) (**************************************************************************) let clexp_rename from_id to_id = @@ -2471,6 +2264,7 @@ let clexp_rename from_id to_id = | CL_id id -> CL_id (rename id) | CL_field (id, field) -> CL_field (rename id, field) | CL_addr id -> CL_addr (rename id) + | CL_addr_field (id, field) -> CL_addr_field (rename id, field) | CL_current_exception -> CL_current_exception | CL_have_exception -> CL_have_exception @@ -2513,6 +2307,10 @@ let hoist_id () = id let hoist_allocations ctx = function + | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id ctx.recursive_functions -> + c_debug (lazy (Printf.sprintf "skipping recursive function %s" (string_of_id function_id))); + [cdef] + | CDEF_fundef (function_id, heap_return, args, body) -> let decls = ref [] in let cleanups = ref [] in @@ -2610,15 +2408,78 @@ let flatten_instrs ctx = | cdef -> [cdef] +(* When this optimization fires we know we have bytecode of the form + + recreate x : S; x = y; ... + + when this continues with x.A = a, x.B = b etc until y = x. Then + provided there are no further references to x we can eliminate + the variable x. + + Must be called after hoist_allocations, otherwise does nothing. *) +let fix_struct_updates ctx = + (* FIXME need to check no remaining references *) + let rec fix_updates struct_id id = function + | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs + when Id.compare struct_id struct_id' = 0 -> + Util.option_map (fun instrs -> I_aux (I_copy (CL_field (id, field), cval), aux) :: instrs) (fix_updates struct_id id instrs) + | I_aux (I_copy (CL_id id', (F_id struct_id', ctyp)), aux) :: instrs + when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0-> + Some instrs + | _ -> None + in + let rec fix_updates_ret struct_id id = function + | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs + when Id.compare struct_id struct_id' = 0 -> + Util.option_map (fun instrs -> I_aux (I_copy (CL_addr_field (id, field), cval), aux) :: instrs) (fix_updates_ret struct_id id instrs) + | I_aux (I_copy (CL_addr id', (F_id struct_id', ctyp)), aux) :: instrs + when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0-> + Some instrs + | _ -> None + in + let rec opt hr = function + | (I_aux (I_reset (ctyp, struct_id), _) as instr1) + :: (I_aux (I_copy (CL_id struct_id', (F_id id, ctyp')), _) as instr2) + :: instrs + when is_ct_struct ctyp && ctyp_equal ctyp ctyp' && Id.compare struct_id struct_id' = 0 -> + prerr_endline ("Potential struct update " ^ string_of_id struct_id); + begin match fix_updates struct_id id instrs with + | None -> instr1 :: instr2 :: opt hr instrs + | Some updated -> opt hr updated + end + + | (I_aux (I_reset (ctyp, struct_id), _) as instr) :: instrs + when is_ct_struct ctyp && Util.is_some hr -> + let id = match hr with Some id -> id | None -> assert false in + prerr_endline ("Potential struct return " ^ string_of_id struct_id ^ " to " ^ string_of_id id); + begin match fix_updates_ret struct_id id instrs with + | None -> instr :: opt hr instrs + | Some updated -> opt hr updated + end + + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (opt hr block), aux) :: opt hr instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (opt hr block), aux) :: opt hr instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (cval, opt hr then_instrs, opt hr else_instrs, ctyp), aux) :: opt hr instrs + + | instr :: instrs -> instr :: opt hr instrs + | [] -> [] + in + function + | CDEF_fundef (function_id, heap_return, args, body) -> + [CDEF_fundef (function_id, heap_return, args, opt heap_return body)] + | cdef -> [cdef] + let concatMap f xs = List.concat (List.map f xs) let optimize ctx cdefs = let nothing cdefs = cdefs in cdefs - |> if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing + |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing) + |> (if !optimize_struct_updates then concatMap (fix_struct_updates ctx) else nothing) (**************************************************************************) -(* 7. Code generation *) +(* 6. Code generation *) (**************************************************************************) let sgen_id id = Util.zencode_string (string_of_id id) @@ -2678,6 +2539,7 @@ let sgen_clexp = function | CL_id id -> "&" ^ sgen_id id | CL_field (id, field) -> "&(" ^ sgen_id id ^ "." ^ Util.zencode_string field ^ ")" | CL_addr id -> sgen_id id + | CL_addr_field (id, field) -> "&(" ^ sgen_id id ^ "->" ^ Util.zencode_string field ^ ")" | CL_have_exception -> "have_exception" | CL_current_exception -> "current_exception" @@ -2685,6 +2547,7 @@ let sgen_clexp_pure = function | CL_id id -> sgen_id id | CL_field (id, field) -> sgen_id id ^ "." ^ Util.zencode_string field | CL_addr id -> sgen_id id + | CL_addr_field (id, field) -> sgen_id id ^ "->" ^ Util.zencode_string field | CL_have_exception -> "have_exception" | CL_current_exception -> "current_exception" @@ -2760,7 +2623,12 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = | "undefined_vector", _ -> Printf.sprintf "undefined_vector_%s" (sgen_ctyp_name ctyp) | fname, _ -> fname in - if is_stack_ctyp ctyp then + if fname = "reg_deref" then + if is_stack_ctyp ctyp then + string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args) + else + string (Printf.sprintf " set_%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) else string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) @@ -2786,7 +2654,10 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = special conversion code-generator for full generality *) | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 -> let convert i (ctyp1, ctyp2) = - if ctyp_equal ctyp1 ctyp2 then string " /* no change */" + if ctyp_equal ctyp1 ctyp2 then + string (Printf.sprintf " %s.ztup%i = %s.ztup%i;" (sgen_clexp_pure x) i (sgen_id y) i) + else if ctyp_equal ctyp1 ctyp2 then + c_error "heap tuple type conversion" else if is_stack_ctyp ctyp1 then string (Printf.sprintf " %s.ztup%i = convert_%s_of_%s(%s.ztup%i);" (sgen_clexp_pure x) @@ -3172,7 +3043,7 @@ let codegen_vector ctx (direction, ctyp) = ^^ string "}" in let internal_vector_update = - string (Printf.sprintf "void internal_vector_update_%s(%s *rop, %s op, const int64_t n, const %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + string (Printf.sprintf "void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) ^^ string (if is_stack_ctyp ctyp then " rop->data[n] = elem;\n" else @@ -3247,13 +3118,14 @@ let codegen_def' ctx = function | CDEF_fundef (id, ret_arg, args, instrs) as def -> if !opt_ddump_flow_graphs then make_dot id (instrs_graph instrs) else (); let instrs = add_local_labels instrs in - let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in let arg_typs, ret_typ = match fn_typ with | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ | _ -> assert false in - let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in if (List.length arg_ctyps <> List.length args) then c_error ~loc:(id_loc id) ("function arguments " ^ Util.string_of_list ", " string_of_id args @@ -3272,22 +3144,12 @@ let codegen_def' ctx = function ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) ^^ hardline in - let instrs = - if !optimize_struct_undefined && is_ct_struct ret_ctyp && Str.string_match (Str.regexp_string "undefined_") (string_of_id id) 0 then - [] - else - instrs - in - let instrs = - if !optimize_enum_undefined && is_ct_enum ret_ctyp && Str.string_match (Str.regexp_string "undefined_") (string_of_id id) 0 then - [] - else - instrs - in function_header + (* ^^ string (Printf.sprintf "{ fprintf(stderr, \"%s \"); " (string_of_id id)) *) ^^ string "{" ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline ^^ string "}" + (* ^^ string "}" *) | CDEF_type ctype_def -> codegen_type_def ctx ctype_def @@ -3341,7 +3203,7 @@ let codegen_def ctx def = let lists = List.map (fun ctyp -> codegen_list ctx (unlist ctyp)) lists in let vectors = List.filter is_ct_vector (cdef_ctyps ctx def) in let vectors = List.map (fun ctyp -> codegen_vector ctx (unvector ctyp)) vectors in - prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); + (* prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); *) concat tups ^^ concat lists ^^ concat vectors @@ -3368,16 +3230,28 @@ let sgen_finish = function let bytecode_ast ctx rewrites (Defs defs) = let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in - let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs; exit_vs])) } in + let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in let cdefs = List.concat (List.rev chunks) in rewrites cdefs +let rec get_recursive_functions (Defs defs) = + match defs with + | DEF_internal_mutrec fundefs :: defs -> + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + | _ :: defs -> get_recursive_functions (Defs defs) + | [] -> IdSet.empty + let compile_ast ctx (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 + let ctx = { ctx with recursive_functions = recursive_functions } in + c_debug (lazy (Util.string_of_list ", " string_of_id (IdSet.elements recursive_functions))); + let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in - let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs; exit_vs])) } in + let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in let cdefs = List.concat (List.rev chunks) in let cdefs = optimize ctx cdefs in @@ -3444,4 +3318,4 @@ let compile_ast ctx (Defs defs) = Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl ^^ postamble) |> print_endline with - Type_error (l, err) -> prerr_endline ("Unexpected type error when compiling to C:\n" ^ string_of_type_error err) + 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/constant_fold.ml b/src/constant_fold.ml new file mode 100644 index 00000000..7a35226e --- /dev/null +++ b/src/constant_fold.ml @@ -0,0 +1,160 @@ +(**************************************************************************) +(* 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 Type_check +open Rewriter + +module StringMap = Map.Make(String);; + +(* Flag controls whether any constant folding will occur. + false = no folding, true = perform constant folding. *) +let optimize_constant_fold = ref false + +let exp_of_value = + let open Value in + function + | V_int n -> mk_lit_exp (L_num n) + | _ -> failwith "No expression for value" + +(* We want to avoid evaluating things like print statements at compile + time, so we remove them from this list of primops we can use when + constant folding. *) +let safe_primops = + List.fold_left + (fun m k -> StringMap.remove k m) + Value.primops + [ "print_endline"; + "prerr_endline"; + "putchar"; + "print_bits"; + "print_int"; + "print_string"; + "prerr_bits"; + "prerr_int"; + "prerr_string"; + "Elf_loader.elf_entry"; + "Elf_loader.elf_tohost" + ] + +let is_literal = function + | E_aux (E_lit _, _) -> true + | _ -> false + +(* Wrapper around interpreter that repeatedly steps until done. *) +let rec run ast frame = + match frame with + | Interpreter.Done (state, v) -> v + | Interpreter.Step _ -> + run ast (Interpreter.eval_frame ast frame) + | Interpreter.Break frame -> + run ast (Interpreter.eval_frame ast frame) + +(** This rewriting pass looks for function applications (E_app) + expressions where every argument is a literal. It passes these + expressions to the OCaml interpreter in interpreter.ml, and + reconstructs the values returned back into expressions which are + then re-typechecked and re-inserted back into the AST. + + We don't use the effect system to decide if expressions are safe to + evaluate, because this ignores I/O, and would force us to ignore + functions that maybe throw exceptions internally but as called are + totally safe. Instead any exceptions during evaluation are caught, + and the original expression is kept. Some causes of this could be: + + - Function tries to read/write register. + - Calls an unsafe primop. + - Throws an exception that isn't caught. + *) + +let rewrite_constant_function_calls' ast = + let lstate, gstate = + Interpreter.initial_state ast safe_primops + in + let gstate = { gstate with Interpreter.allow_registers = false } in + + let rw_funcall e_aux annot = + match e_aux with + | E_app (id, args) when List.for_all is_literal args -> + begin + let initial_monad = Interpreter.return (E_aux (e_aux, annot)) in + try + begin + let v = run ast (Interpreter.Step (lazy "", (lstate, gstate), initial_monad, [])) in + let exp = exp_of_value v in + try Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot) with + | Type_error (l, err) -> + (* A type error here would be unexpected, so don't ignore it! *) + Util.warn ("Type error when folding constants in " + ^ string_of_exp (E_aux (e_aux, annot)) + ^ "\n" ^ Type_error.string_of_type_error err); + E_aux (e_aux, annot) + end + with + (* Otherwise if anything goes wrong when trying to constant + fold, just continue without optimising. *) + | _ -> E_aux (e_aux, annot) + end + + | _ -> E_aux (e_aux, annot) + in + let rw_exp = { + id_exp_alg with + e_aux = (fun (e_aux, annot) -> rw_funcall e_aux annot) + } in + let rw_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) } in + rewrite_defs_base rw_defs ast + +let rewrite_constant_function_calls ast = + if !optimize_constant_fold then + rewrite_constant_function_calls' ast + else + ast diff --git a/src/elf_loader.ml b/src/elf_loader.ml index 02ff072b..d2a0e9b5 100644 --- a/src/elf_loader.ml +++ b/src/elf_loader.ml @@ -60,9 +60,11 @@ let hex_line bs = in String.concat "" (List.mapi hex_char bs) ^ " " ^ String.concat "" (List.map (fun c -> Printf.sprintf "%c" (escape_char c)) bs) -let rec break n = function - | [] -> [] - | (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs) +let break n xs = + let rec helper acc =function + | [] -> List.rev acc + | (_ :: _ as xs) -> helper ([Lem_list.take n xs] @ acc) (Lem_list.drop n xs) + in helper [] xs let print_segment seg = let bs = seg.Elf_interpreted_segment.elf64_segment_body in @@ -121,7 +123,7 @@ let load_segment ?writer:(writer=write_sail_lib) seg = prerr_endline ("Segment base address: " ^ Big_int.to_string base); prerr_endline ("Segment physical address: " ^ Big_int.to_string paddr); print_segment seg; - List.iteri (writer paddr) (List.map int_of_char (Byte_sequence.char_list_of_byte_sequence bs)) + List.iteri (writer paddr) (List.rev_map int_of_char (List.rev (Byte_sequence.char_list_of_byte_sequence bs))) let load_elf ?writer:(writer=write_sail_lib) name = let segments, e_entry, symbol_map = read name in diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index 9eb59319..87c9af39 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -212,3 +212,10 @@ let barrier bk = Barrier bk (Done ()) val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e let footprint _ = Footprint (Done ()) + +(* Define a type synonym that also takes the register state as a type parameter, + in order to make switching to the state monad without changing generated + definitions easier, see also lib/hol/prompt_monad.lem. *) + +type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e +type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 5c6dc593..0f384cab 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -45,12 +45,19 @@ let negate_real r = realNegate r let abs_real r = realAbs r let power_real b e = realPowInteger b e*) +val print_endline : string -> unit +let print_endline _ = () +declare ocaml target_rep function print_endline = `print_endline` + val prerr_endline : string -> unit let prerr_endline _ = () declare ocaml target_rep function prerr_endline = `prerr_endline` val print_int : string -> integer -> unit -let print_int msg i = prerr_endline (msg ^ (stringFromInteger i)) +let print_int msg i = print_endline (msg ^ (stringFromInteger i)) + +val prerr_int : string -> integer -> unit +let prerr_int msg i = prerr_endline (msg ^ (stringFromInteger i)) val putchar : integer -> unit let putchar _ = () @@ -85,7 +92,7 @@ let rec replace bs (n : integer) b' = match bs with if n = 0 then b' :: bs else b :: replace bs (n - 1) b' end -declare {isabelle} termination_argument replace = automatic +declare {isabelle; hol} termination_argument replace = automatic let upper n = n @@ -128,7 +135,7 @@ let rec just_list l = match l with | (_, _) -> Nothing end end -declare {isabelle} termination_argument just_list = automatic +declare {isabelle; hol} termination_argument just_list = automatic lemma just_list_spec: ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) && @@ -267,7 +274,7 @@ let rec nat_of_bools_aux acc bs = match bs with | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs | false :: bs -> nat_of_bools_aux (2 * acc) bs end -declare {isabelle} termination_argument nat_of_bools_aux = automatic +declare {isabelle; hol} termination_argument nat_of_bools_aux = automatic let nat_of_bools bs = nat_of_bools_aux 0 bs val unsigned_of_bools : list bool -> integer @@ -306,7 +313,7 @@ let rec add_one_bool_ignore_overflow_aux bits = match bits with | false :: bits -> true :: bits | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits end -declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = automatic +declare {isabelle; hol} termination_argument add_one_bool_ignore_overflow_aux = automatic let add_one_bool_ignore_overflow bits = List.reverse (add_one_bool_ignore_overflow_aux (List.reverse bits)) @@ -369,7 +376,7 @@ let rec add_one_bit_ignore_overflow_aux bits = match bits with | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits | BU :: bits -> BU :: List.map (fun _ -> BU) bits end -declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic +declare {isabelle; hol} termination_argument add_one_bit_ignore_overflow_aux = automatic let add_one_bit_ignore_overflow bits = List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) @@ -417,7 +424,7 @@ let rec hexstring_of_bits bs = match bs with | [] -> Just [] | _ -> Nothing end -declare {isabelle} termination_argument hexstring_of_bits = automatic +declare {isabelle; hol} termination_argument hexstring_of_bits = automatic let show_bitlist bs = match hexstring_of_bits bs with @@ -630,7 +637,7 @@ let rec byte_chunks bs = match bs with Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest)) | _ -> Nothing end -declare {isabelle} termination_argument byte_chunks = automatic +declare {isabelle; hol} termination_argument byte_chunks = automatic val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte) let bytes_of_bits bs = byte_chunks (bits_of bs) @@ -854,7 +861,7 @@ let rec foreach l vars body = | (x :: xs) -> foreach xs (body x vars) body end -declare {isabelle} termination_argument foreach = automatic +declare {isabelle; hol} termination_argument foreach = automatic val index_list : integer -> integer -> integer -> list integer let rec index_list from to step = diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 61477258..f69f59c1 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -1,33 +1,8 @@ open import Pervasives_extra -(*open import Sail_impl_base*) open import Sail_values -open import Prompt_monad -open import Prompt open import State_monad open import {isabelle} `State_monad_lemmas` -(* State monad wrapper around prompt monad *) - -val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e -let rec liftState ra s = match s with - | (Done a) -> returnS a - | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) - | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v)) - | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v)) - | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v)) - | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) - | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) - | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) - | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k) - | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) - | (Footprint k) -> liftState ra k - | (Barrier _ k) -> liftState ra k - | (Print _ k) -> liftState ra k (* TODO *) - | (Fail descr) -> failS descr - | (Exception e) -> throwS e -end - - val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e let rec iterS_aux i f xs = match xs with | x :: xs -> f i x >>$ iterS_aux (i + 1) f xs @@ -53,6 +28,46 @@ end declare {isabelle} termination_argument foreachS = automatic +val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e +let and_boolS l r = l >>$= (fun l -> if l then r else returnS false) + +val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e +let or_boolS l r = l >>$= (fun l -> if l then returnS true else r) + +val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e +let bool_of_bitU_fail = function + | B0 -> returnS false + | B1 -> returnS true + | BU -> failS "bool_of_bitU" +end + +val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e +let bool_of_bitU_oracleS = function + | B0 -> returnS false + | B1 -> returnS true + | BU -> undefined_boolS () +end + +val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e +let bools_of_bits_oracleS bits = + foreachS bits [] + (fun b bools -> + bool_of_bitU_oracleS b >>$= (fun b -> + returnS (bools ++ [b]))) + +val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e +let of_bits_oracleS bits = + bools_of_bits_oracleS bits >>$= (fun bs -> + returnS (of_bools bs)) + +val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e +let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits) + +val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e +let mword_oracleS () = + bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs -> + returnS (wordFromBitlist bs)) + val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) -> ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e diff --git a/src/gen_lib/state_lifting.lem b/src/gen_lib/state_lifting.lem new file mode 100644 index 00000000..7e569a7e --- /dev/null +++ b/src/gen_lib/state_lifting.lem @@ -0,0 +1,27 @@ +open import Pervasives_extra +open import Sail_values +open import Prompt_monad +open import Prompt +open import State_monad +open import {isabelle} `State_monad_lemmas` + +(* State monad wrapper around prompt monad *) + +val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e +let rec liftState ra s = match s with + | (Done a) -> returnS a + | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) + | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v)) + | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v)) + | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v)) + | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) + | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) + | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) + | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k) + | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) + | (Footprint k) -> liftState ra k + | (Barrier _ k) -> liftState ra k + | (Print _ k) -> liftState ra k (* TODO *) + | (Fail descr) -> failS descr + | (Exception e) -> throwS e +end diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index a2919762..89021890 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -94,12 +94,12 @@ let assert_expS exp msg = if exp then returnS () else failS msg (* For early return, we abuse exceptions by throwing and catching the return value. The exception type is "either 'r 'e", where "Right e" represents a proper exception and "Left r" an early return of value "r". *) -type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e) +type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e) -val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e +val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e let early_returnS r = throwS (Left r) -val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e +val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e let catch_early_returnS m = try_catchS m (function @@ -108,12 +108,12 @@ let catch_early_returnS m = end) (* Lift to monad with early return by wrapping exceptions *) -val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e -let liftSR m = try_catchS m (fun e -> throwS (Right e)) +val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e +let liftRS m = try_catchS m (fun e -> throwS (Right e)) (* Catch exceptions in the presence of early returns *) -val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) -> monadSR 'regs 'a 'r 'e2 -let try_catchSR m h = +val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) -> monadRS 'regs 'a 'r 'e2 +let try_catchRS m h = try_catchS m (function | Left r -> throwS (Left r) diff --git a/src/initial_check.ml b/src/initial_check.ml index 9545ce44..63ff8f57 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -55,6 +55,7 @@ module Big_int = Nat_big_num (* See mli file for details on what these flags do *) let opt_undefined_gen = ref false +let opt_fast_undefined = ref false let opt_magic_hash = ref false let opt_enum_casts = ref false @@ -1137,8 +1138,11 @@ let generate_undefineds vs_ids (Defs defs) = [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) (mk_pat (P_lit (mk_lit L_unit))) - (mk_exp (E_app (mk_id "internal_pick", - [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] + (if !opt_fast_undefined && List.length ids > 0 then + mk_exp (E_id (List.hd ids)) + else + mk_exp (E_app (mk_id "internal_pick", + [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); @@ -1150,7 +1154,10 @@ let generate_undefineds vs_ids (Defs defs) = [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat - (mk_exp (E_app (mk_id "internal_pick", + (if !opt_fast_undefined && List.length tus > 0 then + undefined_tu (List.hd tus) + else + mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map undefined_tu tus))])))]] | _ -> [] in diff --git a/src/initial_check.mli b/src/initial_check.mli index 757959f7..e6b29216 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -51,9 +51,20 @@ open Ast open Ast_util -(* Generate undefined_T functions for every type T *) +(* Generate undefined_T functions for every type T. False by + default. *) val opt_undefined_gen : bool ref +(* Generate faster undefined_T functions. Rather than generating + functions that allow for the undefined values of enums and variants + to be picked at runtime using a RNG or similar, this creates + undefined_T functions for those types that simply return a specific + member of the type chosen at compile time, which is much + faster. These functions don't have the right effects, so the + -no_effects flag may be needed if this is true. False by + default. *) +val opt_fast_undefined : bool ref + (* Allow # in identifiers when set, like the GHC option of the same name *) val opt_magic_hash : bool ref diff --git a/src/interpreter.ml b/src/interpreter.ml index e62fcfc3..00846d73 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -54,7 +54,9 @@ open Value type gstate = { registers : value Bindings.t; + allow_registers : bool; (* For some uses we want to forbid touching any registers. *) boxes : value StringMap.t; + primops : (value list -> value) StringMap.t; letbinds : (Type_check.tannot letbind) list; } @@ -80,16 +82,18 @@ let rec ast_letbinds (Defs defs) = | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs) | _ :: defs -> ast_letbinds (Defs defs) -let initial_gstate ast = +let initial_gstate ast primops = { registers = Bindings.empty; + allow_registers = true; boxes = StringMap.empty; + primops = primops; letbinds = ast_letbinds ast; } let initial_lstate = { locals = Bindings.empty } -let initial_state ast = initial_lstate, initial_gstate ast +let initial_state ast primops = initial_lstate, initial_gstate ast primops let value_of_lit (L_aux (l_aux, _)) = match l_aux with @@ -109,6 +113,14 @@ let value_of_lit (L_aux (l_aux, _)) = Util.string_to_list str |> List.map (fun c -> V_bit (Sail_lib.bin_char c)) |> (fun v -> V_vector v) + | L_real str -> + begin match Util.split_on_char '.' str with + | [whole; frac] -> + let whole = Rational.of_int (int_of_string whole) in + let frac = Rational.div (Rational.of_int (int_of_string frac)) (Rational.of_int (Util.power 10 (String.length frac))) in + V_real (Rational.add whole frac) + | _ -> failwith "could not parse real literal" + end | _ -> failwith "Unimplemented value_of_lit" (* TODO *) let is_value = function @@ -254,7 +266,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp)) | E_loop (While, exp, body) -> wrap (E_if (exp, E_aux (E_block [body; orig_exp], annot), exp_of_value V_unit)) - | E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, orig_exp, exp_of_value V_unit), annot)]) + | E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, exp_of_value V_unit, orig_exp), annot)]) | E_assert (exp, msg) when is_true exp -> wrap unit_exp | E_assert (exp, msg) when is_false exp && is_value msg -> @@ -327,10 +339,15 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = if extern = "reg_deref" then let regname = List.hd evaluated |> value_of_exp |> coerce_ref in gets >>= fun (_, gstate) -> - try return (exp_of_value (Bindings.find (mk_id regname) gstate.registers)) with + try + if gstate.allow_registers + then return (exp_of_value (Bindings.find (mk_id regname) gstate.registers)) + else raise Not_found + with | Not_found -> return (exp_of_value (StringMap.find regname gstate.boxes)) else - let primop = try StringMap.find extern primops with Not_found -> failwith ("No primop " ^ extern) in + gets >>= fun (_, gstate) -> + let primop = try StringMap.find extern gstate.primops with Not_found -> failwith ("No primop " ^ extern) in return (exp_of_value (primop (List.map value_of_exp evaluated))) end | [] -> liftM exp_of_value (call id (List.map value_of_exp evaluated)) @@ -384,7 +401,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_ref id -> gets >>= fun (lstate, gstate) -> - if Bindings.mem id gstate.registers then + if Bindings.mem id gstate.registers && gstate.allow_registers then return (exp_of_value (V_ref (string_of_id id))) else if Bindings.mem id lstate.locals then let b = box_name id in @@ -405,7 +422,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let open Type_check in gets >>= fun (lstate, gstate) -> match Env.lookup_id id (env_of_annot annot) with - | Register _ -> + | Register _ when gstate.allow_registers -> let exp = try exp_of_value (Bindings.find id gstate.registers) with | Not_found -> @@ -420,7 +437,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = return chain | Enum _ -> return (exp_of_value (V_ctor (string_of_id id, []))) - | _ -> failwith ("id " ^ string_of_id id) + | _ -> failwith ("Coudln't find id " ^ string_of_id id) end | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> @@ -484,7 +501,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let open Type_check in gets >>= fun (lstate, gstate) -> match Env.lookup_id id (env_of_annot annot) with - | Register _ -> + | Register _ when gstate.allow_registers -> puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp | Local (Mutable, _) | Unbound -> begin @@ -500,7 +517,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) -> let name = coerce_ref (value_of_exp reference) in gets >>= fun (lstate, gstate) -> - if Bindings.mem (mk_id name) gstate.registers then + if Bindings.mem (mk_id name) gstate.registers && gstate.allow_registers then puts (lstate, { gstate with registers = Bindings.add (mk_id name) (value_of_exp exp) gstate.registers }) >> wrap unit_exp else puts (lstate, { gstate with boxes = StringMap.add name (value_of_exp exp) gstate.boxes }) >> wrap unit_exp @@ -524,11 +541,22 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let v_from = value_of_exp exp_from in let v_to = value_of_exp exp_to in let v_step = value_of_exp exp_step in - begin match value_gt [v_from; v_to] with - | V_bool true -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) - | V_bool false -> - wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_add_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)]) - | _ -> assert false + begin match ord with + | Ord_aux (Ord_inc, _) -> + begin match value_gt [v_from; v_to] with + | V_bool true -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) + | V_bool false -> + wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_add_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)]) + | _ -> assert false + end + | Ord_aux (Ord_dec, _) -> + begin match value_lt [v_from; v_to] with + | V_bool true -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) + | V_bool false -> + wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_sub_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)]) + | _ -> assert false + end + | Ord_aux (Ord_var _, _) -> failwith "Polymorphic order in foreach" end | E_for (id, exp_from, exp_to, exp_step, ord, body) when is_value exp_to && is_value exp_step -> step exp_from >>= fun exp_from' -> wrap (E_for (id, exp_from', exp_to, exp_step, ord, body)) @@ -616,7 +644,7 @@ let stack_state (_, lstate, _) = lstate type frame = | Done of state * value - | Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list + | Step of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (value -> (Type_check.tannot exp) monad)) list | Break of frame let rec eval_frame' ast = function @@ -629,17 +657,17 @@ let rec eval_frame' ast = function (* print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear); *) Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack') | Pure exp', _ -> - let out' = Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp') in + let out' = lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp')) in Step (out', state, step exp', stack) | Yield (Call(id, vals, cont)), _ when string_of_id id = "break" -> let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in let body = exp_of_fundef (get_fundef id ast) arg in - Break (Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)) + Break (Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)) | Yield (Call(id, vals, cont)), _ -> (* print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); *) let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in let body = exp_of_fundef (get_fundef id ast) arg in - Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack) + Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack) | Yield (Gets cont), _ -> eval_frame' ast (Step (out, state, cont state, stack)) | Yield (Puts (state', cont)), _ -> @@ -651,10 +679,9 @@ let rec eval_frame' ast = function | Yield (Assertion_failed msg), _ -> failwith msg | Yield (Exception v), _ -> - print_endline ("Uncaught Exception" |> Util.cyan |> Util.clear); - Done (state, v) + failwith ("Uncaught Exception" |> Util.cyan |> Util.clear) let eval_frame ast frame = try eval_frame' ast frame with | Type_check.Type_error (l, err) -> - raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err)) + raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) diff --git a/src/isail.ml b/src/isail.ml index 5cd23f83..593167f9 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -103,15 +103,15 @@ let sail_logo = let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast) -let interactive_state = ref (initial_state !interactive_ast) +let interactive_state = ref (initial_state !interactive_ast Value.primops) let print_program () = match !current_mode with | Normal -> () | Evaluation (Step (out, _, _, stack)) -> let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in - List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep); - print_endline out + List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline (Lazy.force code); print_endline sep); + print_endline (Lazy.force out) | Evaluation (Done (_, v)) -> print_endline (Value.string_of_value v |> Util.green |> Util.clear) | Evaluation _ -> () @@ -135,6 +135,7 @@ let rec run () = end let rec run_steps n = + print_endline ("step " ^ string_of_int n); match !current_mode with | _ when n <= 0 -> () | Normal -> () @@ -262,7 +263,7 @@ let handle_input' input = let ast, env = Specialize.specialize !interactive_ast !interactive_env in interactive_ast := ast; interactive_env := env; - interactive_state := initial_state !interactive_ast + interactive_state := initial_state !interactive_ast Value.primops | ":pretty" -> print_endline (Pretty_print_sail.to_string (Latex.latex_defs "sail_latex" !interactive_ast)) | ":bytecode" -> @@ -274,7 +275,7 @@ let handle_input' input = let byte_ast = bytecode_ast ctx (fun cdefs -> List.concat (List.map (flatten_instrs ctx) cdefs)) ast in let chan = open_out arg in Util.opt_colors := false; - Pretty_print_sail.pretty_sail chan (separate_map hardline pp_cdef byte_ast); + Pretty_print_sail.pretty_sail chan (separate_map hardline Bytecode_util.pp_cdef byte_ast); Util.opt_colors := true; close_out chan | ":ast" -> @@ -304,13 +305,13 @@ let handle_input' input = let (_, ast, env) = load_files !interactive_env files in let ast = Process_file.rewrite_ast_interpreter ast in interactive_ast := append_ast !interactive_ast ast; - interactive_state := initial_state !interactive_ast; + interactive_state := initial_state !interactive_ast Value.primops; interactive_env := env; vs_ids := Initial_check.val_spec_ids !interactive_ast | ":u" | ":unload" -> interactive_ast := Ast.Defs []; interactive_env := Type_check.initial_env; - interactive_state := initial_state !interactive_ast; + interactive_state := initial_state !interactive_ast Value.primops; vs_ids := Initial_check.val_spec_ids !interactive_ast; (* See initial_check.mli for an explanation of why we need this. *) Initial_check.have_undefined_builtins := false @@ -320,7 +321,7 @@ let handle_input' input = (* An expression in normal mode is type checked, then puts us in evaluation mode. *) let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord str) in - current_mode := Evaluation (eval_frame !interactive_ast (Step ("", !interactive_state, return exp, []))); + current_mode := Evaluation (eval_frame !interactive_ast (Step (lazy "", !interactive_state, return exp, []))); print_program () | Empty -> () end @@ -363,7 +364,7 @@ let handle_input' input = let handle_input input = try handle_input' input with | Type_check.Type_error (l, err) -> - print_endline (Type_check.string_of_type_error err) + print_endline (Type_error.string_of_type_error err) | Reporting_basic.Fatal_error err -> Reporting_basic.print_error err | exn -> diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4f257712..f4f28c41 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -735,7 +735,7 @@ let reduce_cast typ exp l annot = let typ' = Env.base_typ_of env typ in match exp, destruct_exist env typ' with | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> - let nc_env = Env.add_typ_var kid BK_int env in + let nc_env = Env.add_typ_var l kid BK_int env in let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in if prove nc_env nc then exp @@ -3729,6 +3729,7 @@ let rewrite_app env typ (id,args) = let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in let is_zeros = is_id env (Id "Zeros") in + let is_ones = is_id env (Id "Ones") in match args with | (E_aux (E_app (append1, [E_aux (E_app (subrange1, [vector1; start1; end1]), _); @@ -3757,7 +3758,8 @@ let rewrite_app env typ (id,args) = E_app (mk_id "zext_slice", [vector1; start1; length1]) | [E_aux (E_app (ones, [len1]),_); - _ (* unnecessary ZeroExtend length *)] -> + _ (* unnecessary ZeroExtend length *)] + when is_ones ones -> E_app (mk_id "zext_ones", [len1]) | _ -> E_app (id,args) @@ -3975,6 +3977,9 @@ let add_bitvector_casts (Defs defs) = end | E_return e' -> E_aux (E_return (make_bitvector_cast_exp top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann) + (* TODO: (env_of_annot ann) isn't suitable, because it contains + constraints revealing the case splits involved; needs a more + subtle approach *) | E_assign (LEXP_aux (lexp,lexp_annot),e') -> E_aux (E_assign (LEXP_aux (lexp,lexp_annot), make_bitvector_cast_exp (env_of_annot ann) quant_kids (fill_in_type (env_of e') (typ_of e')) @@ -3987,7 +3992,8 @@ let add_bitvector_casts (Defs defs) = e_aux = rewrite_aux } exp in let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann)) = - let (tq,typ) = Env.get_val_spec_orig id (env_of_annot fcl_ann) in + let fcl_env = env_of_annot fcl_ann in + let (tq,typ) = Env.get_val_spec_orig id fcl_env in let quant_kids = List.map kopt_kid (quant_kopts tq) in let ret_typ = match typ with @@ -3998,11 +4004,11 @@ let add_bitvector_casts (Defs defs) = " is not a function type")) in let pat,guard,body,annot = destruct_pexp pexp in - let env = env_of body in - let body = rewrite_body id quant_kids env ret_typ body in + let body_env = env_of body in + let body = rewrite_body id quant_kids body_env ret_typ body in (* Also add a cast around the entire function clause body, if necessary *) let body = - make_bitvector_cast_exp env quant_kids (fill_in_type (env_of body) (typ_of body)) ret_typ body + make_bitvector_cast_exp fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body in let pexp = construct_pexp (pat,guard,body,annot) in FCL_aux (FCL_Funcl (id,pexp),fcl_ann) @@ -4113,7 +4119,7 @@ let rewrite_toplevel_nexps (Defs defs) = | TypQ_aux (TypQ_no_forall,_) -> None | TypQ_aux (TypQ_tq qs, tq_l) -> let env = env_of_annot ann in - let env = add_typquant tqs env in + let env = add_typquant tq_l tqs env in let nexp_map, typ = rewrite_typ_in_spec env [] typ in match nexp_map with | [] -> None @@ -4198,7 +4204,7 @@ type options = { let recheck defs = let w = !Util.opt_warnings in let () = Util.opt_warnings := false in - let r = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in + let r = Type_error.check (Type_check.Env.no_casts Type_check.initial_env) defs in let () = Util.opt_warnings := w in r diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 00a6c4c3..1feb6513 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -58,6 +58,8 @@ module Big_int = Nat_big_num (* Option to turn tracing features on or off *) let opt_trace_ocaml = ref false +(* Option to not build generated ocaml by default *) +let opt_ocaml_nobuild = ref false type ctx = { register_inits : tannot exp list; @@ -175,9 +177,9 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) = | P_id id -> begin match Env.lookup_id id (pat_env_of pat) with - | Local (Immutable, _) | Unbound -> zencode ctx id + | Local (_, _) | Unbound -> zencode ctx id | Enum _ -> zencode_upper ctx id - | _ -> failwith ("Ocaml: Cannot pattern match on mutable variable or register:" ^ string_of_pat pat) + | _ -> failwith ("Ocaml: Cannot pattern match on register: " ^ string_of_pat pat) end | P_lit lit -> ocaml_lit lit | P_typ (_, pat) -> ocaml_pat ctx pat @@ -246,8 +248,8 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = (ocaml_atomic_exp ctx body ^^ semi) ^/^ separate space [string "if"; ocaml_atomic_exp ctx cond; - string "then loop ()"; - string "else ()"] + string "then ()"; + string "else loop ()"] in (string "let rec loop () =" ^//^ loop_body) ^/^ string "in" @@ -285,6 +287,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = (string ("let rec loop " ^ zencode_string (string_of_id id) ^ " =") ^//^ loop_body) ^/^ string "in" ^/^ (string "loop" ^^ space ^^ ocaml_atomic_exp ctx exp_from) + | E_cons (x, xs) -> ocaml_exp ctx x ^^ string " :: " ^^ ocaml_exp ctx xs | _ -> string ("EXP(" ^ string_of_exp exp ^ ")") and ocaml_letbind ctx (LB_aux (lb_aux, _)) = match lb_aux with @@ -697,6 +700,7 @@ let ocaml_compile spec defs = Unix.chdir "_sbuild"; let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/elf_loader.ml .") in let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lib.ml .") in + let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/util.ml .") in let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/_tags .") in let out_chan = open_out (spec ^ ".ml") in ocaml_pp_defs out_chan defs; @@ -708,10 +712,12 @@ let ocaml_compile spec defs = let out_chan = open_out "main.ml" in output_string out_chan (ocaml_main spec sail_dir); close_out out_chan; - system_checked "ocamlbuild -use-ocamlfind main.native"; - let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in - () + if not !opt_ocaml_nobuild then ( + system_checked "ocamlbuild -use-ocamlfind main.native"; + ignore (Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec)) + ) end - else - system_checked ("ocamlbuild -use-ocamlfind " ^ spec ^ ".cmo"); + else (if not !opt_ocaml_nobuild then + system_checked ("ocamlbuild -use-ocamlfind " ^ spec ^ ".cmo") + ); Unix.chdir cwd diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index a1133e09..2bc32c54 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -57,7 +57,7 @@ fix_id doc_quant_item on constraints type quantifiers in records, unions - update notation for records + multiple update notation for records register_refs? should I control the nexps somewhat? L_real @@ -86,18 +86,22 @@ open Pretty_print_common module StringSet = Set.Make(String) +let opt_undef_axioms = ref false + (**************************************************************************** * PPrint-based sail-to-coq pprinter ****************************************************************************) type context = { early_ret : bool; - kid_renames : kid KBindings.t; + kid_renames : kid KBindings.t; (* Plain tyvar -> tyvar renames *) + kid_id_renames : id KBindings.t; (* tyvar -> argument renames *) bound_nexps : NexpSet.t; } let empty_ctxt = { early_ret = false; kid_renames = KBindings.empty; + kid_id_renames = KBindings.empty; bound_nexps = NexpSet.empty } @@ -105,6 +109,7 @@ let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar let enclose_record = enclose (string "{| ") (string " |}") +let enclose_record_update = enclose (string "{[ ") (string " ]}") let bigarrow = string "=>" let separate_opt s f l = separate s (Util.map_filter f l) @@ -130,7 +135,7 @@ let rec fix_id remove_tick name = match name with | "LT" | "GT" | "EQ" - | "integer" + | "Z" -> name ^ "'" | _ -> if String.contains name '#' then @@ -170,7 +175,11 @@ let doc_id_ctor (Id_aux(i,_)) = * token in case of x ending with star. *) separate space [colon; string x; empty] -let doc_var_lem ctx kid = string (fix_id true (string_of_kid (try KBindings.find kid ctx.kid_renames with Not_found -> kid))) +let doc_var_lem ctx kid = + match KBindings.find kid ctx.kid_id_renames with + | id -> doc_id id + | exception Not_found -> + string (fix_id true (string_of_kid (try KBindings.find kid ctx.kid_renames with Not_found -> kid))) let doc_docstring_lem (l, _) = match l with | Parse_ast.Documented (str, _) -> string ("(*" ^ str ^ "*)") ^^ hardline @@ -200,19 +209,35 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with | _ -> false let doc_nexp ctx nexp = - let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in - match nexp with - | Nexp_constant i -> string (Big_int.to_string i) - | Nexp_var v -> doc_var_lem ctx v - | Nexp_id id -> doc_id id - | Nexp_times (n1, n2) -> separate space [doc_nexp n1; star; doc_nexp n2] - | Nexp_sum (n1, n2) -> separate space [doc_nexp n1; plus; doc_nexp n2] - | Nexp_minus (n1, n2) -> separate space [doc_nexp n1; minus; doc_nexp n2] - | Nexp_exp n -> separate space [string "2"; caret; doc_nexp n] - | Nexp_neg n -> separate space [minus; doc_nexp n] - | _ -> - raise (Reporting_basic.err_unreachable l - ("cannot pretty-print nexp \"" ^ string_of_nexp full_nexp ^ "\"")) + (* Print according to Coq's precedence rules *) + let rec plussub (Nexp_aux (n,l) as nexp) = + match n with + | Nexp_sum (n1, n2) -> separate space [plussub n1; plus; muldiv n2] + | Nexp_minus (n1, n2) -> separate space [plussub n1; minus; muldiv n2] + | _ -> muldiv nexp + and muldiv (Nexp_aux (n,l) as nexp) = + match n with + | Nexp_times (n1, n2) -> separate space [muldiv n1; star; uneg n2] + | _ -> uneg nexp + and uneg (Nexp_aux (n,l) as nexp) = + match n with + | Nexp_neg n -> separate space [minus; uneg n] + | _ -> exp nexp + and exp (Nexp_aux (n,l) as nexp) = + match n with + | Nexp_exp n -> separate space [string "2"; caret; exp n] + | _ -> atomic nexp + and atomic (Nexp_aux (n,l) as nexp) = + match n with + | Nexp_constant i -> string (Big_int.to_string i) + | Nexp_var v -> doc_var_lem ctx v + | Nexp_id id -> doc_id id + | Nexp_sum _ | Nexp_minus _ | Nexp_times _ | Nexp_neg _ | Nexp_exp _ + -> parens (plussub nexp) + | _ -> + raise (Reporting_basic.err_unreachable l + ("cannot pretty-print nexp \"" ^ string_of_nexp nexp ^ "\"")) + in atomic (nexp_simp nexp) (* Rewrite mangled names of type variables to the original names *) let rec orig_nexp (Nexp_aux (nexp, l)) = @@ -265,6 +290,48 @@ let lem_tyvars_of_typ typ = NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp)) (lem_nexps_of_typ typ) KidSet.empty +(* In existential types we don't want term-level versions of the + type variables to stick around *) +let drop_duplicate_atoms kids ty = + let kids = KidSet.of_list kids in + let rec aux_typ (Typ_aux (typ,l) as full_typ) = + match typ with + | Typ_id _ + | Typ_var _ -> Some full_typ + | Typ_fn (arg,res,eff) -> failwith "Function type nested inside existential" + | Typ_tup typs -> + (match Util.map_filter aux_typ typs with + | [] -> None + | typs' -> Some (Typ_aux (Typ_tup typs',l))) + | Typ_exist _ -> failwith "Nested existential type" + (* This is an AST type, don't need to check for equivalent nexps *) + | Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid,_)),_)]) + when KidSet.mem kid kids -> + None + (* Don't recurse into type arguments, removing stuff there + would be weird (and difficult) *) + | Typ_app _ -> Some full_typ + in aux_typ ty + +(* TODO: parens *) +let rec doc_nc ctx (NC_aux (nc,_)) = + match nc with + | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_set (kid, is) -> (* TODO: is this a good translation? *) + separate space [string "In"; doc_var_lem ctx kid; + brackets (separate (string "; ") + (List.map (fun i -> string (Nat_big_num.to_string i)) is))] + | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc ctx nc1) (doc_nc ctx nc2) + | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc ctx nc1) (doc_nc ctx nc2) + | NC_true -> string "True" + | NC_false -> string "False" + +let doc_arithfact ctxt nc = + string "ArithFact" ^^ space ^^ parens (doc_nc ctxt nc) + (* When making changes here, check whether they affect lem_tyvars_of_typ *) let doc_typ, doc_atomic_typ = let fns ctx = @@ -325,11 +392,22 @@ let doc_typ, doc_atomic_typ = * if we add a new Typ constructor *) let tpp = typ ty in if atyp_needed then parens tpp else tpp - | Typ_exist (kids,_,ty) -> - let tpp = typ ty in -tpp (* List.fold_left - (fun tpp kid -> braces (separate space [doc_var_lem kid; colon; string "Z"; ampersand; tpp])) - tpp kids*) + | Typ_exist (kids,nc,ty) -> begin + let add_tyvar tpp kid = + braces (separate space [doc_var_lem ctx kid; colon; string "Z"; ampersand; tpp]) + in + match drop_duplicate_atoms kids ty with + | Some ty -> + let tpp = typ ty in + let tpp = match nc with NC_aux (NC_true,_) -> tpp | _ -> + braces (separate space [underscore; colon; parens (doc_arithfact ctx nc); ampersand; tpp]) + in + List.fold_left add_tyvar tpp kids + | None -> + match nc with + | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids) + | _ -> List.fold_left add_tyvar (doc_arithfact ctx nc) kids + end and doc_typ_arg (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ true t | Typ_arg_nexp n -> doc_nexp ctx n @@ -347,7 +425,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = match t with | Typ_app (Id_aux (Id "vector",_) as id, [Typ_arg_aux (Typ_arg_nexp size,_);ord;typ']) -> begin - let mk_typ nexp = + let mk_typ nexp = Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in match Type_check.solve env size with @@ -387,7 +465,7 @@ let doc_lit (L_aux(lit,l)) = | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> - utf8string "(return (failwith \"undefined value of unsupported type\"))" + utf8string "(Fail \"undefined value of unsupported type\")" | L_string s -> utf8string ("\"" ^ s ^ "\"") | L_real s -> (* Lem does not support decimal syntax, so we translate a string @@ -407,43 +485,44 @@ let doc_lit (L_aux(lit,l)) = parens (separate space (List.map string [ "realFromFrac"; Big_int.to_string num; Big_int.to_string denom])) -(* TODO: parens *) -let rec doc_nc ctx (NC_aux (nc,_)) = - match nc with - | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_set (kid, is) -> (* TODO: is this a good translation? *) - separate space [string "In"; doc_var_lem ctx kid; - brackets (separate (string "; ") - (List.map (fun i -> string (Nat_big_num.to_string i)) is))] - | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc ctx nc1) (doc_nc ctx nc2) - | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc ctx nc1) (doc_nc ctx nc2) - | NC_true -> string "True" - | NC_false -> string "False" - -let doc_quant_item ctx delimit (QI_aux (qi,_)) = +let doc_quant_item_id ctx delimit (QI_aux (qi,_)) = match qi with | QI_id (KOpt_aux (KOpt_none kid,_)) -> + if KBindings.mem kid ctx.kid_id_renames then None else Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Z"])) | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (kind,_)],_),kid),_)) -> begin + if KBindings.mem kid ctx.kid_id_renames then None else match kind with | BK_type -> Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Type"])) | BK_int -> Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Z"])) | BK_order -> None end | QI_id _ -> failwith "Quantifier with multiple kinds" - | QI_const nc -> Some (bquote ^^ braces (string "ArithFact" ^^ parens (doc_nc ctx nc))) + | QI_const nc -> None + +let doc_quant_item_constr ctx delimit (QI_aux (qi,_)) = + match qi with + | QI_id _ -> None + | QI_const nc -> Some (bquote ^^ braces (doc_arithfact ctx nc)) let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) = match tq with - | TypQ_tq qis -> separate_opt space (doc_quant_item ctx delimit) qis + | TypQ_tq qis -> + separate_opt space (doc_quant_item_id ctx delimit) qis ^^ + separate_opt space (doc_quant_item_constr ctx delimit) qis | TypQ_no_forall -> empty +let doc_typquant_items_separate ctx delimit (TypQ_aux (tq,_)) = + match tq with + | TypQ_tq qis -> + separate_opt space (doc_quant_item_id ctx delimit) qis, + separate_opt space (doc_quant_item_constr ctx delimit) qis + | TypQ_no_forall -> empty, empty + let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with | TypQ_tq ((_ :: _) as qs) -> - string "forall " ^^ separate_opt space (doc_quant_item ctx parens) qs ^^ string ". " ^^ typ + string "forall " ^^ separate_opt space (doc_quant_item_id ctx braces) qs ^/^ + separate_opt space (doc_quant_item_constr ctx parens) qs ^^ string ", " ^^ typ | _ -> typ (* Produce Size type constraints for bitvector sizes when using @@ -476,51 +555,80 @@ let is_ctor env id = match Env.lookup_id id env with | Enum _ -> true | _ -> false +let is_auto_decomposed_exist env typ = + match destruct_exist env typ with + | Some (kids, nc, (Typ_aux (Typ_app (id, _),_) as typ')) when string_of_id id = "atom" -> Some typ' + | _ -> None + (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) -let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot))) = match p with - | P_app(id, ((_ :: _) as pats)) -> - let ppp = doc_unop (doc_id_ctor id) - (parens (separate_map comma (doc_pat ctxt true) pats)) in - if apat_needed then parens ppp else ppp - | P_app(id, []) -> doc_id_ctor id - | P_lit lit -> doc_lit lit - | P_wild -> underscore - | P_id id -> doc_id id - | P_var(p,_) -> doc_pat ctxt true p - | P_as(p,id) -> parens (separate space [doc_pat ctxt true p; string "as"; doc_id id]) - | P_typ(typ,p) -> - let doc_p = doc_pat ctxt true p in - doc_p - (* Type annotations aren't allowed everywhere in patterns in Coq *) - (*parens (doc_op colon doc_p (doc_typ typ))*) - | P_vector pats -> - let ppp = brackets (separate_map semi (doc_pat ctxt true) pats) in - if apat_needed then parens ppp else ppp - | P_vector_concat pats -> - raise (Reporting_basic.err_unreachable l - "vector concatenation patterns should have been removed before pretty-printing") - | P_tup pats -> - (match pats with - | [p] -> doc_pat ctxt apat_needed p - | _ -> parens (separate_map comma_sp (doc_pat ctxt false) pats)) - | P_list pats -> brackets (separate_map semi (doc_pat ctxt false) pats) - | P_cons (p,p') -> doc_op (string "::") (doc_pat ctxt true p) (doc_pat ctxt true p') - | P_record (_,_) -> empty (* TODO *) - -let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with - | Typ_tup ts -> List.exists typ_needs_printed ts - | Typ_app (Id_aux (Id "itself",_),_) -> true - | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs - | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2 - | Typ_exist (kids,_,t) -> - let visible_kids = KidSet.inter (KidSet.of_list kids) (lem_tyvars_of_typ t) in - typ_needs_printed t && KidSet.is_empty visible_kids - | _ -> false -and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with - | Typ_arg_typ t -> typ_needs_printed t - | _ -> false +let rec doc_pat ctxt apat_needed (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 is_auto_decomposed_exist env typ with + | Some typ' -> + let pat_pp = doc_pat ctxt 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 + | None -> + match p with + (* Special case translation of the None constructor to remove the unit arg *) + | P_app(id, _) when string_of_id id = "None" -> string "None" + | P_app(id, ((_ :: _) as pats)) -> + let ppp = doc_unop (doc_id_ctor id) + (* TODO: we shouldn't use pat_typ_of here, + we should either get the type checker to put the full type in the + annotation (including all existentials), or provide some other way to + retrieve the full types for the args from typ. *) + (parens (separate_map comma (fun p -> doc_pat ctxt true (p, pat_typ_of p)) pats)) in + if apat_needed then parens ppp else ppp + | P_app(id, []) -> doc_id_ctor id + | P_lit lit -> doc_lit lit + | P_wild -> underscore + | P_id id -> doc_id id + | P_var(p,_) -> doc_pat ctxt true (p, typ) + | P_as(p,id) -> parens (separate space [doc_pat ctxt true (p, typ); string "as"; doc_id id]) + | P_typ(ptyp,p) -> + let doc_p = doc_pat ctxt true (p, ptyp) in + doc_p + (* Type annotations aren't allowed everywhere in patterns in Coq *) + (*parens (doc_op colon doc_p (doc_typ typ))*) + | P_vector pats -> + let el_typ = + match destruct_vector env typ with + | Some (_,_,t) -> t + | None -> failwith "vector pattern doesn't have vector type" + in + let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true (p,el_typ)) pats) in + if apat_needed then parens ppp else ppp + | P_vector_concat pats -> + raise (Reporting_basic.err_unreachable l + "vector concatenation patterns should have been removed before pretty-printing") + | P_tup pats -> + let typs = match typ with + | Typ_aux (Typ_tup typs, _) -> typs + | _ -> failwith "tuple pattern doesn't have tuple type" + in + (match pats, typs with + | [p], [typ'] -> doc_pat ctxt apat_needed (p, typ') + | [_], _ -> failwith "tuple pattern length does not match tuple type length" + | _ -> parens (separate_map comma_sp (doc_pat ctxt false) (List.combine pats typs))) + | P_list pats -> + let el_typ = match typ with + | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_) + when Id.compare f (mk_id "list") = 0 -> el_typ + | _ -> failwith "list pattern not a list" + in + brackets (separate_map semi (fun p -> doc_pat ctxt false (p, el_typ)) pats) + | P_cons (p,p') -> + let el_typ = match typ with + | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_) + when Id.compare f (mk_id "list") = 0 -> el_typ + | _ -> failwith "list pattern not a list" + in + doc_op (string "::") (doc_pat ctxt true (p, el_typ)) (doc_pat ctxt true (p', typ)) + | P_record (_,_) -> empty (* TODO *) let contains_early_return exp = let e_app (f, args) = @@ -551,6 +659,13 @@ let doc_exp_lem, doc_let_lem = let expY = top_exp ctxt true in let expN = top_exp ctxt false in let expV = top_exp ctxt in + let maybe_add_exist epp = + match destruct_exist (env_of full_exp) (typ_of full_exp) with + | None -> epp + | Some _ -> + let epp = string "build_ex" ^/^ epp in + if aexp_needed then parens epp else epp + in let liftR doc = if ctxt.early_ret && effectful (effect_of full_exp) then separate space [string "liftR"; parens (doc)] @@ -637,12 +752,14 @@ let doc_exp_lem, doc_let_lem = match args with | [exp1; exp2; exp3; ord_exp; vartuple; body] -> let loopvar, body = match body with - | E_aux (E_let (LB_aux (LB_val ( - P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body - | E_aux (E_let (LB_aux (LB_val ( - P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body - | E_aux (E_let (LB_aux (LB_val ( - P_aux (P_id id, _), _), _), body), _) -> id, body + | E_aux (E_let (LB_aux (LB_val (_, _), _), + E_aux (E_let (LB_aux (LB_val (_, _), _), + E_aux (E_if (_, + E_aux (E_let (LB_aux (LB_val ( + ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _)) + | (P_aux (P_var (P_aux (P_id id, _), _), _)) + | (P_aux (P_id id, _))), _), _), + body), _), _), _)), _)), _) -> id, body | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in let step = match ord_exp with | E_aux (E_lit (L_aux (L_false, _)), _) -> @@ -733,31 +850,52 @@ let doc_exp_lem, doc_let_lem = "Unexpected number of arguments for early_return builtin") end | _ -> - begin match annot with - | Some (env, _, _) when Env.is_union_constructor f env -> - let epp = - match args with - | [] -> doc_id_ctor f - | [arg] -> doc_id_ctor f ^^ space ^^ expV true arg - | _ -> - doc_id_ctor f ^^ space ^^ - parens (separate_map comma (expV false) args) in - if aexp_needed then parens (align epp) else epp - | _ -> - let call, is_extern = match annot with - | Some (env, _, _) when Env.is_extern f env "coq" -> - string (Env.get_extern f env "coq"), true - | _ -> doc_id f, false in - let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in - let (taepp,aexp_needed) = - let env = env_of full_exp in - let t = Env.expand_synonyms env (typ_of full_exp) in - let eff = effect_of full_exp in - if typ_needs_printed t - then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true) - else (epp, aexp_needed) in - liftR (if aexp_needed then parens (align taepp) else taepp) - end + let env = env_of_annot (l,annot) in + if Env.is_union_constructor f env then + let epp = + match args with + | [] -> doc_id_ctor f + | [arg] -> doc_id_ctor f ^^ space ^^ expV true arg + | _ -> + doc_id_ctor f ^^ space ^^ + parens (separate_map comma (expV false) args) in + if aexp_needed then parens (align epp) else epp + else + let call, is_extern = + if Env.is_extern f env "coq" + then string (Env.get_extern f env "coq"), true + else doc_id f, false in + let (tqs,fn_ty) = Env.get_val_spec_orig f env in + let arg_typs, ret_typ = match fn_ty with + | Typ_aux (Typ_fn (arg_typ,ret_typ,_),_) -> + (match arg_typ with + | Typ_aux (Typ_tup typs,_) -> typs, ret_typ + | _ -> [arg_typ], ret_typ) + | _ -> failwith "Function not a function type" + in + (* Insert existential unpacking of arguments where necessary *) + let doc_arg arg typ_from_fn = + let arg_pp = expY arg in + (* TODO: more sophisticated check *) + match destruct_exist env (typ_of arg), destruct_exist env typ_from_fn with + | Some _, None -> parens (string "projT1 " ^^ arg_pp) + | _, _ -> arg_pp + in + let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in + (* Unpack existential result *) + let ret_typ_inst = subst_unifiers (instantiation_of full_exp) ret_typ in + let unpack,build_ex = + let ann_typ = Env.expand_synonyms env (typ_of_annot (l,annot)) in + match ret_typ_inst, ann_typ with + | Typ_aux (Typ_exist _,_), Typ_aux (Typ_exist _,_) -> + if alpha_equivalent env ret_typ_inst ann_typ then false,false else true,true + | Typ_aux (Typ_exist _,_), _ -> true,false + | _, Typ_aux (Typ_exist _,_) -> false,true + | _, _ -> false,false + in + let epp = if unpack then string "projT1" ^^ space ^^ parens epp else epp in + let epp = if build_ex then string "build_ex" ^^ space ^^ parens epp else epp in + liftR (if aexp_needed then parens (align epp) else epp) end | E_vector_access (v,e) -> raise (Reporting_basic.err_unreachable l @@ -774,7 +912,7 @@ let doc_exp_lem, doc_let_lem = if prefix_recordtype && string_of_id tid <> "regstate" then (string (string_of_id tid ^ "_")) ^^ doc_id id else doc_id id in - expY fexp ^^ dot ^^ fname + expY fexp ^^ dot ^^ parens fname | _ -> raise (report l "E_field expression with no register or record type")) | E_block [] -> string "tt" @@ -792,8 +930,8 @@ let doc_exp_lem, doc_let_lem = else liftR epp else if Env.is_register id env then doc_id (append_id id "_ref") else if is_ctor env id then doc_id_ctor id - else doc_id id - | E_lit lit -> doc_lit lit + else maybe_add_exist (doc_id id) + | E_lit lit -> maybe_add_exist (doc_lit lit) | E_cast(typ,e) -> expV aexp_needed e | E_tuple exps -> @@ -816,7 +954,7 @@ let doc_exp_lem, doc_let_lem = when Env.is_record tid env -> tid | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in - anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) + enclose_record_update (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = @@ -855,7 +993,7 @@ let doc_exp_lem, doc_let_lem = 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) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt (typ_of e)) pexps) ^/^ (string "end")) in if aexp_needed then parens (align epp) else align epp | E_try (e, pexps) -> @@ -863,7 +1001,7 @@ let doc_exp_lem, doc_let_lem = let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in let epp = group ((separate space [string try_catch; expY e; string "(function "]) ^/^ - (separate_map (break 1) (doc_case ctxt) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^ (string "end)")) in if aexp_needed then parens (align epp) else align epp else @@ -893,10 +1031,10 @@ let doc_exp_lem, doc_let_lem = tuple patterns to Isabelle *) separate space [string ">>= fun varstup => let"; - doc_pat ctxt true pat; + doc_pat ctxt true (pat, typ_of e1); string "= varstup in"] | _ -> - separate space [string ">>= fun"; doc_pat ctxt true pat; bigarrow] + separate space [string ">>= fun"; doc_pat ctxt true (pat, typ_of e1); bigarrow] in infix 0 1 middle (expV b e1) (expN e2) in @@ -934,14 +1072,24 @@ let doc_exp_lem, doc_let_lem = | _ -> prefix 2 1 (string "else") (top_exp ctxt false e) in (prefix 2 1 - (soft_surround 2 1 if_pp (top_exp ctxt true c) (string "then")) + (soft_surround 2 1 if_pp (string "sumbool_of_bool" ^^ space ^^ parens (top_exp ctxt true c)) (string "then")) (top_exp ctxt false t)) ^^ break 1 ^^ else_pp and let_exp ctxt (LB_aux(lb,_)) = match lb with + (* 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) -> + 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) -> + prefix 2 1 + (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq]) + (top_exp ctxt false e) | LB_val(pat,e) -> prefix 2 1 - (separate space [string "let"; squote ^^ doc_pat ctxt true pat; coloneq]) + (separate space [string "let"; squote ^^ doc_pat ctxt true (pat, typ_of e); coloneq]) (top_exp ctxt false e) and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) = @@ -951,9 +1099,9 @@ let doc_exp_lem, doc_let_lem = else doc_id id in group (doc_op coloneq fname (top_exp ctxt true e)) - and doc_case ctxt = function + and doc_case ctxt typ = function | Pat_aux(Pat_exp(pat,e),_) -> - group (prefix 3 1 (separate space [pipe; doc_pat ctxt false pat;bigarrow]) + group (prefix 3 1 (separate space [pipe; doc_pat ctxt false (pat,typ);bigarrow]) (group (top_exp ctxt false e))) | Pat_aux(Pat_when(_,_,_),(l,_)) -> raise (Reporting_basic.err_unreachable l @@ -1060,13 +1208,18 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with | Id_aux ((Id "diafp"),_) -> empty *) | Id_aux ((Id "option"),_) -> empty | _ -> - let typ_nm = separate space [doc_id_type id; doc_typquant_items empty_ctxt parens typq] in - let ar_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_type_union empty_ctxt typ_nm) ar) in + let id_pp = doc_id_type id in + let typ_nm = separate space [id_pp; doc_typquant_items empty_ctxt braces typq] in + let ar_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_type_union empty_ctxt id_pp) ar) in let typ_pp = (doc_op coloneq) (concat [string "Inductive"; space; typ_nm]) ((*doc_typquant_lem typq*) ar_doc) in - typ_pp ^^ dot ^^ hardline ^^ hardline) + (* We declared the type parameters as implicit so that they're implicit + in the constructors. Currently Coq also makes them implicit in the + type, so undo that here. *) + let resetimplicit = separate space [string "Arguments"; id_pp; colon; string "clear implicits."] in + typ_pp ^^ dot ^^ hardline ^^ resetimplicit ^^ hardline ^^ hardline) | TD_enum(id,nm,enums,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty @@ -1202,6 +1355,35 @@ let mk_kid_renames ids_to_avoid kids = in check kid in snd (KidSet.fold check_kid kids (kids, KBindings.empty)) +let merge_kids_atoms pats = + let try_eliminate (gone,map,seen) = function + | P_aux (P_id id, ann), typ -> begin + match Type_check.destruct_atom_nexp (env_of_annot ann) typ with + | Some (Nexp_aux (Nexp_var kid,l)) -> + if KidSet.mem kid seen then + let () = + Reporting_basic.print_err false true l "merge_kids_atoms" + ("want to merge tyvar and argument for " ^ string_of_kid kid ^ + " but rearranging arguments isn't supported yet") in + gone,map,seen + else + KidSet.add kid gone, KBindings.add kid id map, KidSet.add kid seen + | _ -> gone,map,KidSet.union seen (tyvars_of_typ typ) + end + | _, typ -> gone,map,KidSet.union seen (tyvars_of_typ typ) + in + let gone,map,_ = List.fold_left try_eliminate (KidSet.empty, KBindings.empty, KidSet.empty) pats in + gone,map + +let doc_binder ctxt (P_aux (p,ann) as pat, typ) = + let env = env_of_annot ann in + let exp_typ = Env.expand_synonyms env typ in + match p with + | P_id id + | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ]) + | _ -> squote ^^ parens (separate space [doc_pat ctxt true (pat, exp_typ); colon; doc_typ ctxt typ]) + let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in let (arg_typ, ret_typ, eff) = match typ with @@ -1211,16 +1393,20 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let ids_to_avoid = all_ids pexp in let kids_used = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in + let pats, bind = untuple_args_pat arg_typ pat in + let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in + let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in + let kids_used = KidSet.diff kids_used eliminated_kids in let ctxt = { early_ret = contains_early_return exp; kid_renames = mk_kid_renames ids_to_avoid kids_used; + kid_id_renames = kid_to_arg_rename; bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ) } in - let quantspp = doc_typquant_items ctxt braces tq in - let pats, bind = untuple_args_pat arg_typ pat in - let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in + (* Put the constraints after pattern matching so that any type variable that's + been replaced by one of the term-level arguments is bound. *) + let quantspp, constrspp = doc_typquant_items_separate ctxt braces tq in let exp = List.fold_left (fun body f -> f body) (bind exp) binds in - let patspp = separate_map space (fun (pat,typ) -> - squote ^^ parens (separate space [doc_pat ctxt true pat; colon; doc_typ ctxt typ])) pats in + let patspp = separate_map space (doc_binder ctxt) pats in let atom_constr_pp = separate_opt space (atom_constraint ctxt) pats in let retpp = if effectful eff @@ -1233,7 +1419,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = raise (Reporting_basic.err_unreachable l "guarded pattern expression should have been rewritten before pretty-printing") in group (prefix 3 1 - (separate space [doc_id id; quantspp; patspp; atom_constr_pp; colon; retpp; coloneq]) + (separate space [doc_id id; quantspp; patspp; constrspp; atom_constr_pp; colon; retpp; coloneq]) (doc_fun_body ctxt exp ^^ dot)) let get_id = function @@ -1330,10 +1516,84 @@ let doc_regtype_fields (tname, (n1, n2, fields)) = in separate_map hardline doc_field fields -let rec doc_def def = +(* Remove some type variables in a similar fashion to merge_kids_atoms *) +let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) = + let typ_env = add_typquant l tqs typ_env in + match typ with + | Typ_aux (Typ_fn (args_ty, ret_ty, eff),l') -> + let check_typ (args,used) typ = + match Type_check.destruct_atom_nexp typ_env typ with + | Some (Nexp_aux (Nexp_var kid,_)) -> + if KidSet.mem kid used then args,used else + KidSet.add kid args, used + | Some _ -> args, used + | _ -> args, KidSet.union used (tyvars_of_typ typ) + in + let typs = match args_ty with Typ_aux (Typ_tup typs,_) -> typs | _ -> [args_ty] in + let args, used = List.fold_left check_typ (KidSet.empty, KidSet.empty) typs in + let used = if is_number ret_ty then used else KidSet.union used (tyvars_of_typ ret_ty) in + let tqs = match tqs with + | TypQ_aux (TypQ_tq qs,l) -> TypQ_aux (TypQ_tq (List.filter (function + | QI_aux (QI_id kopt,_) when is_nat_kopt kopt -> + let kid = kopt_kid kopt in + KidSet.mem kid used && not (KidSet.mem kid args) + | _ -> true) qs),l) + | _ -> tqs + in + let doc_typ' typ = + match Type_check.destruct_atom_nexp typ_env typ with + | Some (Nexp_aux (Nexp_var kid,_)) when KidSet.mem kid args -> + parens (doc_var_lem empty_ctxt kid ^^ string " : Z") + | _ -> parens (underscore ^^ string " : " ^^ doc_typ empty_ctxt typ) + in + let arg_typs_pp = separate space (List.map doc_typ' typs) in + let ret_typ_pp = doc_typ empty_ctxt ret_ty in + let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in + string "forall" ^/^ tyvars_pp ^/^ arg_typs_pp ^/^ constrs_pp ^^ comma ^/^ ret_typ_pp + | _ -> doc_typschm empty_ctxt true ts + +let doc_val_spec unimplemented (VS_aux (VS_val_spec(tys,id,_,_),ann)) = + if !opt_undef_axioms && IdSet.mem id unimplemented then + let typ_env = env_of_annot ann in + group (separate space + [string "Axiom"; doc_id id; colon; doc_axiom_typschm typ_env tys] ^^ dot) ^/^ hardline + else empty (* Type signatures appear in definitions *) + +(* If a top-level value is an existential type, we define the dependent pair of + the value and the proof, then just the value with Let so that it appears in + the local context when constraint solving and the ltac can find the proof. *) +let doc_val pat exp = + let (id,typpp) = match pat with + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ empty_ctxt typ + | P_aux (P_id id, _) -> id, empty + | _ -> failwith "Top-level value definition with complex pattern not supported for Coq yet" + in + let id, opt_unpack = + match destruct_exist (env_of exp) (typ_of exp) with + | None -> id, None + | Some (kids,nc,typ) -> + match drop_duplicate_atoms kids typ, nc with + | None, NC_aux (NC_true,_) -> id, None + | _ -> + (* TODO: name collisions *) + mk_id (string_of_id id ^ "_spec"), + Some (id, string_of_id id ^ "_prop") + in + let idpp = doc_id id in + let basepp = + group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^^ + space ^^ doc_exp_lem empty_ctxt false exp ^^ dot) ^^ hardline + in + match opt_unpack with + | None -> basepp ^^ hardline + | Some (orig_id, hyp_id) -> + basepp ^^ + group (separate space [string "Let"; doc_id orig_id; coloneq; string "projT1"; idpp; dot]) ^^ hardline ^^ hardline + +let rec doc_def unimplemented def = (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with - | DEF_spec v_spec -> empty (* Types appear in definitions *) + | DEF_spec v_spec -> doc_val_spec unimplemented v_spec | DEF_fixity _ -> empty | DEF_overload _ -> empty | DEF_type t_def -> group (doc_typdef t_def) ^/^ hardline @@ -1342,20 +1602,13 @@ let rec doc_def def = | DEF_default df -> empty | DEF_fundef fdef -> group (doc_fundef fdef) ^/^ hardline | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline - | DEF_val (LB_aux (LB_val (pat, exp), _)) -> - let (id,typpp) = match pat with - | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ empty_ctxt typ - | P_aux (P_id id, _) -> id, empty - | _ -> failwith "Top-level value definition with complex pattern not supported for Coq yet" - in - group (string "Definition" ^^ space ^^ doc_id id ^^ typpp ^^ space ^^ coloneq ^^ - doc_exp_lem empty_ctxt false exp ^^ dot) ^/^ hardline + | DEF_val (LB_aux (LB_val (pat, exp), _)) -> doc_val pat exp | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" | DEF_kind _ -> empty | DEF_comm (DC_comm s) -> comment (string s) - | DEF_comm (DC_comm_struct d) -> comment (doc_def d) + | DEF_comm (DC_comm_struct d) -> comment (doc_def unimplemented d) let find_exc_typ defs = @@ -1364,6 +1617,23 @@ let find_exc_typ defs = | _ -> false in if List.exists is_exc_typ_def defs then "exception" else "unit" +let find_unimplemented defs = + let adjust_def unimplemented = function + | DEF_spec (VS_aux (VS_val_spec (_,id,ext,_),_)) -> begin + match ext "coq" with + | Some _ -> unimplemented + | None -> IdSet.add id unimplemented + end + | DEF_fundef (FD_aux (FD_function (_,_,_,funcls),_)) -> begin + match funcls with + | [] -> unimplemented + | (FCL_aux (FCL_Funcl (id,_),_))::_ -> + IdSet.remove id unimplemented + end + | _ -> unimplemented + in + List.fold_left adjust_def IdSet.empty defs + let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line = (* let regtypes = find_regtypes d in *) let state_ids = @@ -1383,15 +1653,21 @@ let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) let typdefs, defs = List.partition is_typ_def defs in let statedefs, defs = List.partition is_state_def defs in let register_refs = State.register_refs_coq (State.find_registers defs) in + let unimplemented = find_unimplemented defs in + let () = if !opt_undef_axioms || IdSet.is_empty unimplemented then () else + Reporting_basic.print_err false false Parse_ast.Unknown "Warning" + ("The following functions were declared but are undefined:\n" ^ + String.concat "\n" (List.map string_of_id (IdSet.elements unimplemented))) + in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "Require Import";string lib] ^^ dot) types_modules;hardline; string "Require Import String."; hardline; - separate empty (List.map doc_def typdefs); hardline; + separate empty (List.map (doc_def unimplemented) typdefs); hardline; hardline; - separate empty (List.map doc_def statedefs); hardline; + separate empty (List.map (doc_def unimplemented) statedefs); hardline; hardline; register_refs; hardline; concat [ @@ -1404,7 +1680,14 @@ string "Require Import String."; hardline; [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline; -string "Require Import List. Import ListNotations."; +string "Require Import List. Import ListNotations. Require Import Sumbool."; + hardline; + (* Put the body into a Section so that we can define some values with + Let to put them into the local context, where tactics can see them *) + string "Section Content."; + hardline; + hardline; + separate empty (List.map (doc_def unimplemented) defs); hardline; - separate empty (List.map doc_def defs); + string "End Content."; hardline]); diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 58bbfc4b..c872d420 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -883,8 +883,7 @@ let doc_exp_lem, doc_let_lem = let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in let middle = match fst (untyp_pat pat) with - | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> - string ">>" + | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_tup _, _) when not (IdSet.mem (mk_id "varstup") (find_e_ids e2)) -> (* Work around indentation issues in Lem when translating @@ -894,7 +893,8 @@ let doc_exp_lem, doc_let_lem = doc_pat_lem ctxt true pat; string "= varstup in"] | _ -> - separate space [string ">>= fun"; doc_pat_lem ctxt true pat; arrow] + separate space [string ">>= fun"; + doc_pat_lem ctxt true pat; arrow] in infix 0 1 middle (expV b e1) (expN e2) in @@ -908,12 +908,11 @@ let doc_exp_lem, doc_let_lem = raise (Reporting_basic.err_unreachable l "pretty-printing non-constant sizeof expressions to Lem not supported")) | E_return r -> - let ret_monad = if !opt_sequential then " : MR regstate" else " : MR" in let ta = if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r) then empty else separate space - [string ret_monad; + [string ": MR"; parens (doc_typ_lem (typ_of full_exp)); parens (doc_typ_lem (typ_of r))] in align (parens (string "early_return" ^//^ expV true r ^//^ ta)) @@ -1438,17 +1437,11 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs) separate empty (List.map doc_def_lem statedefs); hardline; hardline; register_refs; hardline; - (* if !opt_sequential then - concat [ - string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline; - ] - else *) - concat [ - string ("type MR 'a 'r = monadR register_value 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = monad register_value 'a " ^ exc_typ); hardline - ] - ]); + concat [ + string ("type MR 'a 'r = base_monadR register_value regstate 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = base_monad register_value regstate 'a " ^ exc_typ); hardline + ] + ]); (print defs_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; diff --git a/src/process_file.ml b/src/process_file.ml index 7cab1266..710655c4 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -51,9 +51,6 @@ open PPrint open Pretty_print_common -let opt_lem_sequential = ref false -let opt_lem_mwords = ref false - type out_type = | Lem_ast_out | Lem_out of string list @@ -221,7 +218,7 @@ let load_file_no_check order f = convert_ast order (preprocess_ast (parse_file f let load_file order env f = let ast = convert_ast order (preprocess_ast (parse_file f)) in - Type_check.check env ast + Type_error.check env ast let opt_just_check = ref false let opt_ddump_tc_ast = ref false @@ -230,7 +227,7 @@ let opt_dno_cast = ref false let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in - let ast, env = Type_check.check env defs in + let ast, env = Type_error.check env defs in let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) @@ -282,10 +279,7 @@ let output_lem filename libs defs = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in - let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in - (* if !Pretty_print_lem.opt_sequential - then ["State_monad"; "State"] - else ["Prompt_monad"; "Prompt"] in *) + let monad_modules = ["Prompt_monad"; "Prompt"] in let operators_module = if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" @@ -399,13 +393,17 @@ let rewrite_step defs (name,rewriter) = let rewrite rewriters defs = try List.fold_left rewrite_step defs rewriters with | Type_check.Type_error (l, err) -> - raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err)) + raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)] let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml -let rewrite_ast_c = rewrite Rewrites.rewrite_defs_c +let rewrite_ast_c ast = + ast + |> rewrite Rewrites.rewrite_defs_c + |> Constant_fold.rewrite_constant_function_calls + let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check diff --git a/src/process_file.mli b/src/process_file.mli index b38b4259..cc94888e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -65,8 +65,6 @@ val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val load_file_no_check : Ast.order -> string -> unit Ast.defs val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t -val opt_lem_sequential : bool ref -val opt_lem_mwords : bool ref val opt_just_check : bool ref val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref diff --git a/src/rewrites.ml b/src/rewrites.ml index 5fe54f84..b938d2d7 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -418,7 +418,7 @@ let rewrite_sizeof (Defs defs) = let inst = try instantiation_of orig_exp with | Type_error (l, err) -> - raise (Reporting_basic.err_typ l (string_of_type_error err)) in + raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) in (* Rewrite the inst using orig_kid so that each type variable has it's original name rather than a mangled typechecker name *) let inst = KBindings.fold (fun kid uvar b -> KBindings.add (orig_kid kid) uvar b) inst KBindings.empty in @@ -431,7 +431,7 @@ let rewrite_sizeof (Defs defs) = let sizeof = E_aux (E_sizeof nexp, (l, Some (env, atom_typ nexp, no_effect))) in (try rewrite_trivial_sizeof_exp sizeof with | Type_error (l, err) -> - raise (Reporting_basic.err_typ l (string_of_type_error err))) + raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))) (* If the type variable is Not_found then it was probably introduced by a P_var pattern, so it likely exists as a variable in scope. It can't be an existential because the assert rules that out. *) @@ -642,7 +642,7 @@ let rewrite_sizeof (Defs defs) = (Bindings.empty, []) defs in let defs = List.map (rewrite_sizeof_valspec params_map) defs in (* Defs defs *) - fst (check initial_env (Defs defs)) + fst (Type_error.check initial_env (Defs defs)) let rewrite_defs_remove_assert defs = let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with @@ -1667,7 +1667,7 @@ let rewrite_defs_exp_lift_assign defs = rewrite_defs_base write_reg_ref (vector_access (GPR, i)) exp *) let rewrite_register_ref_writes (Defs defs) = - let (Defs write_reg_spec) = fst (check Env.empty (Defs (List.map gen_vs + let (Defs write_reg_spec) = fst (Type_error.check Env.empty (Defs (List.map gen_vs [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in let lexp_ref_exp (LEXP_aux (_, annot) as lexp) = try @@ -1902,7 +1902,7 @@ let rewrite_defs_early_return (Defs defs) = FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, List.map (rewrite_funcl_early_return rewriters) funcls), a) in - let (Defs early_ret_spec) = fst (check Env.empty (Defs [gen_vs + let (Defs early_ret_spec) = fst (Type_error.check Env.empty (Defs [gen_vs ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in rewrite_defs_base @@ -2366,7 +2366,7 @@ let rewrite_vector_concat_assignments defs = begin try check_exp env e_aux unit_typ with | Type_error (l, err) -> - raise (Reporting_basic.err_typ l (string_of_type_error err)) + raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) end else E_aux (e_aux, annot) | _ -> E_aux (e_aux, annot) @@ -2392,7 +2392,7 @@ let rewrite_tuple_assignments defs = begin try check_exp env let_exp unit_typ with | Type_error (l, err) -> - raise (Reporting_basic.err_typ l (string_of_type_error err)) + raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) end | _ -> E_aux (e_aux, annot) in @@ -3349,7 +3349,8 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | E_for(id,exp1,exp2,exp3,order,exp4) -> (* Translate for loops into calls to one of the foreach combinators. The loop body becomes a function of the loop variable and any - mutable local variables that are updated inside the loop. + mutable local variables that are updated inside the loop and + are used after or within the loop. Since the foreach* combinators are higher-order functions, they cannot be represented faithfully in the AST. The following code abuses the parameters of an E_app node, embedding the loop body @@ -3358,7 +3359,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = function and passed to foreach*. *) let vars, varpats = find_updated_vars exp4 - |> IdSet.inter used_vars + |> IdSet.inter (IdSet.union used_vars (find_used_vars full_exp)) |> mk_var_exps_pats pl env in let exp4 = rewrite_var_updates (add_vars overwrite exp4 vars) in @@ -3414,9 +3415,11 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body])) el env (typ_of body)) in Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats)) | E_loop(loop,cond,body) -> + (* Find variables that might be updated in the loop body and are used + either after or within the loop. *) let vars, varpats = find_updated_vars body - |> IdSet.inter used_vars + |> IdSet.inter (IdSet.union used_vars (find_used_vars full_exp)) |> mk_var_exps_pats pl env in let body = rewrite_var_updates (add_vars overwrite body vars) in @@ -3659,7 +3662,7 @@ let rewrite_defs_remove_superfluous_returns = let rewrite_defs_remove_e_assign (Defs defs) = - let (Defs loop_specs) = fst (check Env.empty (Defs (List.map gen_vs + let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs [("foreach", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars"); ("while", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); ("until", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in @@ -3894,7 +3897,7 @@ let rewrite_defs_realise_mappings (Defs defs) = in Defs (List.map rewrite_def defs |> List.flatten) -let recheck_defs defs = fst (check initial_env defs) +let recheck_defs defs = fst (Type_error.check initial_env defs) let remove_mapping_valspecs (Defs defs) = let allowed_def def = @@ -4012,7 +4015,7 @@ let rewrite_check_annot = else ()); exp with - Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err)) + Type_error (l, err) -> raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) in let check_pat pat = prerr_endline ("CHECKING PAT: " ^ string_of_pat pat ^ " : " ^ string_of_typ (pat_typ_of pat)); diff --git a/src/sail.ml b/src/sail.ml index f459d774..36b4efd8 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -50,6 +50,8 @@ open Process_file +module Big_int = Nat_big_num + let lib = ref ([] : string list) let opt_file_out : string option ref = ref None let opt_interactive = ref false @@ -60,6 +62,7 @@ let opt_print_verbose = ref false let opt_print_lem_ast = ref false let opt_print_lem = ref false let opt_print_ocaml = ref false +let opt_ocaml_nobuild = ref false let opt_print_c = ref false let opt_print_latex = ref false let opt_print_coq = ref false @@ -88,6 +91,9 @@ let options = Arg.align ([ ( "-ocaml", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); + ( "-ocaml-nobuild", + Arg.Set Ocaml_backend.opt_ocaml_nobuild, + " do not build generated ocaml"); ( "-ocaml_trace", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml], " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"); @@ -103,10 +109,16 @@ let options = Arg.align ([ ( "-O", Arg.Tuple [Arg.Set C_backend.optimize_primops; Arg.Set C_backend.optimize_hoist_allocations; - (* Arg.Set C_backend.optimize_enum_undefined; *) - (* Arg.Set C_backend.optimize_struct_undefined; *) + Arg.Set Initial_check.opt_fast_undefined; + Arg.Set Type_check.opt_no_effects; Arg.Set C_backend.optimize_struct_updates ], " turn on optimizations for C compilation"); + ( "-Oz3", + Arg.Set C_backend.optimize_z3, + " use z3 analysis for optimization (experimental)"); + ( "-Oconstant_fold", + Arg.Set Constant_fold.optimize_constant_fold, + " Apply constant folding optimizations"); ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); @@ -128,6 +140,9 @@ let options = Arg.align ([ ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), "<filename> provide additional library to open in Coq output"); + ( "-dcoq_undef_axioms", + Arg.Set Pretty_print_coq.opt_undef_axioms, + "Generate axioms for functions that are declared but not defined"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix), " set a custom prefix for generated latex command (default sail)"); @@ -275,6 +290,8 @@ let main() = let open Elf_loader in let chan = open_out out in load_elf ~writer:(write_file chan) elf; + output_string chan "elf_entry\n"; + output_string chan (Big_int.to_string !opt_elf_entry ^ "\n"); close_out chan; exit 0 end diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 665ff3af..89056347 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -52,7 +52,7 @@ let trace_call str = type bit = B0 | B1 let eq_bit (a, b) = a = b - + let and_bit = function | B1, B1 -> B1 | _, _ -> B0 @@ -400,55 +400,85 @@ let rec bits_of_int bit n = let byte_of_int n = bits_of_int 128 n -module BigIntHash = - struct - type t = Big_int.num - let equal i j = Big_int.equal i j - let hash i = Hashtbl.hash i - end +module Mem = struct + include Map.Make(struct + type t = Big_int.num + let compare = Big_int.compare + end) +end -module RAM = Hashtbl.Make(BigIntHash) +let mem_pages = (ref Mem.empty : (Bytes.t Mem.t) ref);; -let ram : int RAM.t = RAM.create 256 +let page_shift_bits = 20 (* 1M page *) +let page_size_bytes = 1 lsl page_shift_bits;; -let write_ram' (addr_size, data_size, hex_ram, addr, data) = - let data = List.map (fun byte -> Big_int.to_int (uint byte)) (break 8 data) in - let rec write_byte i byte = - trace (Printf.sprintf "Store: %s 0x%02X" (Big_int.to_string (Big_int.add addr (Big_int.of_int i))) byte); - RAM.add ram (Big_int.add addr (Big_int.of_int i)) byte - in - List.iteri write_byte (List.rev data) +let page_no_of_addr a = Big_int.shift_right a page_shift_bits +let bottom_addr_of_page p = Big_int.shift_left p page_shift_bits +let top_addr_of_page p = Big_int.shift_left (Big_int.succ p) page_shift_bits +let get_mem_page p = + try + Mem.find p !mem_pages + with Not_found -> + let new_page = Bytes.create page_size_bytes in + mem_pages := Mem.add p new_page !mem_pages; + new_page + +let rec add_mem_bytes addr buf off len = + let page_no = page_no_of_addr addr in + let page_bot = bottom_addr_of_page page_no in + let page_top = top_addr_of_page page_no in + let page_off = Big_int.to_int (Big_int.sub addr page_bot) in + let page = get_mem_page page_no in + let bytes_left_in_page = Big_int.sub page_top addr in + let to_copy = min (Big_int.to_int bytes_left_in_page) len in + Bytes.blit buf off page page_off to_copy; + if (to_copy < len) then + add_mem_bytes page_top buf (off + to_copy) (len - to_copy) + +let rec read_mem_bytes addr len = + let page_no = page_no_of_addr addr in + let page_bot = bottom_addr_of_page page_no in + let page_top = top_addr_of_page page_no in + let page_off = Big_int.to_int (Big_int.sub addr page_bot) in + let page = get_mem_page page_no in + let bytes_left_in_page = Big_int.sub page_top addr in + let to_get = min (Big_int.to_int bytes_left_in_page) len in + let bytes = Bytes.sub page page_off to_get in + if to_get >= len then + bytes + else + Bytes.cat bytes (read_mem_bytes page_top (len - to_get)) + +let write_ram' (data_size, addr, data) = + let len = Big_int.to_int data_size in + let bytes = Bytes.create len in begin + List.iteri (fun i byte -> Bytes.set bytes (len - i - 1) (char_of_int (Big_int.to_int (uint byte)))) (break 8 data); + add_mem_bytes addr bytes 0 len + end let write_ram (addr_size, data_size, hex_ram, addr, data) = - write_ram' (addr_size, data_size, hex_ram, uint addr, data) + write_ram' (data_size, uint addr, data) let wram addr byte = - RAM.add ram addr byte + let bytes = Bytes.make 1 (char_of_int byte) in + add_mem_bytes addr bytes 0 1 let read_ram (addr_size, data_size, hex_ram, addr) = let addr = uint addr in - let rec read_byte i = - if Big_int.equal i Big_int.zero - then [] - else - begin - let loc = Big_int.sub (Big_int.add addr i) (Big_int.of_int 1) in - let byte = try RAM.find ram loc with Not_found -> 0 in - trace (Printf.sprintf "Load: %s 0x%02X" (Big_int.to_string loc) byte); - byte_of_int byte @ read_byte (Big_int.sub i (Big_int.of_int 1)) - end - in - read_byte data_size - -let tag_ram : bool RAM.t = RAM.create 256 + let bytes = read_mem_bytes addr (Big_int.to_int data_size) in + let vector = ref [] in + Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes; + !vector +let tag_ram = (ref Mem.empty : (bool Mem.t) ref);; + let write_tag_bool (addr, tag) = let addri = uint addr in - RAM.add tag_ram addri tag + tag_ram := Mem.add addri tag !tag_ram let read_tag_bool addr = let addri = uint addr in - try RAM.find tag_ram addri with Not_found -> false + try Mem.find addri !tag_ram with Not_found -> false let rec reverse_endianness bits = if List.length bits <= 8 then bits else @@ -503,8 +533,8 @@ let gteq_real (x, y) = Rational.geq x y let to_real x = Rational.of_int (Big_int.to_int x) (* FIXME *) let negate_real x = Rational.neg x -let round_down x = failwith "round_down" (* Num.big_int_of_num (Num.floor_num x) *) -let round_up x = failwith "round_up" (* Num.big_int_of_num (Num.ceiling_num x) *) +let round_down x = Rational.floor x (* Num.big_int_of_num (Num.floor_num x) *) +let round_up x = Rational.ceiling x (* Num.big_int_of_num (Num.ceiling_num x) *) let quotient_real (x, y) = Rational.div x y let mult_real (x, y) = Rational.mul x y (* Num.mult_num x y *) let real_power (x, y) = failwith "real_power" (* Num.power_num x (Num.num_of_big_int y) *) @@ -534,15 +564,13 @@ let rec pow x = function | n -> x * pow x (n - 1) let real_of_string str = - let rat_of_string sr = Rational.of_int (int_of_string str) in - try - let point = String.index str '.' in - let whole = Rational.of_int (int_of_string (String.sub str 0 point)) in - let frac_str = String.sub str (point + 1) (String.length str - (point + 1)) in - let frac = Rational.div (rat_of_string frac_str) (Rational.of_int (pow 10 (String.length frac_str))) in - Rational.add whole frac - with - | Not_found -> Rational.of_int (int_of_string str) + match Util.split_on_char '.' str with + | [whole; frac] -> + let whole = Rational.of_int (int_of_string whole) in + let frac = Rational.div (Rational.of_int (int_of_string frac)) (Rational.of_int (pow 10 (String.length frac))) in + Rational.add whole frac + | [whole] -> Rational.of_int (int_of_string str) + | _ -> failwith "invalid real literal" (* Not a very good sqrt implementation *) let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *) @@ -550,12 +578,21 @@ let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt let print_int (str, x) = print_endline (str ^ Big_int.to_string x) +let prerr_int (str, x) = + prerr_endline (str ^ Big_int.to_string x) + let print_bits (str, xs) = print_endline (str ^ string_of_bits xs) +let prerr_bits (str, xs) = + prerr_endline (str ^ string_of_bits xs) + let print_string(str, msg) = print_endline (str ^ msg) +let prerr_string(str, msg) = + prerr_endline (str ^ msg) + let reg_deref r = !r let string_of_zbit = function @@ -713,3 +750,30 @@ let hex_bits_32_matches_prefix s = ZSome ((bits_of_int 2147483648 n, len)) else ZNone () + +let string_of_bool = function + | true -> "true" + | false -> "false" + +let dec_str x = Big_int.to_string x + +let hex_str x = Big_int.to_string x + +let trace_memory_write (_, _, _) = () +let trace_memory_read (_, _, _) = () + +let sleep_request () = () + +let load_raw (paddr, file) = + let i = ref 0 in + let paddr = uint paddr in + let in_chan = open_in file in + try + while true do + let byte = input_char in_chan |> Char.code in + wram (Big_int.add paddr (Big_int.of_int !i)) byte; + incr i + done + with + | End_of_file -> () + diff --git a/src/specialize.ml b/src/specialize.ml index 191ee3be..0090cdfd 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -335,12 +335,13 @@ let specialize_id_fundef instantiations id ast = let spec_id = id_of_instantiation id instantiation in if IdSet.mem spec_id !spec_ids then [] else begin + prerr_endline ("specialised fundef " ^ string_of_id id ^ " to " ^ string_of_id spec_id); spec_ids := IdSet.add spec_id !spec_ids; [DEF_fundef (rename_fundef spec_id fundef)] end in let fundefs = List.map specialize_fundef instantiations |> List.concat in - append_ast pre_ast (append_ast (Defs fundefs) post_ast) + append_ast pre_ast (append_ast (Defs (DEF_fundef fundef :: fundefs)) post_ast) | Some _ -> assert false (* unreachable *) let specialize_id_overloads instantiations id (Defs defs) = @@ -380,8 +381,11 @@ let remove_unused_valspecs env ast = let rec remove_unused (Defs defs) id = match defs with - | def :: defs when is_fundef id def -> remove_unused (Defs defs) id + | def :: defs when is_fundef id def -> + prerr_endline ("Removing fundef: " ^ string_of_id id); + remove_unused (Defs defs) id | def :: defs when is_valspec id def -> + prerr_endline ("Removing valspec: " ^ string_of_id id); remove_unused (Defs defs) id | DEF_overload (overload_id, overloads) :: defs -> begin @@ -396,7 +400,9 @@ let remove_unused_valspecs env ast = List.fold_left (fun ast id -> Defs (remove_unused ast id)) ast (IdSet.elements unused) let specialize_id id ast = + prerr_endline ("specialising: " ^ string_of_id id); let instantiations = instantiations_of id ast in + List.iter (fun i -> prerr_endline (string_of_instantiation i)) instantiations; let ast = specialize_id_valspec instantiations id ast in let ast = specialize_id_fundef instantiations id ast in @@ -423,9 +429,11 @@ let reorder_typedefs (Defs defs) = let specialize_ids ids ast = let ast = List.fold_left (fun ast id -> specialize_id id ast) ast (IdSet.elements ids) in let ast = reorder_typedefs ast in - let ast, _ = Type_check.check Type_check.initial_env ast in - let ast = List.fold_left (fun ast id -> rewrite_polymorphic_calls id ast) ast (IdSet.elements ids) in - let ast, env = Type_check.check Type_check.initial_env ast in + let ast, _ = Type_error.check Type_check.initial_env ast in + let ast = + List.fold_left (fun ast id -> rewrite_polymorphic_calls id ast) ast (IdSet.elements ids) + in + let ast, env = Type_error.check Type_check.initial_env ast in let ast = remove_unused_valspecs env ast in ast, env @@ -519,9 +527,10 @@ let specialize_variants ((Defs defs) as ast) env = let ast = Defs (specialize_variants' defs) in let ast = List.fold_left (fun ast id -> rewrite_polymorphic_constructors id ast) ast !ctors in - Type_check.check Type_check.initial_env ast + Type_error.check Type_check.initial_env ast let rec specialize ast env = + prerr_endline (Util.log_line __MODULE__ __LINE__ "Performing specialisation pass"); let ids = polymorphic_functions (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt) ast in if IdSet.is_empty ids then specialize_variants ast env diff --git a/src/state.ml b/src/state.ml index ab63747c..c591f753 100644 --- a/src/state.ml +++ b/src/state.ml @@ -366,11 +366,11 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = let id = remove_leading_underscores (string_of_id id) in let id' = remove_trailing_underscores id in separate_map hardline string [ - "lemma liftS_read_reg_" ^ id ^ "[simp]:"; + "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:"; " \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\""; " by (auto simp: liftState_read_reg_readS register_defs)"; ""; - "lemma liftS_write_reg_" ^ id ^ "[simp]:"; + "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; " \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\""; " by (auto simp: liftState_write_reg_updateS register_defs)" ] @@ -510,5 +510,5 @@ let generate_regstate_defs mwords defs = defs let add_regstate_defs mwords env (Defs defs) = - let reg_defs, env = check env (generate_regstate_defs mwords defs) in + let reg_defs, env = Type_error.check env (generate_regstate_defs mwords defs) in env, append_ast (Defs defs) reg_defs diff --git a/src/type_check.ml b/src/type_check.ml index 5c062b57..66e5e656 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -84,50 +84,13 @@ type type_error = (* First parameter is the error that caused us to start doing type coercions, the second is the errors encountered by all possible coercions *) - | Err_no_casts of unit exp * type_error * type_error list + | Err_no_casts of unit exp * typ * typ * type_error * type_error list | Err_no_overloading of id * (id * type_error) list | Err_unresolved_quants of id * quant_item list - | Err_subtype of typ * typ * n_constraint list + | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t | Err_no_num_ident of id | Err_other of string -let pp_type_error err = - let open PPrint in - let rec pp_err = function - | Err_no_casts (exp, trigger, []) -> - (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp) - ^^ hardline ^^ (string "Failed because" ^//^ pp_err trigger) - | Err_no_casts (exp, trigger, errs) -> - (string "Tried performing type coercion on" ^//^ Pretty_print_sail.doc_exp exp) - ^/^ string "Failed because" ^//^ pp_err trigger - | Err_no_overloading (id, errs) -> - string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^ - group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^//^ pp_err err) errs) - | Err_subtype (typ1, typ2, []) -> - separate space [ string (string_of_typ typ1); - string "is not a subtype of"; - string (string_of_typ typ2) ] - | Err_subtype (typ1, typ2, constrs) -> - separate space [ string (string_of_typ typ1); - string "is not a subtype of"; - string (string_of_typ typ2) ] - ^/^ string "in context" - ^//^ string (string_of_list ", " string_of_n_constraint constrs) - | Err_no_num_ident id -> - string "No num identifier" ^^ space ^^ string (string_of_id id) - | Err_unresolved_quants (id, quants) -> - string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id) - ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants) - | Err_other str -> string str - in - pp_err err - -let rec string_of_type_error err = - let open PPrint in - let b = Buffer.create 20 in - ToBuffer.pretty 1. 120 b (pp_type_error err); - "\n" ^ Buffer.contents b - exception Type_error of l * type_error;; let typ_error l m = raise (Type_error (l, Err_other m)) @@ -420,8 +383,10 @@ module Env : sig val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t val get_typ_var : kid -> t -> base_kind_aux + val get_typ_var_loc : kid -> t -> Ast.l val get_typ_vars : t -> base_kind_aux KBindings.t - val add_typ_var : kid -> base_kind_aux -> t -> t + val get_typ_var_locs : t -> Ast.l KBindings.t + val add_typ_var : l -> kid -> base_kind_aux -> t -> t val get_ret_typ : t -> typ option val add_ret_typ : typ -> t -> t val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t @@ -481,7 +446,7 @@ end = struct registers : typ Bindings.t; variants : (typquant * type_union list) Bindings.t; mappings : (typquant * typ * typ) Bindings.t; - typ_vars : base_kind_aux KBindings.t; + typ_vars : (Ast.l * base_kind_aux) KBindings.t; typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; num_defs : nexp Bindings.t; overloads : (id list) Bindings.t; @@ -535,10 +500,15 @@ end = struct let set_allow_unknowns b env = { env with allow_unknowns = b } let get_typ_var kid env = - try KBindings.find kid env.typ_vars with + try snd (KBindings.find kid env.typ_vars) with + | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) + + let get_typ_var_loc kid env = + try fst (KBindings.find kid env.typ_vars) with | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) - let get_typ_vars env = env.typ_vars + let get_typ_vars env = KBindings.map snd env.typ_vars + let get_typ_var_locs env = KBindings.map fst env.typ_vars let bk_counter = ref 0 let bk_name () = let kid = mk_kid ("bk#" ^ string_of_int !bk_counter) in incr bk_counter; kid @@ -668,10 +638,13 @@ end = struct let rename_kid kid = if KBindings.mem kid env.typ_vars then prepend_kid "syn#" kid else kid in let add_typ_var env kid = - if KBindings.mem kid env.typ_vars then - (rebindings := kid :: !rebindings; { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) BK_int env.typ_vars }) - else - { env with typ_vars = KBindings.add kid BK_int env.typ_vars } + try + let (l, _) = KBindings.find kid env.typ_vars in + rebindings := kid :: !rebindings; + { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, BK_int) env.typ_vars } + with + | Not_found -> + { env with typ_vars = KBindings.add kid (l, BK_int) env.typ_vars } in let env = List.fold_left add_typ_var env kids in @@ -708,7 +681,7 @@ end = struct let complex_nexps = ref KBindings.empty in let simplify_nexp (Nexp_aux (nexp_aux, l) as nexp) = match nexp_aux with - | Nexp_var _ | Nexp_constant _ -> nexp + | Nexp_constant _ -> nexp (* Check this ? *) | _ -> let kid = Kid_aux (Var ("'c#" ^ string_of_int !counter), l) in complex_nexps := KBindings.add kid nexp !complex_nexps; @@ -725,7 +698,7 @@ end = struct let counter = ref 0 in let simplify_nexp (Nexp_aux (nexp_aux, l) as nexp) = match nexp_aux with - | Nexp_var _ | Nexp_constant _ -> nexp + | Nexp_constant _ -> nexp | _ -> (incr counter; nexp) in let typ = map_nexps simplify_nexp typ in @@ -760,8 +733,14 @@ end = struct then typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq) else () | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id) - | Typ_var kid when KBindings.mem kid env.typ_vars -> () - | Typ_var kid -> typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) + | Typ_var kid -> begin + match KBindings.find kid env.typ_vars with + | (_, BK_type) -> () + | (_, k) -> typ_error l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ + ^ " is " ^ string_of_base_kind_aux k ^ " rather than Type") + | exception Not_found -> + typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) + end | Typ_fn (typ_arg, typ_ret, effs) -> wf_typ ~exs:exs env typ_arg; wf_typ ~exs:exs env typ_ret | Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 -> typ_error l "Bidirectional types cannot be the same on both sides" @@ -850,7 +829,7 @@ end = struct let get_val_spec id env = try let bind = Bindings.find id env.top_val_specs in - typ_debug (lazy ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, bk) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars))); + typ_debug (lazy ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, (_, bk)) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars))); let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in typ_debug (lazy ("get_val_spec: freshened to " ^ string_of_bind bind')); bind' @@ -1083,13 +1062,13 @@ end = struct end end - let add_typ_var kid k env = + let add_typ_var l kid k env = if KBindings.mem kid env.typ_vars then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound") else begin typ_print (lazy ("Adding kind identifier " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k)); - { env with typ_vars = KBindings.add kid k env.typ_vars } + { env with typ_vars = KBindings.add kid (l, k) env.typ_vars } end let add_num_def id nexp env = @@ -1185,13 +1164,13 @@ end = struct } end -let add_typquant (quant : typquant) (env : Env.t) : Env.t = +let add_typquant l (quant : typquant) (env : Env.t) : Env.t = let rec add_quant_item env = function | QI_aux (qi, _) -> add_quant_item_aux env qi and add_quant_item_aux env = function | QI_const constr -> Env.add_constraint constr env - | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var kid BK_int env - | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var kid k env + | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var l kid BK_int env + | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var l kid k env | QI_id (KOpt_aux (_, l)) -> typ_error l "Type variable had non base kinds!" in match quant with @@ -1220,11 +1199,11 @@ let destruct_exist env typ = Some (List.map snd fresh_kids, nc, typ) | _ -> None -let add_existential kids nc env = - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids in +let add_existential l kids nc env = + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids in Env.add_constraint nc env -let add_typ_vars kids env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids +let add_typ_vars l kids env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids let is_exist = function | Typ_aux (Typ_exist (_, _, _), _) -> true @@ -1263,16 +1242,16 @@ let destruct_numeric env typ = let bind_numeric l typ env = match destruct_numeric env typ with | Some (kids, nc, nexp) -> - nexp, add_existential kids nc env + nexp, add_existential l kids nc env | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric") (** Pull an (potentially)-existentially qualified type into the global typing environment **) -let bind_existential typ env = +let bind_existential l typ env = match destruct_numeric env typ with - | Some (kids, nc, nexp) -> atom_typ nexp, add_existential kids nc env + | Some (kids, nc, nexp) -> atom_typ nexp, add_existential l kids nc env | None -> match destruct_exist env typ with - | Some (kids, nc, typ) -> typ, add_existential kids nc env + | Some (kids, nc, typ) -> typ, add_existential l kids nc env | None -> typ, env let destruct_range env typ = @@ -1414,7 +1393,7 @@ let solve env nexp = try KBindings.find kid !bindings with | Not_found -> fresh_var kid in - let env = Env.add_typ_var (mk_kid "solve#") BK_int env in + let env = Env.add_typ_var Parse_ast.Unknown (mk_kid "solve#") BK_int env in let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (nc_constraint env var_of (nc_eq (nvar (mk_kid "solve#")) nexp)) in @@ -1914,11 +1893,11 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t | _, _ when alpha_equivalent env typ1 typ2 -> () (* Special cases for two numeric (atom) types *) | Some (kids1, nc1, nexp1), Some ([], _, nexp2) -> - let env = add_existential kids1 nc1 env in - if prove env (nc_eq nexp1 nexp2) then () else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env)) + let env = add_existential l kids1 nc1 env in + if prove env (nc_eq nexp1 nexp2) then () else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env)) | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) -> - let env = add_existential kids1 nc1 env in - let env = add_typ_vars (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2))) env in + let env = add_existential l kids1 nc1 env in + let env = add_typ_vars l (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2))) env in let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in let env = Env.add_constraint (nc_eq nexp1 nexp2) env in let constr var_of = @@ -1926,16 +1905,14 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t (nc_constraint env var_of (nc_negate nc2)) in if prove_z3' env constr then () - else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env)) + else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env)) | _, _ -> match destruct_exist env typ1, unwrap_exist env (Env.canonicalize env typ2) with | Some (kids, nc, typ1), _ -> - let env = add_existential kids nc env in subtyp l env typ1 typ2 - (* | None, ([], _, typ2) -> - typ_error l (string_of_typ typ1 ^ " < " ^ string_of_typ typ2) *) + let env = add_existential l kids nc env in subtyp l env typ1 typ2 | None, (kids, nc, typ2) -> typ_debug (lazy "Subtype check with unification"); - let env = add_typ_vars kids env in + let env = add_typ_vars l kids env in let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in let unifiers, existential_kids, existential_nc = try unify l env typ2 typ1 with @@ -1946,7 +1923,7 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t let env = match existential_kids, existential_nc with | [], None -> env | _, Some enc -> - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env existential_kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env existential_kids in Env.add_constraint enc env | _, None -> assert false (* Cannot have existential_kids without existential_nc *) in @@ -1955,7 +1932,7 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t (nc_constraint env var_of (nc_negate nc)) in if prove_z3' env constr then () - else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env)) + else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env)) let typ_equality l env typ1 typ2 = subtyp l env typ1 typ2; subtyp l env typ2 typ1 @@ -2005,12 +1982,10 @@ let is_nat_kid kid = function let is_order_kid kid = function | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid'), _) -> Kid.compare kid kid' = 0 - | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0 | _ -> false let is_typ_kid kid = function | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid'), _) -> Kid.compare kid kid' = 0 - | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0 | _ -> false let rec instantiate_quants quants kid uvar = match quants with @@ -2152,18 +2127,25 @@ exception Not_a_constraint;; let rec assert_nexp env exp = destruct_atom_nexp env (typ_of exp) -let rec assert_constraint env (E_aux (exp_aux, _) as exp) = +let rec combine_constraint b f x y = match b, x, y with + | true, Some x, Some y -> Some (f x y) + | true, Some x, None -> Some x + | true, None, Some y -> Some y + | false, Some x, Some y -> Some (f x y) + | _, _, _ -> None + +let rec assert_constraint env b (E_aux (exp_aux, _) as exp) = match exp_aux with | E_constraint nc -> Some nc | E_lit (L_aux (L_true, _)) -> Some nc_true | E_lit (L_aux (L_false, _)) -> Some nc_false | E_let (_,e) -> - assert_constraint env e (* TODO: beware of fresh type vars *) + assert_constraint env b e (* TODO: beware of fresh type vars *) | E_app (op, [x; y]) when string_of_id op = "or_bool" -> - option_binop nc_or (assert_constraint env x) (assert_constraint env y) + combine_constraint (not b) nc_or (assert_constraint env b x) (assert_constraint env b y) | E_app (op, [x; y]) when string_of_id op = "and_bool" -> - option_binop nc_and (assert_constraint env x) (assert_constraint env y) + combine_constraint b nc_and (assert_constraint env b x) (assert_constraint env b y) | E_app (op, [x; y]) when string_of_id op = "gteq_atom" -> option_binop nc_gteq (assert_nexp env x) (assert_nexp env y) | E_app (op, [x; y]) when string_of_id op = "lteq_atom" -> @@ -2179,83 +2161,10 @@ let rec assert_constraint env (E_aux (exp_aux, _) as exp) = | _ -> None -type flow_constraint = - | Flow_lteq of Big_int.num * nexp - | Flow_gteq of Big_int.num * nexp - -let restrict_range_upper c1 nexp1 (Typ_aux (typ_aux, l) as typ) = - match typ_aux with - | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _); Typ_arg_aux (Typ_arg_nexp nexp2, _)]) - when string_of_id f = "range" -> - begin - match big_int_of_nexp nexp2 with - | Some c2 -> - let upper = if (Big_int.less c1 c2) then nexp1 else nexp2 in - range_typ nexp upper - | _ -> typ - end - | _ -> typ - -let restrict_range_lower c1 nexp1 (Typ_aux (typ_aux, l) as typ) = - match typ_aux with - | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp2, _); Typ_arg_aux (Typ_arg_nexp nexp, _)]) - when string_of_id f = "range" -> - begin - match big_int_of_nexp nexp2 with - | Some c2 -> - let lower = if (Big_int.greater c1 c2) then nexp1 else nexp2 in - range_typ lower nexp - | _ -> typ - end - | _ -> typ - -let apply_flow_constraint = function - | Flow_lteq (c, nexp) -> - (restrict_range_upper c nexp, - restrict_range_lower (Big_int.succ c) (nexp_simp (nsum nexp (nint 1)))) - | Flow_gteq (c, nexp) -> - (restrict_range_lower c nexp, - restrict_range_upper (Big_int.pred c) (nexp_simp (nminus nexp (nint 1)))) - -let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = - match exp_aux with - | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lt_range_atom" -> - let kid = Env.fresh_kid env in - begin - match destruct_atom (typ_of y) with - | Some (c, nexp) -> - [(v, Flow_lteq (Big_int.pred c, nexp_simp (nminus nexp (nint 1))))], [] - | _ -> [], [] - end - | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lteq_range_atom" -> - let kid = Env.fresh_kid env in - begin - match destruct_atom (typ_of y) with - | Some (c, nexp) -> [(v, Flow_lteq (c, nexp))], [] - | _ -> [], [] - end - | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gt_range_atom" -> - let kid = Env.fresh_kid env in - begin - match destruct_atom (typ_of y) with - | Some (c, nexp) -> - [(v, Flow_gteq (Big_int.succ c, nexp_simp (nsum nexp (nint 1))))], [] - | _ -> [], [] - end - | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gteq_range_atom" -> - let kid = Env.fresh_kid env in - begin - match destruct_atom (typ_of y) with - | Some (c, nexp) -> [(v, Flow_gteq (c, nexp))], [] - | _ -> [], [] - end - | _ -> [], option_these [assert_constraint env exp] - -let rec add_flows b flows env = - match flows with - | [] -> env - | (id, flow) :: flows when b -> add_flows true flows (Env.add_flow id (fst (apply_flow_constraint flow)) env) - | (id, flow) :: flows -> add_flows false flows (Env.add_flow id (snd (apply_flow_constraint flow)) env) +let rec add_opt_constraint constr env = + match constr with + | None -> env + | Some constr -> Env.add_constraint constr env let rec add_constraints constrs env = List.fold_left (fun env constr -> Env.add_constraint constr env) env constrs @@ -2357,7 +2266,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | ((E_aux (E_assert (constr_exp, assert_msg), _) as exp) :: exps) -> let constr_exp = crule check_exp env constr_exp bool_typ in let checked_msg = crule check_exp env assert_msg string_typ in - let env = match assert_constraint env constr_exp with + let env = match assert_constraint env true constr_exp with | Some nc -> typ_print (lazy ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert")); Env.add_constraint nc env @@ -2461,11 +2370,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ typ_print (lazy("Trying forwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); begin try crule check_exp env (E_aux (E_app (forwards_id, xs), (l, ()))) typ with | Type_error (_, err1) -> - typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); + (* typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); *) typ_print (lazy ("Trying backwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); begin try crule check_exp env (E_aux (E_app (backwards_id, xs), (l, ()))) typ with | Type_error (_, err2) -> - typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); + (* typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); *) typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)])) end end @@ -2476,7 +2385,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); try crule check_exp env (E_aux (E_app (f, xs), (l, ()))) typ with | Type_error (_, err) -> - typ_print (lazy ("Error : " ^ string_of_type_error err)); + typ_debug (lazy "Error"); try_overload (errs @ [(f, err)], fs) end in @@ -2495,9 +2404,8 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ type_coercion env inferred_exp typ | E_if (cond, then_branch, else_branch), _ -> let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in - let flows, constrs = infer_flow env cond' in - let then_branch' = crule check_exp (add_constraints constrs (add_flows true flows env)) then_branch typ in - let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch typ in + let then_branch' = crule check_exp (add_opt_constraint (assert_constraint env true cond') env) then_branch typ in + let else_branch' = crule check_exp (add_opt_constraint (option_map nc_negate (assert_constraint env false cond')) env) else_branch typ in annot_exp (E_if (cond', then_branch', else_branch')) typ | E_exit exp, _ -> let checked_exp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in @@ -2529,7 +2437,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let env = match bind_exp with | E_aux (E_assert (constr_exp, _), _) -> begin - match assert_constraint env constr_exp with + match assert_constraint env true constr_exp with | Some nc -> typ_print (lazy ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert")); Env.add_constraint nc env @@ -2569,8 +2477,7 @@ and check_case env pat_typ pexp typ = | None -> None, env | Some guard -> let checked_guard = check_exp env guard bool_typ in - let flows, constrs = infer_flow env checked_guard in - Some checked_guard, add_constraints constrs (add_flows true flows env) + Some checked_guard, add_opt_constraint (assert_constraint env true checked_guard) env in let checked_case = crule check_exp env' case typ in construct_pexp (tpat, checked_guard, checked_case, (l, None)) @@ -2604,8 +2511,7 @@ and check_mpexp other_env env mpexp typ = | None -> None, env | Some guard -> let checked_guard = check_exp env guard bool_typ in - let flows, constrs = infer_flow env checked_guard in - Some checked_guard, add_constraints constrs (add_flows true flows env) + Some checked_guard, env in construct_mpexp (checked_mpat, checked_guard, (l, None)) @@ -2623,7 +2529,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = | _ -> failwith "Cannot switch type for unannotated function" in let rec try_casts trigger errs = function - | [] -> typ_raise l (Err_no_casts (strip_exp annotated_exp, trigger, errs)) + | [] -> typ_raise l (Err_no_casts (strip_exp annotated_exp, typ_of annotated_exp, typ, trigger, errs)) | (cast :: casts) -> begin typ_print (lazy ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ)); try @@ -2685,7 +2591,7 @@ and bind_pat_no_guard env (P_aux (_,(l,_)) as pat) typ = | tpat, env, [] -> tpat, env and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) = - let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in + let (Typ_aux (typ_aux, _) as typ), env = bind_existential l typ env in typ_print (lazy ("Binding " ^ string_of_pat pat ^ " to " ^ string_of_typ typ)); let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in let switch_typ pat typ = match pat with @@ -2966,7 +2872,7 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _) begin match typ_nexps typ with | [nexp] -> - Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_int env) + Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env) | [] -> typ_error l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to") | nexps -> @@ -2979,7 +2885,7 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_arg_aux (typ_ match typ_pat_aux, typ_arg_aux with | TP_wild, _ -> env | TP_var kid, Typ_arg_nexp nexp -> - Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_int env) + Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env) | _, Typ_arg_typ typ -> bind_typ_pat env typ_pat typ | _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order" | _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat) @@ -3268,11 +3174,11 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = typ_print (lazy ("Trying forwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); begin try irule infer_exp env (E_aux (E_app (forwards_id, xs), (l, ()))) with | Type_error (_, err1) -> - typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); + (* typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); *) typ_print (lazy ("Trying backwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); begin try irule infer_exp env (E_aux (E_app (backwards_id, xs), (l, ()))) with | Type_error (_, err2) -> - typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); + (* typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); *) typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)])) end end @@ -3283,7 +3189,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); try irule infer_exp env (E_aux (E_app (f, xs), (l, ()))) with | Type_error (_, err) -> - typ_print (lazy ("Error : " ^ string_of_type_error err)); + typ_debug (lazy "Error"); try_overload (errs @ [(f, err)], fs) end in @@ -3291,8 +3197,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_app (f, xs) -> infer_funapp l env f xs None | E_loop (loop_type, cond, body) -> let checked_cond = crule check_exp env cond bool_typ in - let flows, constrs = infer_flow env checked_cond in - let checked_body = crule check_exp (add_flows true flows env) body unit_typ in + let checked_body = crule check_exp (add_opt_constraint (assert_constraint env true checked_cond) env) body unit_typ in annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin @@ -3307,7 +3212,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) -> let loop_kid = mk_kid ("loop_" ^ string_of_id v) in - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env (loop_kid :: kids1 @ kids2) in + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env (loop_kid :: kids1 @ kids2) in let env = Env.add_constraint (nc_and nc1 nc2) env in let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in let loop_vtyp = atom_typ (nvar loop_kid) in @@ -3319,9 +3224,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = end | E_if (cond, then_branch, else_branch) -> let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in - let flows, constrs = infer_flow env cond' in - let then_branch' = irule infer_exp (add_constraints constrs (add_flows true flows env)) then_branch in - let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch (typ_of then_branch') in + let then_branch' = irule infer_exp (add_opt_constraint (assert_constraint env true cond') env) then_branch in + let else_branch' = crule check_exp (add_opt_constraint (option_map nc_negate (assert_constraint env false cond')) env) else_branch (typ_of then_branch') in annot_exp (E_if (cond', then_branch', else_branch')) (typ_of then_branch') | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ()))) | E_vector_update (v, n, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, ()))) @@ -3356,7 +3260,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let env = match bind_exp with | E_aux (E_assert (constr_exp, _), _) -> begin - match assert_constraint env constr_exp with + match assert_constraint env true constr_exp with | Some nc -> typ_print (lazy ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert")); Env.add_constraint nc env @@ -3459,7 +3363,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = | [], None -> env | _, Some enc -> let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in - let env = List.fold_left (fun env kid -> Env.add_typ_var (prepend_kid ex_tag kid) BK_int env) env ex_kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var l (prepend_kid ex_tag kid) BK_int env) env ex_kids in Env.add_constraint enc env | _, None -> assert false (* Cannot have ex_kids without ex_nc *) in @@ -3495,7 +3399,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers))); if ex_kids = [] then () else (typ_debug (lazy ("EX GOAL: " ^ string_of_option string_of_n_constraint ex_nc)); ex_goal := ex_nc); record_unifiers unifiers; - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env ex_kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env ex_kids in let typs' = List.map (subst_unifiers unifiers) typs in let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in let ret_typ' = @@ -3553,7 +3457,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = exp, !all_unifiers and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as typ) = - let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in + let (Typ_aux (typ_aux, _) as typ), env = bind_existential l typ env in typ_print (lazy ("Binding " ^ string_of_mpat mpat ^ " to " ^ string_of_typ typ)); let annot_mpat mpat typ = MP_aux (mpat, (l, Some (env, typ, no_effect))) in let switch_typ mpat typ = match mpat with @@ -4309,7 +4213,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) in check_tannotopt env quant vtyp_ret tannotopt; typ_debug (lazy ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ))); - let funcl_env = add_typquant quant env in + let funcl_env = add_typquant l quant env in let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in let eff = List.fold_left union_effects no_effect (List.map funcl_effect funcls) in let vs_def, env, declared_eff = @@ -4354,7 +4258,7 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md else [], env in - let mapcl_env = add_typquant quant env in + let mapcl_env = add_typquant l quant env in let mapcls = List.map (fun mapcl -> check_mapcl mapcl_env mapcl typ) mapcls in let eff = List.fold_left union_effects no_effect (List.map mapcl_effect mapcls) in let env = Env.define_val_spec id env in @@ -4376,7 +4280,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) = | Some op, None -> Env.add_smt_op id op env | _, _ -> env in - Env.wf_typ (add_typquant quants env) typ; + Env.wf_typ (add_typquant l quants env) typ; typ_debug (lazy "CHECKED WELL-FORMED VAL SPEC"); let env = (* match ext_opt with @@ -4392,7 +4296,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) = | Typ_aux (Typ_fn (_,_,eff),_) -> eff | _ -> no_effect in - [annotate vs typ eff], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant quants env) typ) env + [annotate vs typ eff], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant l quants env) typ) env let check_default env (DT_aux (ds, l)) = match ds with @@ -4495,7 +4399,7 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t = Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id b, _)), _)]), _) when string_of_id v = "vector" && string_of_id b = "bit" -> let size = Big_int.to_int size in - let (Defs defs), env = check' env (Bitfield.macro id size order ranges) in + let (Defs defs), env = check env (Bitfield.macro id size order ranges) in defs, env | _ -> typ_error l "Bad bitfield type" @@ -4532,20 +4436,15 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = let defs, env = check_def env def in List.map (fun def -> DEF_comm (DC_comm_struct def)) defs, env -and check' : 'a. Env.t -> 'a defs -> tannot defs * Env.t = +and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = fun env (Defs defs) -> match defs with | [] -> (Defs []), env | def :: defs -> let (def, env) = check_def env def in - let (Defs defs, env) = check' env (Defs defs) in + let (Defs defs, env) = check env (Defs defs) in (Defs (def @ defs)), env -let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = - fun env defs -> - try check' env defs with - | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err)) - let initial_env = Env.empty |> Env.add_prover prove diff --git a/src/type_check.mli b/src/type_check.mli index f1ce967e..af422025 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -70,17 +70,15 @@ val opt_no_lexp_bounds_check : bool ref (** {2 Type errors} *) type type_error = - | Err_no_casts of unit exp * type_error * type_error list + | Err_no_casts of unit exp * typ * typ * type_error * type_error list | Err_no_overloading of id * (id * type_error) list | Err_unresolved_quants of id * quant_item list - | Err_subtype of typ * typ * n_constraint list + | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t | Err_no_num_ident of id | Err_other of string exception Type_error of l * type_error;; -val string_of_type_error : type_error -> string - val typ_debug : string Lazy.t -> unit val typ_print : string Lazy.t -> unit @@ -129,7 +127,9 @@ module Env : sig val get_typ_vars : t -> base_kind_aux KBindings.t - val add_typ_var : kid -> base_kind_aux -> t -> t + val get_typ_var_locs : t -> Ast.l KBindings.t + + val add_typ_var : Ast.l -> kid -> base_kind_aux -> t -> t val is_record : id -> t -> bool @@ -191,7 +191,11 @@ end (** Push all the type variables and constraints from a typquant into an environment *) -val add_typquant : typquant -> Env.t -> Env.t +val add_typquant : Ast.l -> typquant -> Env.t -> Env.t + +val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option + +val add_existential : Ast.l -> kid list -> n_constraint -> Env.t -> Env.t (** When the typechecker creates new type variables it gives them fresh names of the form 'fvXXX#name, where XXX is a number (not @@ -366,12 +370,12 @@ Some invariants that will hold of a fully checked AST are: - Toplevel expressions such as typedefs and some subexpressions such as letbinds may have None as their tannots if it doesn't make sense - for them to have type annotations. *) -val check : Env.t -> 'a defs -> tannot defs * Env.t + for them to have type annotations. -(** Like check but throws type_errors rather than Sail generic errors - from Reporting_basic. *) -val check' : Env.t -> 'a defs -> tannot defs * Env.t + check throws type_errors rather than Sail generic errors from + Reporting_basic. For a function that uses generic errors, use + Type_error.check *) +val check : Env.t -> 'a defs -> tannot defs * Env.t (** The initial type checking environment *) val initial_env : Env.t diff --git a/src/type_error.ml b/src/type_error.ml new file mode 100644 index 00000000..78db65bc --- /dev/null +++ b/src/type_error.ml @@ -0,0 +1,141 @@ +(**************************************************************************) +(* 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 PPrint +open Util +open Ast +open Ast_util +open Type_check + +let bullet f xs = + group (separate_map hardline (fun x -> string "* " ^^ nest 2 (f x)) xs) + +let pp_nexp, pp_n_constraint = + let rec string_of_nexp = function + | Nexp_aux (nexp, _) -> string_of_nexp_aux nexp + and string_of_nexp_aux = function + | Nexp_id id -> string_of_id id + | Nexp_var kid -> string_of_kid kid + | Nexp_constant c -> Big_int.to_string c + | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")" + | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")" + | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")" + | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_nexp nexps ^ ")" + | Nexp_exp n -> "2 ^ " ^ string_of_nexp n + | Nexp_neg n -> "- " ^ string_of_nexp n + in + + let string_of_n_constraint = function + | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 + | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 + | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 + | NC_aux (NC_or (nc1, nc2), _) -> + "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")" + | NC_aux (NC_and (nc1, nc2), _) -> + "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" + | NC_aux (NC_set (kid, ns), _) -> + string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" + | NC_aux (NC_true, _) -> "true" + | NC_aux (NC_false, _) -> "false" + in + + let pp_nexp' nexp = + string (string_of_nexp nexp) + in + + let pp_n_constraint' nc = + string (string_of_n_constraint nc) + in + + pp_nexp', pp_n_constraint' + +let rec pp_type_error = function + | Err_no_casts (exp, typ_from, typ_to, trigger, _) -> + let coercion = + group (string "Tried performing type coercion from" ^/^ Pretty_print_sail.doc_typ typ_from + ^/^ string "to" ^/^ Pretty_print_sail.doc_typ typ_to + ^/^ string "on" ^/^ Pretty_print_sail.doc_exp exp) + in + coercion ^^ hardline ^^ (string "Failed because" ^/^ pp_type_error trigger) + + | Err_no_overloading (id, errs) -> + string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^ + group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^//^ pp_type_error err) errs) + + | Err_subtype (typ1, typ2, constrs, locs) -> + enclose (string (Util.termcode 1)) (string (Util.termcode 21)) + (separate space [ string (string_of_typ typ1); + string "is not a subtype of"; + string (string_of_typ typ2) ]) + ^/^ string "in context" + ^/^ bullet pp_n_constraint constrs + ^/^ string "where" + ^/^ bullet (fun (kid, l) -> string (string_of_kid kid ^ " bound at " ^ Reporting_basic.loc_to_string l ^ "\n")) (KBindings.bindings locs) + + | Err_no_num_ident id -> + string "No num identifier" ^^ space ^^ string (string_of_id id) + + | Err_unresolved_quants (id, quants) -> + string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id) + ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants) + + | Err_other str -> string str + +let rec string_of_type_error err = + let open PPrint in + let b = Buffer.create 20 in + ToBuffer.pretty 1. 400 b (pp_type_error err); + "\n" ^ Buffer.contents b + +let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = + fun env defs -> + try Type_check.check env defs with + | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err)) diff --git a/src/util.ml b/src/util.ml index 471b0c4c..b54c13d4 100644 --- a/src/util.ml +++ b/src/util.ml @@ -442,3 +442,6 @@ let warn str = if !opt_warnings then prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str) else () + +let log_line str line msg = + "\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg diff --git a/src/util.mli b/src/util.mli index 7a20a6dd..bb7aa70d 100644 --- a/src/util.mli +++ b/src/util.mli @@ -252,3 +252,5 @@ val warn : string -> unit val zencode_string : string -> string val zencode_upper_string : string -> string + +val log_line : string -> int -> string -> string diff --git a/src/value.ml b/src/value.ml index 858a17d9..8ee219b7 100644 --- a/src/value.ml +++ b/src/value.ml @@ -73,6 +73,7 @@ type value = | V_vector of value list | V_list of value list | V_int of Big_int.num + | V_real of Rational.t | V_bool of bool | V_bit of Sail_lib.bit | V_tuple of value list @@ -128,6 +129,10 @@ let coerce_int = function | V_int i -> i | _ -> assert false +let coerce_real = function + | V_real r -> r + | _ -> assert false + let coerce_cons = function | V_list (v :: vs) -> Some (v, vs) | V_list [] -> None @@ -277,6 +282,10 @@ let value_sub_int = function | [v1; v2] -> V_int (Sail_lib.sub_int (coerce_int v1, coerce_int v2)) | _ -> failwith "value sub" +let value_negate = function + | [v1] -> V_int (Sail_lib.negate (coerce_int v1)) + | _ -> failwith "value negate" + let value_mult = function | [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2)) | _ -> failwith "value mult" @@ -293,6 +302,10 @@ 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" +let value_sub_vec_int = function + | [v1; v2] -> mk_vector (Sail_lib.sub_vec_int (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value add_vec_int" + let value_add_vec = function | [v1; v2] -> mk_vector (Sail_lib.add_vec (coerce_bv v1, coerce_bv v2)) | _ -> failwith "value add_vec" @@ -343,6 +356,7 @@ let rec string_of_value = function | V_unit -> "()" | V_string str -> "\"" ^ str ^ "\"" | V_ref str -> "ref " ^ str + | V_real r -> "REAL" (* No Rational.to_string *) | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" | V_record record -> "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" @@ -396,6 +410,10 @@ let value_write_ram = function V_unit | _ -> failwith "value write_ram" +let value_load_raw = function + | [v1; v2] -> Sail_lib.load_raw (coerce_bv v1, coerce_string v2) ; V_unit + | _ -> failwith "value load_raw" + let value_putchar = function | [v] -> output_char !print_chan (char_of_int (Big_int.to_int (coerce_int v))); @@ -411,6 +429,62 @@ let value_print_int = function | [msg; n] -> output_endline (coerce_string msg ^ string_of_value n); V_unit | _ -> failwith "value print_int" +let value_print_string = function + | [msg; str] -> output_endline (coerce_string msg ^ coerce_string str); V_unit + | _ -> failwith "value print_string" + +let value_prerr_bits = function + | [msg; bits] -> prerr_endline (coerce_string msg ^ string_of_value bits); V_unit + | _ -> failwith "value prerr_bits" + +let value_prerr_int = function + | [msg; n] -> prerr_endline (coerce_string msg ^ string_of_value n); V_unit + | _ -> failwith "value prerr_int" + +let value_prerr_string = function + | [msg; str] -> output_endline (coerce_string msg ^ coerce_string str); V_unit + | _ -> failwith "value print_string" + +let value_concat_str = function + | [v1; v2] -> V_string (Sail_lib.concat_str (coerce_string v1, coerce_string v2)) + | _ -> failwith "value concat_str" + +let value_to_real = function + | [v] -> V_real (Sail_lib.to_real (coerce_int v)) + | _ -> failwith "value to_real" + +let value_quotient_real = function + | [v1; v2] -> V_real (Sail_lib.quotient_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value quotient_real" + +let value_round_up = function + | [v] -> V_int (Sail_lib.round_up (coerce_real v)) + | _ -> failwith "value round_up" + +let value_round_down = function + | [v] -> V_int (Sail_lib.round_down (coerce_real v)) + | _ -> failwith "value round_down" + +let value_eq_real = function + | [v1; v2] -> V_bool (Sail_lib.eq_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value eq_real" + +let value_lt_real = function + | [v1; v2] -> V_bool (Sail_lib.lt_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value lt_real" + +let value_gt_real = function + | [v1; v2] -> V_bool (Sail_lib.gt_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value gt_real" + +let value_lteq_real = function + | [v1; v2] -> V_bool (Sail_lib.lteq_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value lteq_real" + +let value_gteq_real = function + | [v1; v2] -> V_bool (Sail_lib.gteq_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value gteq_real" + let primops = List.fold_left (fun r (x, y) -> StringMap.add x y r) @@ -424,6 +498,11 @@ let primops = ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs))); ("print_bits", value_print_bits); ("print_int", value_print_int); + ("print_string", value_print_string); + ("prerr_bits", value_print_bits); + ("prerr_int", value_print_int); + ("prerr_string", value_prerr_string); + ("concat_str", value_concat_str); ("eq_int", value_eq_int); ("lteq", value_lteq); ("gteq", value_gteq); @@ -461,18 +540,34 @@ let primops = ("shiftl", value_shiftl); ("add_int", value_add_int); ("sub_int", value_sub_int); + ("div_int", value_quotient); + ("mult_int", value_mult); ("mult", value_mult); ("quotient", value_quotient); ("modulus", value_modulus); + ("negate", value_negate); ("shr_int", value_shr_int); ("shl_int", value_shl_int); ("max_int", value_max_int); ("min_int", value_min_int); ("add_vec_int", value_add_vec_int); + ("sub_vec_int", value_sub_vec_int); ("add_vec", value_add_vec); ("sub_vec", value_sub_vec); ("read_ram", value_read_ram); ("write_ram", value_write_ram); + ("trace_memory_read", fun _ -> V_unit); + ("trace_memory_write", fun _ -> V_unit); + ("load_raw", value_load_raw); + ("to_real", value_to_real); + ("eq_real", value_eq_real); + ("lt_real", value_lt_real); + ("gt_real", value_gt_real); + ("lteq_real", value_lt_real); + ("gteq_real", value_gt_real); + ("round_up", value_round_up); + ("round_down", value_round_down); + ("quotient_real", value_quotient_real); ("undefined_unit", fun _ -> V_unit); ("undefined_bit", fun _ -> V_bit Sail_lib.B0); ("undefined_int", fun _ -> V_int Big_int.zero); |