Skip to content

Commit

Permalink
Insert some assertions to catch undetected inconsistencies that my le…
Browse files Browse the repository at this point in the history 
…ad to an infinite loop
  • Loading branch information
@msprotz
msprotz committed Aug 29, 2024
1 parent cd5c9e5 commit 4acfceb
Showing 1 changed file with 115 additions and 105 deletions.
220 changes: 115 additions & 105 deletions lib/AstOfLlbc.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -864,6 +864,8 @@ and mk_clause_binders_and_args env clause_mapping : clause_binder list =
K.n_cgs = List.length signature.generics.const_generics - trait_ts.n_cgs;
}
in
(* TODO: figure out why this fails for e.g. Iterator.rev *)
assert (ts.n_cgs > 0 && ts.n > 0);
{ pretty_name; t; clause_id; item_name; ts })
clause_mapping

Expand Down Expand Up @@ -1603,7 +1605,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
let decl = try Some (env.get_nth_function id) with Not_found -> None in
match decl with
| None -> None
| Some decl -> (
| Some decl ->
let { C.def_id; signature; body; is_global_decl_body; item_meta; kind; _ } = decl in
let env = { env with generic_params = signature.generics } in
L.log "AstOfLlbc" "Visiting %sfunction: %s\n%s"
Expand Down Expand Up @@ -1636,110 +1638,117 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
if is_global_decl_body then
None
else
let env = push_cg_binders env signature.C.generics.const_generics in
let env = push_type_binders env signature.C.generics.types in

L.log "AstOfLlbc" "ty of locals: %s"
(String.concat " ++ "
(List.map
(fun (local : C.var) ->
Charon.PrintTypes.ty_to_string env.format_env local.var_ty)
locals));
L.log "AstOfLlbc" "ty of inputs: %s"
(String.concat " ++ "
(List.map
(fun t -> Charon.PrintTypes.ty_to_string env.format_env t)
signature.C.inputs));

let clause_mapping =
build_trait_clause_mapping env signature.C.generics.trait_clauses
in
debug_trait_clause_mapping env clause_mapping;

(* `locals` contains, in order: special return variable; function arguments;
local variables *)
let args, locals = Krml.KList.split (arg_count + 1) locals in
let return_var = List.hd args in
let args = List.tl args in

let return_type = typ_of_ty env return_var.var_ty in

(* Note: Rust allows zero-argument functions but the krml internal
representation wants a unit there. This is aligned with typ_of_signature. *)
let t_unit =
C.(
TAdt (TTuple, { types = []; const_generics = []; regions = []; trait_refs = [] }))
in
let v_unit =
{
C.index = Charon.Expressions.VarId.of_int max_int;
name = None;
var_ty = t_unit;
}
in
let args =
if args = [] then
[ v_unit ]
else
args
in

(* At this stage, env has:
cg_binders = <<all cg binders>>
type_binders = <<all type binders>>
binders = <<all cg binders>>
*)
let clause_binders = mk_clause_binders_and_args env clause_mapping in
(* Now we turn it into:
binders = <<all cg binders>> ++ <<all clause binders>> ++ <<regular function args>>
*)
let env = push_clause_binders env clause_binders in
let env = push_binders env args in

let arg_binders =
List.map
(fun (arg : C.const_generic_var) ->
Krml.Helpers.fresh_binder ~mut:true arg.name (typ_of_literal_ty env arg.ty))
signature.C.generics.const_generics
@ List.map
(fun { pretty_name; t; _ } -> Krml.Helpers.fresh_binder pretty_name t)
clause_binders
@ List.map
(fun (arg : C.var) ->
let name = Option.value ~default:"_" arg.name in
Krml.Helpers.fresh_binder ~mut:true name (typ_of_ty env arg.var_ty))
try
let env = push_cg_binders env signature.C.generics.const_generics in
let env = push_type_binders env signature.C.generics.types in

L.log "AstOfLlbc" "ty of locals: %s"
(String.concat " ++ "
(List.map
(fun (local : C.var) ->
Charon.PrintTypes.ty_to_string env.format_env local.var_ty)
locals));
L.log "AstOfLlbc" "ty of inputs: %s"
(String.concat " ++ "
(List.map
(fun t -> Charon.PrintTypes.ty_to_string env.format_env t)
signature.C.inputs));

let clause_mapping =
build_trait_clause_mapping env signature.C.generics.trait_clauses
in
debug_trait_clause_mapping env clause_mapping;

(* `locals` contains, in order: special return variable; function arguments;
local variables *)
let args, locals = Krml.KList.split (arg_count + 1) locals in
let return_var = List.hd args in
let args = List.tl args in

let return_type = typ_of_ty env return_var.var_ty in

(* Note: Rust allows zero-argument functions but the krml internal
representation wants a unit there. This is aligned with typ_of_signature. *)
let t_unit =
C.(
TAdt (TTuple, { types = []; const_generics = []; regions = []; trait_refs = [] }))
in
let v_unit =
{
C.index = Charon.Expressions.VarId.of_int max_int;
name = None;
var_ty = t_unit;
}
in
let args =
if args = [] then
[ v_unit ]
else
args
in
L.log "AstOfLlbc" "type of binders: %a" ptyps
(List.map (fun o -> o.K.typ) arg_binders);
let body =
with_locals env return_type (return_var :: locals) (fun env ->
expression_of_raw_statement env return_var.index body.content)
in
let flags =
match item_meta.attr_info.inline with
| Some Hint -> [ Krml.Common.Inline ]
| Some Always -> [ Krml.Common.MustInline ]
| Some Never -> [ Krml.Common.NoInline ]
| _ -> []
in
(* This is kind of a hack here: we indicate that this function is intended to be
specialized, at monomorphization-time (which happens quite early on), on the cg
binders but also on the clause binders... This is ok because even though the
clause binders are not in env.cg_binders, well, types don't refer to clause
binders, so we won't have translation errors. *)
let n_cg = List.length signature.C.generics.const_generics in
let n = List.length signature.C.generics.types in
Some
(K.DFunction
( None,
flags @ flags_of_meta item_meta,
n_cg,
n,
return_type,
name,
arg_binders,
body ))))
in

