Skip to content

Commit

Permalink
fix issues with dependency analysis
Browse files Browse the repository at this point in the history
  • Loading branch information
@wies
wies committed Oct 9, 2024
1 parent 0f1a69b commit 60147cf
Show file tree
Hide file tree
Showing 5 changed files with 76 additions and 52 deletions.
21 changes: 2 additions & 19 deletions lib/backend/checker.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -387,28 +387,12 @@ let check_members (mod_name : ident) (deps : QualIdent.t list list) : smt_env t
(Stdlib.Format.asprintf "Checking members in %a" Ident.pr mod_name)
in
let* _ = Rewriter.List.iter deps ~f:(fun dep ->
Logs.info (fun m -> m "Deps: %a" (Print.pr_list_comma QualIdent.pr) dep);
let* dep_sym = Rewriter.List.map dep ~f:(fun qual_name ->
let+ symbol = Rewriter.find_and_reify Loc.dummy qual_name in
(qual_name, symbol))
in
let sorted_dep =
List.sort dep_sym ~compare:(fun (qid1, sym1) (qid2, sym2) ->
match sym1, sym2 with
| CallDef call_def1, CallDef call_def2 ->
begin
match Callable.kind call_def1, Callable.kind call_def2 with
| (Pred | Func | Invariant), (Lemma | Proc) -> -1
| (Lemma | Proc), (Pred | Func | Invariant) -> 1
| _ ->
Loc.compare (Symbol.to_loc sym1) (Symbol.to_loc sym2)
end
| CallDef _, _ -> 1
| _, CallDef _ -> -1
| _ -> Loc.compare (Symbol.to_loc sym1) (Symbol.to_loc sym2)
)
in
Rewriter.List.iter sorted_dep ~f:(fun (qual_name, sym) -> check_member qual_name sym))
Logs.info (fun m -> m "Deps: %a" (Print.pr_list_comma QualIdent.pr) (List.map ~f:(fun (a,b) -> a) dep_sym));
Rewriter.List.iter dep_sym ~f:(fun (qual_name, sym) -> check_member qual_name sym))
in
let* _ = pop in

Expand All @@ -431,5 +415,4 @@ let check_module (module_def : Ast.Module.t) (tbl : SymbolTbl.t)
(check_members module_def.mod_decl.mod_decl_name dependencies))
tbl
in

smt_env
54 changes: 35 additions & 19 deletions lib/backend/dependencies.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,14 @@ let root_dependencies (tbl: SymbolTbl.t) (mdef: Module.t) (ag: Graph.t) =
| CallDef call_def ->
let+ qid = Rewriter.resolve (Symbol.to_loc sym) (Symbol.to_name sym |> QualIdent.from_ident) in
let deps = Callable.symbols call_def in
Logs.debug (fun m -> m "Dependencies.root_dependencies: Adding dependencies of callable %a: %a" QualIdent.pr qid (Print.pr_list_comma QualIdent.pr) (Set.elements deps));
Logs.info (fun m -> m "Dependencies.root_dependencies: Adding dependencies of callable %a: %a" QualIdent.pr qid (Print.pr_list_comma QualIdent.pr) (Set.elements deps));
Graph.add_edges g qid deps,
if (Callable.to_decl call_def).call_decl_is_auto
then Set.fold deps ~f:(fun g dep_qid ->
if List.equal Ident.(=) QualIdent.(path qid) QualIdent.(path dep_qid)
then Graph.add_edge g dep_qid qid else g) ~init:ag
then
let _ = Logs.info (fun m -> m "Dependencies.root_dependencies: adding auto dependency %a -> %a" QualIdent.pr dep_qid QualIdent.pr qid) in
Graph.add_edge g dep_qid qid else g) ~init:ag
else ag
(*| ConstrDef cdef -> ???
| DestrDef cdef -> ??? *)
Expand All @@ -50,8 +52,8 @@ let root_dependencies (tbl: SymbolTbl.t) (mdef: Module.t) (ag: Graph.t) =

