Skip to content

Commit

Permalink
Add more definitions to the Lean library and add deboguing features
Browse files Browse the repository at this point in the history
  • Loading branch information
sonmarcho committed Dec 3, 2024
1 parent 8238eb8 commit 15b0735
Show file tree
Hide file tree
Showing 11 changed files with 325 additions and 17 deletions.
3 changes: 3 additions & 0 deletions backends/lean/Base/Primitives/ArraySlice.lean
Original file line number Diff line number Diff line change
Expand Up @@ -582,4 +582,7 @@ def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T)
if s.len = src.len then ok src
else fail panic

/- [core::array::TryFromSliceError] -/
def core.array.TryFromSliceError := ()

end Primitives
40 changes: 40 additions & 0 deletions backends/lean/Base/Primitives/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -111,3 +111,43 @@ def core.convert.IntoFrom {T : Type} {U : Type} (fromInst : core.convert.From U
def core.convert.FromSame (T : Type) : core.convert.From T T := {
from_ := fun x => ok (core.convert.FromSame.from_ x)
}

/- [core::result::Result] -/
inductive core.result.Result (T : Type) (E : Type) :=
| Ok : T → core.result.Result T E
| Err : E → core.result.Result T E

/- [core::fmt::Error] -/
@[reducible] def core.fmt.Error := Unit

structure core.convert.TryFrom (Self T : Type) where
Error : Type
try_from : T → Result (core.result.Result Self Error)

structure core.convert.TryInto (Self T : Type) where
Error : Type
try_into : Self → Result (core.result.Result T Error)

@[reducible, simp]
def core.convert.TryIntoFrom.try_into {T U : Type} (fromInst : core.convert.TryFrom U T)
(x : T) : Result (core.result.Result U fromInst.Error) :=
fromInst.try_from x

@[reducible]
def core.convert.TryIntoFrom {T U : Type} (fromInst : core.convert.TryFrom U T) :
core.convert.TryInto T U := {
Error := fromInst.Error
try_into := core.convert.TryIntoFrom.try_into fromInst
}

/- TODO: -/
axiom Formatter : Type

structure core.fmt.Debug (T : Type) where
fmt : T → Formatter → Result (Formatter × Formatter → Formatter)

def core.result.Result.unwrap {T E : Type}
(_ : core.fmt.Debug T) (e : core.result.Result T E) : Primitives.Result T :=
match e with
| .Ok x => ok x
| .Err _ => fail .panic
3 changes: 3 additions & 0 deletions src/Config.ml
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,9 @@ let if_backend (f : unit -> 'a) (default : 'a) : 'a =
| None -> default
| Some _ -> f ()

(** Print all the external definitions which are not listed in the builtin functions *)
let print_unknown_externals = ref false

(** {1 Interpreter} *)

(** Activate the sanity checks, and in particular the invariant checks
Expand Down
10 changes: 10 additions & 0 deletions src/Errors.ml
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,16 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option)
let craise (file : string) (line : int) (span : Meta.span) (msg : string) =
craise_opt_span file line (Some span) msg

(** Lazy assert *)
let classert_opt_span (file : string) (line : int) (b : bool)
(span : Meta.span option) (msg : string Lazy.t) =
if not b then craise_opt_span file line span (Lazy.force msg)

(** Lazy assert *)
let classert (file : string) (line : int) (b : bool) (span : Meta.span)
(msg : string Lazy.t) =
classert_opt_span file line b (Some span) msg

let cassert_opt_span (file : string) (line : int) (b : bool)
(span : Meta.span option) (msg : string) =
if not b then craise_opt_span file line span msg
Expand Down
179 changes: 176 additions & 3 deletions src/Main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,37 @@ Usage: %s [OPTIONS] FILE
|}
Sys.argv.(0)

