Skip to content

Commit

Permalink
Merge pull request #67 from AeneasVerif/protz_fix_inconsistency
Browse files Browse the repository at this point in the history 
Insert some assertions to catch undetected inconsistencies that my le…
  • Loading branch information
@msprotz
msprotz authored Aug 30, 2024
2 parents fa55cf2 + ba43f06 commit 7efec16
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 @@ -865,6 +865,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 @@ -1609,7 +1611,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 @@ -1642,110 +1644,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 @@ -1772,13 +1781,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 7efec16

Please sign in to comment.