Implement entities database and auditor #11

atomb · 2022-09-07T23:25:24Z

Creates a database of program entities (modules, types, definitions, etc.) and updates the translator to handle an entire program instead of a single method.

On top of this, implements an auditor for Dafny, focused initially on producing a report summarizing all assumptions in a program (addressing dafny-lang/dafny#2236).

atomb · 2022-09-07T23:27:32Z

src/Tools/Auditor/Auditor.dfy

+
+//// AST traversals ////
+
+function {:opaque} Any<T>(P: T ~> bool, ts: seq<T>) : (b: bool)


This should go in the standard library

Can we move it to our own library for now?

I removed it as it's no longer used.

atomb · 2022-09-07T23:36:32Z

src/Utils/Lib.Sort.dfy

@@ -0,0 +1,450 @@
+include "Library.dfy"


We should eventually move as much as possible of this file and Library.dfy into https://github.com/dafny-lang/libraries.

atomb · 2022-09-07T23:38:24Z

src/AST/Entities.dfy

+  import Utils.Lib.SetSort
+  import OS = Utils.Lib.Outcome.OfSeq
+
+  // DISCUSS: Should this module be parameterized by `TExpr`?


I could see value in doing so, but I'd be inclined to only change it if we have a concrete use case, along with the change to implement that use case.

atomb · 2022-09-07T23:46:18Z

src/AST/Translator.Common.dfy

+
+  datatype TranslationError =
+    | Invalid(msg: string)
+    | GhostExpr(expr: C.Expression)


We could remove this and use Unsupported instead.

atomb · 2022-09-07T23:46:23Z

src/AST/Translator.Common.dfy

+    | GhostExpr(expr: C.Expression)
+    | UnsupportedType(ty: C.Type)
+    | UnsupportedExpr(expr: C.Expression)
+    | UnsupportedStmt(stmt: C.Statement)


We could get rid of this now that it's no longer used. And we could almost get rid of UnsupportedExpr, too.

atomb · 2022-09-07T23:50:36Z

src/AST/Translator.Entity.dfy

+    else if md is C.Method then
+      TranslateMethod(md)
+    else
+      Failure(Invalid("Unsupported member declaration type: " + TypeConv.AsString(md.FullName)))


We should add an unsupported entity constructor and return Success with it here.

atomb · 2022-09-07T23:51:18Z

src/AST/Translator.Entity.dfy

+    // TODO: handle nonnull types
+    var x := TypeConv.AsString(st.Var.Name);
+    var ty :- Expr.TranslateType(st.Rhs);
+    var constraint :-Expr.TranslateExpression(st.Constraint);


Suggested change

var constraint :-Expr.TranslateExpression(st.Constraint);

var constraint :- Expr.TranslateExpression(st.Constraint);

atomb · 2022-09-07T23:51:38Z

src/AST/Translator.Entity.dfy

+    var x := TypeConv.AsString(st.Var.Name);
+    var ty :- Expr.TranslateType(st.Rhs);
+    var constraint :-Expr.TranslateExpression(st.Constraint);
+    var wit :-Expr.TranslateOptionalExpression(st.Witness);


Suggested change

var wit :-Expr.TranslateOptionalExpression(st.Witness);

var wit :- Expr.TranslateOptionalExpression(st.Witness);

atomb · 2022-09-07T23:52:00Z

src/AST/Translator.Entity.dfy

+    var x := TypeConv.AsString(nt.Var.Name);
+    var ty :- Expr.TranslateType(nt.BaseType);
+    var constraint :- Expr.TranslateOptionalExpression(nt.Constraint);
+    var wit :-Expr.TranslateOptionalExpression(nt.Witness);


Suggested change

var wit :-Expr.TranslateOptionalExpression(nt.Witness);

var wit :- Expr.TranslateOptionalExpression(nt.Witness);

atomb · 2022-09-07T23:52:39Z

src/AST/Translator.Entity.dfy

+               else if tl is C.ClassDecl then
+                 TranslateClassDecl(tl)
+               else
+                 Failure(Invalid("Unsupported top level declaration type for " + TypeConv.AsString(tl.FullName)));


Also return Success(Unsupported(...)) here.

atomb · 2022-09-07T23:53:00Z

src/AST/Translator.Entity.dfy

+      assume ASTHeight(md.Signature) < ASTHeight(tl);
+      TranslateModule(md.Signature)
+    else
+      Failure(Invalid("Unsupported top level declaration type for " + TypeConv.AsString(tl.FullName)))


Also return Success(Unsupported(...)) here.

atomb · 2022-09-07T23:54:00Z

src/AST/Translator.Entity.dfy

+    var topDecls' := Seq.Flatten(topDecls);
+    var topNames := Seq.Map((d: E.Entity) => d.ei.name, topDecls');
+    //:- Need(forall nm <- topNames :: nm.ChildOf(name), Invalid("Malformed name in " + name.ToString()));
+    assume forall nm <- topNames :: nm.ChildOf(name);


Remove this and use Need again.

atomb · 2022-09-07T23:54:51Z

src/AST/Translator.Entity.dfy

+        var prog := E.Program(reg, defaultModule := defaultModuleName, mainMethod := mainMethodName);
+        if prog.Valid?() then Success(prog) else Failure(Invalid("Generated invalid program"))
+      case Fail(errs) =>
+        var err := Seq.Flatten(Seq.Map((e: E.ValidationError) => e.ToString(), errs));


Make this message prettier.

src/AST/Translator.Entity.dfy

atomb · 2022-09-07T23:56:34Z

src/AST/Translator.Expressions.dfy

+    reads *
+    decreases ASTHeight(ue), 0
+  {
+    var children := []; // TODO: ListUtils.ToSeq(ue.SubExpressions);


Implement ListUtils.ToSeq but for IEnumerable.

atomb · 2022-09-07T23:57:19Z

src/AST/Translator.Expressions.dfy

-    var stmts :- Seq.MapResult(ListUtils.ToSeq(m.Body.Body), TranslateStatement);
-    Success(D.Method("Main", DE.Block(stmts)))
+    var subexprs := []; // TODO: ListUtils.ToSeq(ue.SubExpressions);
+    var substmts := []; // TODO: ListUtils.ToSeq(ue.SubStatements);


Implement ListUtils.ToSeq but for IEnumerable.

atomb · 2022-09-07T23:58:27Z

src/Backends/CSharp/Compiler.dfy

-    }
+    var names := p.registry.SortedNames();
+    var entities := Seq.Map(p.registry.Get, names);
+    // TODO: prove


Either prove this entirely or just for the Main method.

atomb · 2022-09-07T23:58:47Z

src/Backends/CSharp/Compiler.dfy

@@ -300,11 +315,14 @@ module Compiler {
          // but it seems cleaner to state that we need ``NotANegatedBinopExpr`` in the
          // preconditions, as it is more precise and ``Tr_Expr_Post`` might be expanded
          // in the future.
+          // TODO: need to redo this for all the entities in the program


Or just for the Main method.

atomb · 2022-09-08T00:01:43Z

src/Transforms/BottomUp.dfy

-    Map_Expr_PreservesRel(m.methodBody, tr, rel);
-  }
-
+/*


Uncomment this and prove it so we can use it to prove transformations correct.

atomb · 2022-09-08T00:02:29Z

src/Transforms/Shallow.dfy

+    e requires Shallow.All_Entity(e, tr.f.requires) => Map_Entity(e, tr)
+  }
+
+  // TODO: prove!


Prove this!

Let's create an issue for this

atomb · 2022-09-08T00:03:18Z

src/Passes/Pass.dfy

@@ -20,5 +22,6 @@ module Bootstrap.Passes.Pass {
  // the input and the output.
    requires Tr_Pre(p)
    ensures Tr_Post(p)
-    ensures EqInterp(p.mainMethod.methodBody, p'.mainMethod.methodBody)
+    // TODO!


Prove this!

atomb · 2022-09-08T00:03:50Z

src/Passes/SimplifyEmptyBlocks.dfy

    // Apply the transformation to a program.
  {
    Deep.All_Expr_True_Forall(Tr_Expr.f.requires);
    assert Deep.All_Program(p, Tr_Expr.f.requires);
    EqInterp_Lift(Tr_Expr.f);
-    Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel);
+    //Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel);


Hopefully this will go through as-is one Map_Program_PreservesRel goes through.

atomb · 2022-09-08T00:04:43Z

src/Passes/EliminateNegatedBinops.dfy

    // Apply the transformation to a program.
  {
    Deep.All_Expr_True_Forall(Tr_Expr.f.requires);
    assert Deep.All_Program(p, Tr_Expr.f.requires);
    TrPreservesRel();
-    Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel);
+    //Map_Program_PreservesRel(p, Tr_Expr, Tr_Expr_Rel);


Hopefully this will go through as-is (with the ensures clause back in place) once Map_Program_PreservesRel exists again.

keyboardDrummer · 2022-09-08T15:34:49Z

Is there an issue that this PR relates to? Maybe we could add one in https://github.com/dafny-lang/dafny ?

atomb · 2022-09-08T16:03:22Z

Is there an issue that this PR relates to? Maybe we could add one in https://github.com/dafny-lang/dafny ?

I just edited the description to be non-empty and include a reference to the relevant issue.

cpitclaudel

Neat, just read through the whole thing, and it's looking pretty good!

GNUmakefile

src/AST/Entities.dfy

src/Utils/Library.dfy

src/AST/Translator.Entity.dfy

src/Tools/Auditor/assets/template.html

The Failure case now should only occur for malformed ASTs, and unsupported constructs should use Success(Unuspported(...)).

* Mark `List` and `Dictionary` parameters nullable when they are that. * Sort dictionary keys to ensure that `DictUtils.FoldL` is a function. * Include `reads` clauses on Dafny `{:extern}` functions for above.

* Change assumption collection process. * Improve text of error message on failure to translate program.

The compiler keeps it in, even if it’s marked ghost, leading to later compilation failures. Let’s reduce it to a smaller example and file a compiler issue about it.

Avoid using `Need` to check types.

These all have issues, but these comments help make plans more immediately clear when browsing the code.

atomb requested a review from cpitclaudel September 7, 2022 23:25

atomb commented Sep 7, 2022

View reviewed changes

src/AST/Translator.Entity.dfy Show resolved Hide resolved

atomb commented Sep 7, 2022

View reviewed changes

atomb commented Sep 8, 2022

View reviewed changes

cpitclaudel requested changes Sep 8, 2022

View reviewed changes

cpitclaudel reviewed Sep 13, 2022

View reviewed changes

src/Tools/Auditor/assets/template.html Show resolved Hide resolved

atomb mentioned this pull request Sep 13, 2022

Prove semantics preservation after translation of whole programs #23

Open

atomb force-pushed the cpitclaudel_entities-impl branch from 63a4438 to fff0d4f Compare September 13, 2022 23:10

atomb and others added 26 commits September 14, 2022 02:21

build: Remove obsolete post-processing of C# code

c514461

ast: Minor syntactic cleanups

8a0e6de

ast: Add EntityInfo to Entity.Unsupported

4ee4767

interp: Fix Unsupported expressions

936118c

lib: Add Option.All

bbbb801

; auditor: Syntactic cleanups

78126ab

lib: Add Option.Map

b4ee536

auditor: Adjust the set of tags

f71a09d

lib: Improve Break and Split

efcd950

ast: Refactor error handling in expression translation

1f3d1f7

The Failure case now should only occur for malformed ASTs, and unsupported constructs should use Success(Unuspported(...)).

interop: More correct List, Dictionary treatment

388e894

* Mark `List` and `Dictionary` parameters nullable when they are that. * Sort dictionary keys to ensure that `DictUtils.FoldL` is a function. * Include `reads` clauses on Dafny `{:extern}` functions for above.

; auditor: Minor refactoring

913b011

* Change assumption collection process. * Improve text of error message on failure to translate program.

auditor: Add some support for decreases *

3f0c810

ast: Properly translate module children

1e16c64

ast: Improve registry validation error messages

999f530

transform: Whitespace only

af643b8

ast: Support traversing IEnumerables in AST nodes

052bfcc

auditor: Support multiple output formats

4b78426

ast: Add BUG comment about ghost parameter

b677d62

The compiler keeps it in, even if it’s marked ghost, leading to later compilation failures. Let’s reduce it to a smaller example and file a compiler issue about it.

ast: Refactor translation of UnaryOpExpr

87c51ce

Avoid using `Need` to check types.

src: Include some TODO comments

7583d80

These all have issues, but these comments help make plans more immediately clear when browsing the code.

; ast: Add two TODO comments in Entities.dfy

b99af8c

; repl: Add a pointer to dafny-lang/dafny#2740

b8d5091

; ast: Remove to DISCUSS markers

bd843a1

src: Use // syntax for docstrings and /// syntax for sections

8ef4afa

; ast: Add a link in a BUG comment

28299a2

cpitclaudel force-pushed the cpitclaudel_entities-impl branch from 12641cc to 28299a2 Compare September 14, 2022 09:51

cpitclaudel merged commit 28299a2 into main Sep 14, 2022

cpitclaudel deleted the cpitclaudel_entities-impl branch September 14, 2022 10:02

atomb mentioned this pull request Sep 27, 2022

Feature: Provide summary of all assumptions in a Dafny program dafny-lang/dafny#2236

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement entities database and auditor #11

Implement entities database and auditor #11

atomb commented Sep 7, 2022 •

edited

Loading

atomb Sep 7, 2022

cpitclaudel Sep 8, 2022

atomb Sep 12, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 7, 2022

atomb Sep 8, 2022

atomb Sep 8, 2022

cpitclaudel Sep 13, 2022

atomb Sep 8, 2022

atomb Sep 8, 2022

atomb Sep 8, 2022

keyboardDrummer commented Sep 8, 2022

atomb commented Sep 8, 2022

cpitclaudel left a comment


		//// AST traversals ////

		function {:opaque} Any<T>(P: T ~> bool, ts: seq<T>) : (b: bool)

	var constraint :-Expr.TranslateExpression(st.Constraint);
	var constraint :- Expr.TranslateExpression(st.Constraint);

	var wit :-Expr.TranslateOptionalExpression(st.Witness);
	var wit :- Expr.TranslateOptionalExpression(st.Witness);

Implement entities database and auditor #11

Implement entities database and auditor #11

Conversation

atomb commented Sep 7, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented Sep 8, 2022

atomb commented Sep 8, 2022

cpitclaudel left a comment

Choose a reason for hiding this comment

atomb commented Sep 7, 2022 •

edited

Loading