(** Produce a topological sort of the strongly connected components in the dependency graph of module [mdef]. *)
(** Assumes that [tbl] is the symbol table and [mdef] the root module of the program. *)
let analyze (tbl: SymbolTbl.t) (mdef: Module.t) (ag: Graph.t): QualIdent.t list list * Graph.t =
let rec inst_dependencies todos covered g auto_g =
let analyze (tbl: SymbolTbl.t) (mdef: Module.t) (root_auto_g: Graph.t): QualIdent.t list list * Graph.t =
let rec inst_dependencies todos covered g auto_g root_auto_g =
let res =
let open Option.Syntax in
let+ qid = Set.choose todos in
Expand All @@ -60,41 +62,55 @@ let analyze (tbl: SymbolTbl.t) (mdef: Module.t) (ag: Graph.t): QualIdent.t list
let subst = Rewriter.Symbol.subst sym in
let orig_qid = Rewriter.Symbol.orig_qid sym in
let _, reified_sym = Rewriter.eval ~update:false (Rewriter.Symbol.reify sym) tbl in
let deps = match reified_sym with
let deps, auto_deps = match reified_sym with
| TypeDef type_def ->
Logs.debug (fun m -> m "Dependencies.analyze: Analyzing dependencies of type %a" Symbol.pr reified_sym);
Option.map type_def.type_def_expr ~f:Type.symbols |> Option.value ~default:Graph.empty_vertex_set
Option.map type_def.type_def_expr ~f:Type.symbols |> Option.value ~default:Graph.empty_vertex_set, Graph.empty_vertex_set
| CallDef call_def ->
let open Callable in
Logs.debug (fun m -> m "Dependencies.analyze: Analyzing dependencies of callable %a" Symbol.pr reified_sym);
begin match Callable.kind call_def with
| Func ->
let orig_auto_deps = Graph.succs auto_g orig_qid in
let orig_auto_deps = Graph.succs root_auto_g orig_qid in
let auto_deps = Set.map (module QualIdent) orig_auto_deps ~f:(QualIdent.requalify subst) in
Set.union auto_deps (Callable.symbols call_def)
Callable.symbols call_def, auto_deps
| Pred | Invariant | Lemma ->
Callable.symbols call_def
| _ -> Graph.empty_vertex_set
Callable.symbols call_def, Graph.empty_vertex_set
| _ -> Graph.empty_vertex_set, Graph.empty_vertex_set
end
| VarDef var_def ->
Logs.debug (fun m -> m "Dependencies.analyze: Analyzing dependencies of variable %a" Symbol.pr reified_sym);
let orig_auto_deps = Graph.succs root_auto_g orig_qid in
let auto_deps = Set.map (module QualIdent) orig_auto_deps ~f:(QualIdent.requalify subst) in
let deps = Option.map var_def.var_init ~f:Expr.symbols |> Option.value ~default:Graph.empty_vertex_set in
let deps = Set.union deps (Type.symbols var_def.var_decl.var_type) in
deps
| _ -> Graph.empty_vertex_set
deps, auto_deps
| _ -> Graph.empty_vertex_set, Graph.empty_vertex_set
in
Logs.info (fun m -> m "Dependencies.analyze: Adding dependencies of %a: %a" QualIdent.pr qid (Print.pr_list_comma QualIdent.pr) (Set.elements deps));
Logs.debug (fun m -> m "Dependencies.analyze: Adding dependencies of %a: %a" QualIdent.pr qid (Print.pr_list_comma QualIdent.pr) (Set.elements deps));
let g1 = Graph.add_edges g qid deps in
let auto_g1 = Graph.add_edges auto_g qid auto_deps in
let covered1 = Set.add covered qid in
let todos1 = Set.union (Set.remove todos qid) (Set.diff deps covered1) in
inst_dependencies todos1 covered1 g1 auto_g
let todos1 = Set.union (Set.remove todos qid) (Set.diff (Set.union auto_deps deps) covered1) in
inst_dependencies todos1 covered1 g1 auto_g1 root_auto_g
in
Option.value res ~default:g
Option.value res ~default:(g, auto_g)
in
Logs.debug (fun m -> m "Dependencies.analyze: Analyzing dependencies of module %a" Ident.pr mdef.mod_decl.mod_decl_name);
let root_g, auto_g = root_dependencies tbl mdef ag in
let root_g, root_auto_g1 = root_dependencies tbl mdef root_auto_g in
Logs.debug (fun m -> m "Dependencies.analyze: Root Dependencies done for module %a" Ident.pr mdef.mod_decl.mod_decl_name);
Logs.debug (fun m -> m "Dependencies.analyze: Root Dependencies for module %a: %a" Ident.pr mdef.mod_decl.mod_decl_name (Print.pr_list_comma QualIdent.pr) (Set.elements (Set.union (Graph.targets root_g) (Graph.vertices root_g))));
let roots = Graph.vertices root_g in
let targets = Graph.targets root_g in
let g = inst_dependencies (Set.diff targets roots) roots root_g auto_g in
Graph.topsort g, auto_g
Logs.debug (fun m -> m "Dependencies.analyze: targets for module %a: %a" Ident.pr mdef.mod_decl.mod_decl_name (Print.pr_list_comma QualIdent.pr) (Set.elements targets));
let g, full_g = inst_dependencies (Set.union targets roots) Graph.empty_vertex_set root_g Graph.empty root_auto_g1 in
Logs.debug (fun m -> m "Graph: %a" (Graph.pr QualIdent.pr) g);
let rank, _ =
List.fold_left (Graph.topsort g) ~init:(Map.empty (module QualIdent), 0)
~f:(fun rank_c sc ->
List.fold sc ~init:rank_c ~f:(fun (rank, c) v -> Map.set rank ~key:v ~data:c, c+1)
)
in
let scs = Graph.topsort (Graph.union g full_g) in
let symbols = List.map scs ~f:(List.sort ~compare:(fun v1 v2 -> compare (Map.find_exn rank v1) (Map.find_exn rank v2))) in
symbols, root_auto_g1
30 changes: 25 additions & 5 deletions lib/library/resource_algebra.rav
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ interface ResourceAlgebra : Type {
ensures forall a:T, b:T :: {comp(a, b)} valid(comp(a, b)) ==> valid(a) && valid(b)

auto axiom frameId()
ensures forall a:T :: {frame(a,id)} frame(a, id) == a
ensures forall a:T :: {frame(a,id)} valid(a) ==> frame(a, id) == a

auto axiom compFrameInv()
ensures forall a:T, b:T :: {comp(frame(a, b), b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a
Expand All @@ -49,6 +49,16 @@ interface CancellativeResourceAlgebra : ResourceAlgebra {
auto axiom frameCompInv()
ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> frame(comp(a, b), b) == a

lemma frameId()
ensures forall a:T :: {frame(a,id)} valid(a) ==> frame(a, id) == a
{
assert forall a:T :: {frame(a,id)} valid(a) ==> frame(a, id) == a with {
if (valid(a)) {
assert valid(comp(a, id));
}
}
}

lemma frameReflexive()
ensures forall a:T :: {frame(a,a)} valid(a) ==> frame(a, a) == id
{
Expand All @@ -66,7 +76,7 @@ interface CancellativeResourceAlgebra : ResourceAlgebra {
ensures forall a:T, b:T, c:T :: {comp(a,b),comp(c,b)} (valid(comp(a, b)) && comp(a,b) == comp(c,b) ==> (a == c))
{
//frameCompInv();
assert forall a:T, b:T, c:T :: (valid(comp(a, b)) && comp(a,b) == comp(c,b) ==> (a == c)) with {
assert forall a:T, b:T, c:T :: {comp(a,b),comp(c,b)} (valid(comp(a, b)) && comp(a,b) == comp(c,b) ==> (a == c)) with {
if (valid(comp(a, b)) && comp(a,b) == comp(c,b)) {
assert frame(comp(a, b), b) == a;
//assert frame(comp(c, b), b) == c;
Expand Down Expand Up @@ -117,17 +127,27 @@ interface LatticeResourceAlgebra : ResourceAlgebra {
ensures forall a:T, b:T :: {valid(frame(a, b))} valid(frame(a, b)) ==> frame(a, b) == a

auto axiom frameCompInv0()
ensures forall a:T, b:T :: {valid(comp(a, b))} valid(comp(a, b)) ==> frame(comp(a, b), b) == comp(a, b)
ensures forall a:T, b:T :: {valid(comp(a, b)),frame(comp(a, b), b)} valid(comp(a, b)) ==> frame(comp(a, b), b) == comp(a, b)

/*auto lemma frameId()
ensures forall a:T :: {frame(a,id)} valid(a) ==> frame(a, id) == a
{
assert forall a:T :: {frame(a,id)} valid(a) ==> frame(a, id) == a with {
if (valid(a)) {
assert valid(comp(a, id));
}
}
}*/

//TW: The following is implied by frameCompInv and frameCompInv0
//auto axiom frameCompInv2()
// ensures forall a:T, b:T :: comp(a, b) == a && valid(a) ==> frame(a, b) == a

auto axiom frame_comp_inv()
ensures forall a:T, b:T, c:T :: {frame(a, comp(b,c))} {frame(frame(a, b), c)} frame(a, comp(b,c)) == frame(frame(a, b), c)
ensures forall a:T, b:T, c:T :: {frame(a, comp(b,c)),frame(frame(a, b), c)} frame(a, comp(b,c)) == frame(frame(a, b), c)

lemma weak_frameCompInv()
ensures forall a:T, b:T:: {valid(comp(a,b))} valid(comp(a, b)) ==> valid(frame(comp(a, b), b))
ensures forall a:T, b:T:: {valid(comp(a,b)),frame(comp(a, b), b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b))
{}
}

Expand Down
13 changes: 12 additions & 1 deletion lib/util/graph.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,12 +48,23 @@ module Make (V : Vertex) = struct
let old_dsts = Option.value old_dsts_opt ~default:empty_vertex_set in
Set.union old_dsts dsts) )

let union (vs1, es1) (vs2, es2) =
Set.union vs1 vs2,
Map.merge es1 es2 ~f:(fun ~key m ->
Map.Merge_element.values m ~left_default:empty_vertex_set ~right_default:empty_vertex_set
|> (fun (e1, e2) -> Some (Set.union e1 e2)))

let succs (vs, es) v : VertexSet.t =
Map.find es v |> Option.value ~default:empty_vertex_set

let targets (vs, es) : VertexSet.t =
Map.fold es ~f:(fun ~key ~data -> Set.union data) ~init:empty_vertex_set

let pr pr_v ppf (vs, es) =
let pr_es ppf (v, vs) = Stdlib.Format.fprintf ppf "%a -> %a" pr_v v (Print.pr_list_comma pr_v) (Set.elements vs) in
Print.pr_list_nl pr_es ppf (Map.to_alist es)


let topsort ((vs, es) : t) : V.t list list =
let index = ref 0 in
let indexes = Hashtbl.create (module V) in
Expand All @@ -64,7 +75,7 @@ module Make (V : Vertex) = struct
Hashtbl.set indexes ~key:v ~data:!index;
Hashtbl.set lowlinks ~key:v ~data:!index;
Int.incr index;
let succs = Map.find_exn es v in
let succs = Map.find es v |> Option.value ~default:empty_vertex_set in
Stack.push s v;
let sccs1 : V.t list list =
Set.fold
Expand Down
10 changes: 2 additions & 8 deletions test/arrays/array_util.rav
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,15 +31,15 @@ interface OrderedType : Library.Type {
x == y ? 0 : (lt(x, y) ? -1 : 1)
}

val bot: T
/*val bot: T
val top: T

auto axiom bot_smallest()
ensures forall a: T :: {lt(a, bot)} !lt(a, bot)
auto axiom top_largest()
ensures forall a: T :: {lt(top, a)} !lt(top, a)
auto axiom nontrivial()
ensures bot != top
ensures bot != top*/

auto axiom lt_irreflexive()
ensures forall a: T :: {lt(a, a)} !lt(a, a)
Expand Down Expand Up @@ -401,9 +401,6 @@ interface ArrayUtil[K: OrderedType] {
found := false;
} else {
unfold sorted_array_with_content(a, len, m);
// assume false;
A.all_diff();
A.len_nonneg();
unfold arr(a, m);
var alo: K := A.loc(a, lo).A.value;
found := !lt(k, alo);
Expand Down Expand Up @@ -443,9 +440,6 @@ interface ArrayUtil[K: OrderedType] {
unfold sorted_array_with_content(a, len, m);
arr_shift(a, i, i + 1, len - i, m);

//assume false;
A.all_diff();
A.len_nonneg();
unfold arr(a, map_shift(m, i, i + 1, len - i));
A.loc(a, i).A.value := k;
m1 := map_shift(m, i, i + 1, len - i)[i := k];
Expand Down

0 comments on commit 60147cf

Please sign in to comment.