(* At this stage, env has:
cg_binders = <<all cg binders>>
type_binders = <<all type binders>>
binders = <<all cg binders>>
*)
let clause_binders = mk_clause_binders_and_args env clause_mapping in
(* Now we turn it into:
binders = <<all cg binders>> ++ <<all clause binders>> ++ <<regular function args>>
*)
let env = push_clause_binders env clause_binders in
let env = push_binders env args in

let arg_binders =
List.map
(fun (arg : C.const_generic_var) ->
Krml.Helpers.fresh_binder ~mut:true arg.name (typ_of_literal_ty env arg.ty))
signature.C.generics.const_generics
@ List.map
(fun { pretty_name; t; _ } -> Krml.Helpers.fresh_binder pretty_name t)
clause_binders
@ List.map
(fun (arg : C.var) ->
let name = Option.value ~default:"_" arg.name in
Krml.Helpers.fresh_binder ~mut:true name (typ_of_ty env arg.var_ty))
args
in
L.log "AstOfLlbc" "type of binders: %a" ptyps
(List.map (fun o -> o.K.typ) arg_binders);
let body =
with_locals env return_type (return_var :: locals) (fun env ->
expression_of_raw_statement env return_var.index body.content)
in
let flags =
match item_meta.attr_info.inline with
| Some Hint -> [ Krml.Common.Inline ]
| Some Always -> [ Krml.Common.MustInline ]
| Some Never -> [ Krml.Common.NoInline ]
| _ -> []
in
(* This is kind of a hack here: we indicate that this function is intended to be
specialized, at monomorphization-time (which happens quite early on), on the cg
binders but also on the clause binders... This is ok because even though the
clause binders are not in env.cg_binders, well, types don't refer to clause
binders, so we won't have translation errors. *)
let n_cg = List.length signature.C.generics.const_generics in
let n = List.length signature.C.generics.types in
Some
(K.DFunction
( None,
flags @ flags_of_meta item_meta,
n_cg,
n,
return_type,
name,
arg_binders,
body ))
with e ->
L.log "AstOfLlbc" "ERROR translating %s: %s\n%s"
(string_of_name env decl.item_meta.name)
(Printexc.to_string e) (Printexc.get_backtrace ());
None
)
| IdGlobal id ->
let global = env.get_nth_global id in
let { C.item_meta; ty; def_id; _ } = global in
Expand All @@ -1766,13 +1775,14 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =

let decls_of_declarations (env : env) (d : C.declaration_group) : K.decl list =
incr seen;
L.log "Progress" "%d/%d" !seen !total;
L.log "Progress" "%s: %d/%d" env.crate_name !seen !total;
Krml.KList.filter_some @@ List.map (decl_of_id env) @@ declaration_group_to_list d

let file_of_crate (crate : Charon.LlbcAst.crate) : Krml.Ast.file =
let { C.name; declarations; type_decls; fun_decls; global_decls; trait_decls; trait_impls } =
crate
in
seen := 0;
total := List.length declarations;
let get_nth_function id = C.FunDeclId.Map.find id fun_decls in
let get_nth_type id = C.TypeDeclId.Map.find id type_decls in
Expand Down

0 comments on commit 4acfceb

Please sign in to comment.