summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml3
-rw-r--r--compiler/InterpreterBorrows.ml26
-rw-r--r--compiler/InterpreterBorrowsCore.ml4
-rw-r--r--compiler/InterpreterPaths.ml21
-rw-r--r--compiler/InterpreterProjectors.ml4
-rw-r--r--compiler/Invariants.ml5
-rw-r--r--compiler/Main.ml4
-rw-r--r--compiler/PrePasses.ml19
-rw-r--r--compiler/Print.ml1
-rw-r--r--compiler/PureTypeCheck.ml9
-rw-r--r--compiler/SymbolicToPure.ml8
-rw-r--r--compiler/Translate.ml69
12 files changed, 91 insertions, 82 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index f7d08fdb..985fb470 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
^ string_of_int (List.length types)
^ " type arguments"
in
- log#serror err;
+ save_error __FILE__ __LINE__ None err;
Result.Error (types, err))
else
let types = List.combine filter types in
@@ -1884,6 +1884,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
let meta = body.meta in
sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
+
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
let name =
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e593ae75..a158ed9a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -303,13 +303,11 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
if bid' = bid then (
(* Sanity check *)
let expected_ty = ty in
- if nv.ty <> expected_ty then (
- log#serror
- ("give_back_value: improper type:\n- expected: "
- ^ ty_to_string ctx ty ^ "\n- received: "
- ^ ty_to_string ctx nv.ty);
+ if nv.ty <> expected_ty then
craise __FILE__ __LINE__ meta
- "Value given back doesn't have the proper type");
+ ("Value given back doesn't have the proper type:\n\
+ - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
+ ^ ty_to_string ctx nv.ty);
(* Replace *)
set_replaced ();
nv.value)
@@ -540,13 +538,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
* see the comment at the level of the definition of
* {!typed_avalue} *)
let _, expected_ty, _ = ty_get_ref ty in
- if nv.ty <> expected_ty then (
- log#serror
- ("give_back_avalue_to_same_abstraction: improper type:\n\
+ if nv.ty <> expected_ty then
+ craise __FILE__ __LINE__ meta
+ ("Value given back doesn't have the proper type:\n\
- expected: " ^ ty_to_string ctx ty ^ "\n- received: "
^ ty_to_string ctx nv.ty);
- craise __FILE__ __LINE__ meta
- "Value given back doesn't have the proper type");
(* This is the loan we are looking for: apply the projection to
* the value we give back and replaced this mutable loan with
* an ended loan *)
@@ -836,26 +832,26 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
match lookup_borrow_opt ek_all l ctx with
| None -> () (* Ok *)
| Some _ ->
- log#lerror
+ log#ltrace
(lazy
(fun_name ^ ": " ^ BorrowId.to_string l
^ ": borrow didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx0
^ "\n\n- new context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx));
- craise __FILE__ __LINE__ meta "Borrow not eliminated"
+ internal_error __FILE__ __LINE__ meta
in
match lookup_loan_opt meta ek_all l ctx with
| None -> () (* Ok *)
| Some _ ->
- log#lerror
+ log#ltrace
(lazy
(fun_name ^ ": " ^ BorrowId.to_string l
^ ": loan didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx0
^ "\n\n- new context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx));
- craise __FILE__ __LINE__ meta "Loan not eliminated"
+ internal_error __FILE__ __LINE__ meta
in
unit_to_cm_fun check_disappeared
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 6e65b11d..a01be046 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -162,11 +162,11 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
default
| _ ->
- log#lerror
+ log#ltrace
(lazy
("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1
^ "\n- ty2: " ^ show_ty ty2));
- craise __FILE__ __LINE__ meta "Unreachable"
+ internal_error __FILE__ __LINE__ meta
(** Check if two different projections intersect. This is necessary when
giving a symbolic value to an abstraction: we need to check that
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index f2c0bcb1..ab3daa72 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -83,7 +83,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
let nv = update v in
(* Type checking *)
if nv.ty <> v.ty then (
- log#lerror
+ log#ltrace
(lazy
("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
^ show_ety v.ty));
@@ -252,8 +252,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
let pe = "- pe: " ^ show_projection_elem pe in
let v = "- v:\n" ^ show_value v in
let ty = "- ty:\n" ^ show_ety ty in
- log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
- craise __FILE__ __LINE__ meta "Inconsistent projection")
+ craise __FILE__ __LINE__ meta
+ ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
(** Generic function to access (read/write) the value at a given place.
@@ -319,14 +319,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
(* Note that we ignore the new environment: it should be the same as the
original one.
*)
- if !Config.sanity_checks then
- if ctx1 <> ctx then (
- let msg =
- "Unexpected environment update:\nNew environment:\n"
- ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
- in
- log#serror msg;
- craise __FILE__ __LINE__ meta "Unexpected environment update");
+ (if !Config.sanity_checks then
+ if ctx1 <> ctx then
+ let msg =
+ "Unexpected environment update:\nNew environment:\n"
+ ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
+ in
+ craise __FILE__ __LINE__ meta msg);
Ok read_value
let read_place (meta : Meta.meta) (access : access_kind) (p : place)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 6e86e6a4..3993d845 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -217,12 +217,12 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
meta);
ASymbolic (AProjBorrows (s, ty))
| _ ->
- log#lerror
+ log#ltrace
(lazy
("apply_proj_borrows: unexpected inputs:\n- input value: "
^ typed_value_to_string ~meta:(Some meta) ctx v
^ "\n- proj rty: " ^ ty_to_string ctx ty));
- craise __FILE__ __LINE__ meta "Unreachable"
+ internal_error __FILE__ __LINE__ meta
in
{ value; ty }
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 642d7a37..2ccf3ad4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
"find_info: could not find the representant of borrow "
^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
in
- log#serror err;
craise __FILE__ __LINE__ meta err
in
@@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
| AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
| AIgnored, _ -> ()
| _ ->
- log#lerror
+ log#ltrace
(lazy
("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
^ "\n- value: "
^ typed_avalue_to_string ~meta:(Some meta) ctx atv
^ "\n- type: " ^ ty_to_string ctx atv.ty));
- craise __FILE__ __LINE__ meta "Erroneous typing");
+ internal_error __FILE__ __LINE__ meta);
(* Continue exploring to inspect the subterms *)
super#visit_typed_avalue info atv
end
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 416f3a07..6161f2f2 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -283,7 +283,9 @@ let () =
if !Errors.error_list <> [] then (
List.iter
(fun (meta, msg) -> log#serror (Errors.format_error_message meta msg))
- !Errors.error_list;
+ (* Reverse the list of error messages so that we print them from the
+ earliest to the latest. *)
+ (List.rev !Errors.error_list);
exit 1);
(* Print total elapsed time *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 0b39f64a..a46ef79c 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -238,9 +238,9 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
method! visit_Sequence env st1 st2 =
match st1.content with
| Loop _ ->
- sanity_check __FILE__ __LINE__
+ cassert __FILE__ __LINE__
(statement_has_no_loop_break_continue st2)
- st2.meta;
+ st2.meta "Sequences of loops are not supported yet";
(replace_breaks_with st1 st2).content
| _ -> super#visit_Sequence env st1 st2
end
@@ -437,9 +437,22 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
let apply_passes (crate : crate) : crate =
let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
+ (* Attempt to apply a pass: if it fails we replace the body by [None] *)
+ let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
+ try pass f
+ with CFailure (_, _) ->
+ (* The error was already registered, we don't need to register it twice.
+ However, we replace the body of the function, and save an error to
+ report to the user the fact that we will ignore the function body *)
+ let fmt = Print.Crate.crate_to_fmt_env crate in
+ let name = Print.name_to_string fmt f.name in
+ save_error __FILE__ __LINE__ (Some f.meta)
+ ("Ignoring the body of '" ^ name ^ "' because of previous error");
+ { f with body = None }
+ in
let fun_decls =
List.fold_left
- (fun fl pass -> FunDeclId.Map.map pass fl)
+ (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl)
crate.fun_decls passes
in
let crate = { crate with fun_decls } in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dad1aea3..51286553 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,4 +1,5 @@
include Charon.PrintUtils
+include Charon.PrintTypes
include Charon.PrintLlbcAst
open Charon.PrintTypes
open Charon.PrintExpressions
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 098e2564..27044c27 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -93,12 +93,11 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx)
get_adt_field_types meta ctx.type_decls type_id av.variant_id generics
in
let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
- if ty <> v.ty then (
+ if ty <> v.ty then
(* TODO: we need to normalize the types *)
- log#serror
- ("check_typed_pattern: not the same types:" ^ "\n- ty: "
- ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
- craise __FILE__ __LINE__ meta "Inconsistent types");
+ craise __FILE__ __LINE__ meta
+ ("Inconsistent types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: "
+ ^ show_ty v.ty);
check_typed_pattern meta ctx v
in
(* Check the field types: check that the field patterns have the expected
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 607da445..93f9ef75 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3867,11 +3867,9 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
with CFailure (meta, _) ->
let env = PrintPure.decls_ctx_to_fmt_env ctx in
let name = PrintPure.name_to_string env a.name in
- let () =
- save_error __FILE__ __LINE__ meta
- ("Could not translate type decl '" ^ name
- ^ "' because of previous error")
- in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate type decl '" ^ name
+ ^ "' because of previous error");
None)
(TypeDeclId.Map.values ctx.type_ctx.type_decls)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2fcf5b43..870f8a22 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -204,10 +204,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
(translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
with CFailure (meta, _) ->
let name = name_to_string trans_ctx fdef.name in
- let () =
- save_error __FILE__ __LINE__ meta
- ("Could not translate function '" ^ name ^ "' because of previous error")
- in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the function '" ^ name
+ ^ "' because of previous error");
None
(* TODO: factor out the return type *)
@@ -231,6 +230,7 @@ let translate_crate_to_pure (crate : crate) :
Pure.TypeDeclId.Map.of_list
(List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
in
+
(* Compute the decomposed fun sigs for the whole crate *)
let fun_dsigs =
FunDeclId.Map.of_list
@@ -243,11 +243,9 @@ let translate_crate_to_pure (crate : crate) :
trans_ctx fdef )
with CFailure (meta, _) ->
let name = name_to_string trans_ctx fdef.name in
- let () =
- save_error __FILE__ __LINE__ meta
- ("Could not translate function signature '" ^ name
- ^ "' because of previous error")
- in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the function signature of '" ^ name
+ ^ "' because of previous error");
None)
(FunDeclId.Map.values crate.fun_decls))
in
@@ -266,11 +264,9 @@ let translate_crate_to_pure (crate : crate) :
try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
with CFailure (meta, _) ->
let name = name_to_string trans_ctx a.name in
- let () =
- save_error __FILE__ __LINE__ meta
- ("Could not translate trait decl '" ^ name
- ^ "' because of previous error")
- in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the trait declaration '" ^ name
+ ^ "' because of previous error");
None)
(TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
in
@@ -282,11 +278,9 @@ let translate_crate_to_pure (crate : crate) :
try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
with CFailure (meta, _) ->
let name = name_to_string trans_ctx a.name in
- let () =
- save_error __FILE__ __LINE__ meta
- ("Could not translate trait impl '" ^ name
- ^ "' because of previous error")
- in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the trait instance '" ^ name
+ ^ "' because of previous error");
None)
(TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
in
@@ -516,12 +510,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
let global =
try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
with CFailure (meta, _) ->
- let () =
- let name = name_to_string ctx.trans_ctx global.name in
- save_error __FILE__ __LINE__ meta
- ("Could not translate global '" ^ name
- ^ "' because of previous error")
- in
+ let name = name_to_string ctx.trans_ctx global.name in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the global declaration '" ^ name
+ ^ "' because of previous error");
None
in
Extract.extract_global_decl ctx fmt global body config.interface
@@ -778,22 +770,28 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
| TypeGroup (RecGroup ids) ->
if config.extract_types then export_types_group true ids
| FunGroup (NonRecGroup id) -> (
- (* Lookup *)
- let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+ (* Lookup - the translated function may not be in the map if we had
+ to ignore it because of errors *)
+ let pure_fun = FunDeclId.Map.find_opt id ctx.trans_funs in
(* Special case: we skip trait method *declarations* (we will
extract their type directly in the records we generate for
the trait declarations themselves, there is no point in having
separate type definitions) *)
- match pure_fun.f.Pure.kind with
- | TraitItemDecl _ -> ()
- | _ ->
- (* Translate *)
- export_functions_group [ pure_fun ])
+ match pure_fun with
+ | Some pure_fun -> (
+ match pure_fun.f.Pure.kind with
+ | TraitItemDecl _ -> ()
+ | _ ->
+ (* Translate *)
+ export_functions_group [ pure_fun ])
+ | None -> ())
| FunGroup (RecGroup ids) ->
(* General case of mutually recursive functions *)
(* Lookup *)
let pure_funs =
- List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
+ List.filter_map
+ (fun id -> FunDeclId.Map.find_opt id ctx.trans_funs)
+ ids
in
(* Translate *)
export_functions_group pure_funs
@@ -951,7 +949,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
| Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
(* Some logging *)
- log#linfo (lazy ("Generated: " ^ fi.filename));
+ if !Errors.error_list <> [] then
+ log#linfo
+ (lazy ("Generated the partial file (because of errors): " ^ fi.filename))
+ else log#linfo (lazy ("Generated: " ^ fi.filename));
(* Flush and close the file *)
close_out out