let matches_name (c : crate) (name : Types.name)
(m : 'a ExtractName.NameMatcherMap.t) : bool =
let open Charon.NameMatcher in
let open ExtractBuiltin in
let mctx : ctx =
{
type_decls = c.type_decls;
global_decls = c.global_decls;
fun_decls = c.fun_decls;
trait_decls = c.trait_decls;
trait_impls = c.trait_impls;
}
in
NameMatcherMap.mem mctx name m

let matches_name_with_generics (c : crate) (name : Types.name)
(generics : Types.generic_args) (m : 'a ExtractName.NameMatcherMap.t) : bool
=
let open Charon.NameMatcher in
let open ExtractBuiltin in
let mctx : ctx =
{
type_decls = c.type_decls;
global_decls = c.global_decls;
fun_decls = c.fun_decls;
trait_decls = c.trait_decls;
trait_impls = c.trait_impls;
}
in
Option.is_some (NameMatcherMap.find_with_generics_opt mctx name generics m)

let () =
(* Measure start time *)
let start_time = Unix.gettimeofday () in
Expand Down Expand Up @@ -129,6 +160,10 @@ let () =
Arg.Set use_nested_tuple_projectors,
" Use nested projectors for tuples (e.g., (0, 1, 2).snd.fst instead of \
(0, 1, 2).1)." );
( "-print-unknown-externals",
Arg.Set print_unknown_externals,
" Print all the external definitions which are not listed in the \
builtin functions" );
]
in

Expand Down Expand Up @@ -190,8 +225,6 @@ let () =
if cond then fail_with_error msg
in

if !print_llbc then main_log#set_level EL.Debug;

(* Sanity check (now that the arguments are parsed!) *)
check_arg_implies
(not !extract_template_decreases_clauses)
Expand Down Expand Up @@ -300,7 +333,9 @@ let () =
| Ok m ->
(* Logging *)
log#linfo (lazy ("Imported: " ^ filename));
log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
if !print_llbc then
log#linfo (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"))
else log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));

(* Check the Charon CLI options *)
check_no_doc m.options.hide_marker_traits
Expand All @@ -323,6 +358,144 @@ let () =
definitions";
fail true);

(* Print the external definitions which are not listed in the builtin functions *)
if !print_unknown_externals then (
let open TranslateCore in
let { type_decls; fun_decls; global_decls; trait_decls; trait_impls; _ }
=
m
in
(* Filter the definitions *)
let type_decls =
Types.TypeDeclId.Map.filter
(fun _ (d : Types.type_decl) ->
let names_map = ExtractBuiltin.builtin_types_map () in
(not d.item_meta.is_local)
&& not (matches_name m d.item_meta.name names_map))
type_decls
in
let fun_decls =
LlbcAst.FunDeclId.Map.filter
(fun _ (d : LlbcAst.fun_decl) ->
let names_map = ExtractBuiltin.builtin_funs_map () in
(not d.item_meta.is_local)
&& (not (matches_name m d.item_meta.name names_map))
(* We also ignore the trait method declarations *)
&&
match d.kind with
| TraitDeclItem _ -> false
| _ -> true)
fun_decls
in
let global_decls =
LlbcAst.GlobalDeclId.Map.filter
(fun _ (d : LlbcAst.global_decl) ->
let funs_map = ExtractBuiltin.builtin_globals_map in
(not d.item_meta.is_local)
&& not (matches_name m d.item_meta.name funs_map))
global_decls
in
let trait_decls =
LlbcAst.TraitDeclId.Map.filter
(fun _ (d : LlbcAst.trait_decl) ->
let names_map = ExtractBuiltin.builtin_trait_decls_map () in
(not d.item_meta.is_local)
&& not (matches_name m d.item_meta.name names_map))
trait_decls
in
let trait_impls =
List.filter_map
(fun (d : LlbcAst.trait_impl) ->
let names_map = ExtractBuiltin.builtin_trait_impls_map () in
match
LlbcAst.TraitDeclId.Map.find_opt d.impl_trait.trait_decl_id
m.trait_decls
with
| None -> None (* Just ignore it *)
| Some trait_decl ->
if
(not d.item_meta.is_local)
&& not
(matches_name_with_generics m trait_decl.item_meta.name
d.impl_trait.decl_generics names_map)
then Some (d, trait_decl)
else None)
(LlbcAst.TraitImplId.Map.values trait_impls)
in
(* Print *)
let fmt_env = Print.Crate.crate_to_fmt_env m in
let type_decls =
List.map
(fun (d : Types.type_decl) ->
let pattern =
TranslateCore.name_with_crate_to_pattern_string m
d.item_meta.name
in
"Type decl (pattern: [" ^ pattern ^ "]]):\n"
^ Print.type_decl_to_string fmt_env d)
(Types.TypeDeclId.Map.values type_decls)
in
let fun_decls =
List.map
(fun (d : LlbcAst.fun_decl) ->
let pattern =
TranslateCore.name_with_crate_to_pattern_string m
d.item_meta.name
in
let d =
(* FIXME: there is a bug in the formatter when splitting the predicates
and trait clauses between the inherited ones and the others (the
index is sometimes out of bounds).
See: https://github.com/AeneasVerif/charon/issues/482
*)
try Print.Ast.fun_decl_to_string fmt_env "" " " d
with _ -> "UNKNOWN"
in
"Fun decl (pattern: [" ^ pattern ^ "]]):\n" ^ d)
(LlbcAst.FunDeclId.Map.values fun_decls)
in
let global_decls =
List.map
(fun (d : LlbcAst.global_decl) ->
let pattern =
TranslateCore.name_with_crate_to_pattern_string m
d.item_meta.name
in
"Global decl (pattern: [" ^ pattern ^ "]]):\n"
^ Print.Ast.global_decl_to_string fmt_env "" " " d)
(LlbcAst.GlobalDeclId.Map.values global_decls)
in
let trait_decls =
List.map
(fun (d : LlbcAst.trait_decl) ->
let pattern =
TranslateCore.name_with_crate_to_pattern_string m
d.item_meta.name
in
"Trait decl (pattern: [" ^ pattern ^ "]]):\n"
^ Print.Ast.trait_decl_to_string fmt_env "" " " d)
(LlbcAst.TraitDeclId.Map.values trait_decls)
in
let trait_impls =
List.map
(fun ((d, trait_decl) : LlbcAst.trait_impl * LlbcAst.trait_decl) ->
let pattern =
TranslateCore.name_with_generics_crate_to_pattern_string m
trait_decl.item_meta.name trait_decl.generics
d.impl_trait.decl_generics
in
"Trait impl (pattern: [" ^ pattern ^ "]]):\n"
^ Print.Ast.trait_impl_to_string fmt_env "" " " d)
trait_impls
in

log#linfo
(lazy
(String.concat "\n\n"
(type_decls @ fun_decls @ global_decls @ trait_decls
@ trait_impls)));
());

