Skip to content

Commit

Permalink
Simplified analysis, swapped from cid to strings
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Nov 21, 2023
1 parent 6709eae commit e1f71bd
Show file tree
Hide file tree
Showing 3 changed files with 37 additions and 66 deletions.
9 changes: 1 addition & 8 deletions engine/bin/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,7 @@
(name lib)
(modules lib)
(wrapped false)
(libraries
hax_engine
fstar_backend
coq_backend
easycrypt_backend
proverif_backend
logs
core)
(libraries hax_engine fstar_backend coq_backend easycrypt_backend proverif_backend logs core)
(preprocess
(pps
ppx_yojson_conv
Expand Down
34 changes: 10 additions & 24 deletions engine/lib/analyses/function_dependency.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,35 +6,21 @@ module%inlined_contents Make (F : Features.T) = struct
module U = Ast_utils.Make (F)
open Ast

type analysis_data = concrete_ident list Map.M(Concrete_ident).t
type analysis_data = concrete_ident list Map.M(String).t (* Concrete_ident *)
type id_order = int

let analyse_function_body (x : A.expr) : concrete_ident list =
Set.to_list (U.Reducers.collect_concrete_idents#visit_expr () x)
(* List.filter_map *)
(* ~f:(function *)
(* | `Projector (`Concrete cid) | `Concrete cid -> *)
(* Some (Uprint.Concrete_ident_view.to_definition_name cid) *)
(* | _ -> None) *)
(* (Set.to_list collect_global_idents) *)

let functions_of_item (x : A.item) : (concrete_ident * A.expr) list =
match x.v with
| Fn { name; generics = _; body; params = _ } -> [ (name, body) ]
| Impl { items; _ } ->
List.filter_map
~f:(fun w ->
match w.ii_v with
| IIFn { body; params = _ } -> Some (w.ii_ident, body)
| _ -> None)
items
| _ -> []
module Uprint =
Ast_utils.MakeWithNamePolicy (F) (Concrete_ident.DefaultNamePolicy)

let analyse (items : A.item list) : analysis_data =
let temp_list = List.concat_map ~f:functions_of_item items in
let temp_list = List.concat_map ~f:U.functions_of_item items in
List.fold_left
~init:(Map.empty (module Concrete_ident))
~init:(Map.empty (module String (* Concrete_ident *)))
~f:(fun y (name, body) ->
Map.set y ~key:name ~data:(analyse_function_body body))
Map.set y
~key:(Uprint.Concrete_ident_view.to_definition_name name)
~data:
(Set.to_list
(U.Reducers.collect_concrete_idents#visit_expr () body)))
temp_list
end
60 changes: 26 additions & 34 deletions engine/lib/analyses/mutable_variables.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,15 @@ module%inlined_contents Make (F : Features.T) = struct
open Ast

type id_order = int
type pre_data = concrete_ident list Map.M(Concrete_ident).t
type pre_data = concrete_ident list Map.M(String).t (* Concrete_ident *)

type analysis_data =
(Local_ident.t list * (U.TypedLocalIdent.t * id_order) list)
(* external mut_vars vs new variables (e.g. needs def / local) *)
Map.M(Concrete_ident).t
Map.M(String).t

module Uprint =
Ast_utils.MakeWithNamePolicy (F) (Concrete_ident.DefaultNamePolicy)

module LocalIdentOrData (Ty : sig
type ty [@@deriving compare, sexp]
Expand Down Expand Up @@ -130,7 +133,8 @@ module%inlined_contents Make (F : Features.T) = struct
(module W)
(List.map ~f:(fun x -> W.Identifier x) x),
m#snd#zero ))
(Map.find data cid)
(Map.find data
(Uprint.Concrete_ident_view.to_definition_name cid))
| _ -> super#visit_global_ident env x

method! visit_concrete_ident (_env : W.t list Map.M(Local_ident).t)
Expand All @@ -141,7 +145,8 @@ module%inlined_contents Make (F : Features.T) = struct
(module W)
(List.map ~f:(fun x -> W.Identifier x) x),
m#snd#zero ))
(Map.find data cid)
(Map.find data
(Uprint.Concrete_ident_view.to_definition_name cid))
end)
#visit_expr
env expr
Expand All @@ -152,44 +157,31 @@ module%inlined_contents Make (F : Features.T) = struct
let rec analyse (func_dep : pre_data) (items : A.item list) : analysis_data =
let (mut_var_list, _)
: (concrete_ident * (U.TypedLocalIdent.t * id_order) list) list * _ =
List.fold_left
~f:(fun (y, count) x ->
match x.v with
| Fn { name; generics = _; body; params = _ } ->
let items, count = analyse_function_body body count in
(y @ [ (name, items) ], count)
| Impl
{
generics = _;
self_ty = _;
of_trait = _ (* name, gen_vals *);
items;
} ->
List.fold_left
~f:(fun (z, count) w ->
match w.ii_v with
| IIFn { body; params = _ } ->
let items, count = analyse_function_body body count in
(* let extra_item, count = ([(LocalIdent.{ name = w.ii_name ^ "_loc"; id = LocalIdent.ty_param_id_of_int 0 (\* todo *\) }, body.typ), count] : (U.TypedLocalIdent.t * id_order) list), count + 1 in *)
(z @ [ (w.ii_ident, items (* @ extra_item *)) ], count)
| _ -> (z, count))
~init:(y, count) items
| _ -> (y, count))
~init:([], 0) items
List.fold_left ~init:([], 0)
~f:(fun (y, count) (name, body) ->
let items, count = analyse_function_body body count in
(y @ [ (name, items) ], count))
(List.concat_map ~f:U.functions_of_item items)
in
let mut_map :
let mut_map (* Concrete_ident *) :
(Local_ident.t list * (U.TypedLocalIdent.t * id_order) list)
Map.M(Concrete_ident).t =
Map.M(String).t =
List.fold_left
~init:(Map.empty (module Concrete_ident))
~init:(Map.empty (module String (* Concrete_ident *)))
~f:(fun y (x_name, x_items) ->
Map.set y ~key:x_name
Map.set y
~key:(Uprint.Concrete_ident_view.to_definition_name x_name)
~data:
( List.map ~f:(fst >> fst) x_items
@ Option.value_map ~default:[]
~f:
(List.filter_map ~f:(Map.find y) >> List.concat_map ~f:fst)
(Map.find func_dep x_name),
(List.filter_map
~f:
(Uprint.Concrete_ident_view.to_definition_name
>> Map.find y)
>> List.concat_map ~f:fst)
(Map.find func_dep
(Uprint.Concrete_ident_view.to_definition_name x_name)),
x_items ))
mut_var_list
in
Expand Down

0 comments on commit e1f71bd

Please sign in to comment.