(* There may be exceptions to catch *)
(try
(* Apply the pre-passes *)
Expand Down
37 changes: 37 additions & 0 deletions src/TranslateCore.ml
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,43 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
in
name_with_generics_to_simple_name mctx ~prefix n p g

let name_with_crate_to_pattern_string (ctx : LlbcAst.crate) (n : Types.name) :
string =
let mctx : Charon.NameMatcher.ctx =
{
type_decls = ctx.type_decls;
global_decls = ctx.global_decls;
fun_decls = ctx.fun_decls;
trait_decls = ctx.trait_decls;
trait_impls = ctx.trait_impls;
}
in
let c : Charon.NameMatcher.to_pat_config =
{ tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
in
let pat = Charon.NameMatcher.name_to_pattern mctx c n in
Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat

let name_with_generics_crate_to_pattern_string (ctx : LlbcAst.crate)
(n : Types.name) (params : Types.generic_params) (args : Types.generic_args)
: string =
let mctx : Charon.NameMatcher.ctx =
{
type_decls = ctx.type_decls;
global_decls = ctx.global_decls;
fun_decls = ctx.fun_decls;
trait_decls = ctx.trait_decls;
trait_impls = ctx.trait_impls;
}
in
let c : Charon.NameMatcher.to_pat_config =
{ tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
in
let pat =
Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args
in
Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat

let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string =
let mctx : Charon.NameMatcher.ctx =
{
Expand Down
11 changes: 7 additions & 4 deletions src/extract/ExtractBase.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1680,10 +1680,13 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx)
let clause_trait = clause.trait.binder_value in
(* *)
let trait_id = clause_trait.trait_decl_id in
let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
let args = clause_trait.decl_generics in
trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
impl_trait_decl.item_meta.name params args
(* The declaration may be missing because of an error *)
match TraitDeclId.Map.find_opt trait_id ctx.crate.trait_decls with
| None -> [ "clause" ]
| Some impl_trait_decl ->
let args = clause_trait.decl_generics in
trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
impl_trait_decl.item_meta.name params args
in
String.concat "" clause

Expand Down
Loading

0 comments on commit 15b0735

Please sign in to comment.