Trace Reconstruction

dafny/lcf/.gitignore

@@ -1 +1,5 @@
+# Compiled C# code
 *.dll
+# Test outputs
+*.trace
+*.thm

dafny/lcf/Makefile

@@ -9,15 +9,33 @@ def.cs: def.dfy
 bin/datalog.dll: datalog/datalog.csproj out/datalogParser.cs def.cs datalog/AstBuilder.cs datalog/Program.cs
 	dotnet build datalog/datalog.csproj --output bin
 
-examples/trace.out: examples/trace.pl
-	swipl -l $< > $@
+tests/%.trace: trace.pl tests/%.pl
+	swipl -l $< -g "consult('tests/$*.pl')" -g trace -g "go" -g notrace -g halt > $@
 
-.PHONY: check
-check: bin/datalog.dll examples/connectivity.pl examples/trace.out
-	dotnet $^
+tests/%.thm: bin/datalog.dll tests/%.pl tests/%.trace
+	dotnet $^ > $@
+
+TESTS=$(wildcard tests/*.pl)
+THMS=$(patsubst %.pl,%.thm,$(TESTS))
+
+.PHONY: test
+test: $(THMS)
+
+.PHONY: print
+print(%):
+	cat '$*'
+
+.PHONY: printtests
+printtests:
+	cat ${TESTS}
+
+.PHONY: printthms
+printthms:
+	cat ${THMS}
 
 .PHONY: clean
 clean:
 	$(RM) -r out
-	$(RM) examples/*.out
-	$(RM) def.cs
+	$(RM) tests/*.trace
+	$(RM) tests/*.thm
+	$(RM) def.cs

dafny/lcf/README.md

@@ -0,0 +1,20 @@
+## Project Overview
+
+The Veri-Datalog project is a verified Datalog+ engine. It proves the correctness of Datalog+ programs by constructing proof trees from their trace output. Datalog+ is a research defined language that is similar to Datalog but with more feature support; both are subsets of Prolog.
+
+## Contributions by Rory Brennan-Jones
+
+### Test Suite
+
+In the lcf directory, running `make test` will verify the go predicate of every Datalog+ file in the tests directory. The results are saved as .thm files with names matching the original code files. Using the Python script in the tools directory, it is possible to randomly generate example Datalog+ programs involving edge connectivity problems.
+
+### Trace Reconstruction
+
+The trace output of a Prolog program shows an exploration of many possible paths before settling on one that allows the query to be true
+or resolves some unification. The new trace reconstruction algorithm attempts to discard all the failed paths and look at just the successful path, which greatly simplifies the process of constructing a proof tree for that query. The algorithm does this by only looking at trace events that use the exit port, since these events result from successes and contain full variable assignments. However, failed paths can have zero or more temporary successes, potentially leading to the presence of "junk" events with exit ports in the trace output.
+
+Since exit ports always follow successes, the first exit ports in the trace happen after finding succesful base cases (builtin operations, facts, etc.), and later exit ports show the successes of predicates that depended on other rules and facts. As a result, the algorithm reads from the trace backwards in order to go from the root to the leaves instead of vice versa. The algorithm uses a mix of recursion and iteration, where the recursion helps the algorithm move "up" and "down" the tree, and the iteration helps algorithm move between siblings in the tree and skip junk events. A trace event with a prop such as a fact, equality, or builtin becomes a leaf in the proof tree, whereas other trace events become regular theorems that have proofs using other theorems and leaves from lower down in the tree as arguments.
+
+### Types and Builtins
+
+Unlike Datalog, Datalog+ supports constants other than atoms, including numbers, strings, and lists. These types are not complete yet. It has not been decided yet if the numbers should be natural numbers or integers (or if both should be supported). Furthermore, strings do not support all characters that could be found in a legal Datalog+ string, including escaped characters such as double quotes. Also, lists currently only support constant terms and cannot use the pipe operator. In addition to these types, there is also support for certain builtin operations, such as equality operators and string and list builtins.

dafny/lcf/datalog.g4

@@ -9,7 +9,7 @@ trace
   ;
 
 traceevent
-  : port level=integer id=integer goal=clause ';'
+  : port level=integer id=integer goal=clause';'
   ;
 
 port
@@ -37,26 +37,63 @@ rule
   ;
 
 clause
-  : name=Identifier '(' term_list ')'
+  : builtin
+  | app
+  | expression
+  ;
+
+builtin
+  : name=Builtin '(' term_list ')'
+  ;
+
+app
+  : name=Identifier ( '(' term_list ')' )?
+  ;
+
+expression
+  : left=term name=Operator right=term
   ;
 
 term
-  : atom
+  : constant
   | variable
   ;
 
+constant
+  : atom
+  | natural
+  | string
+  | list
+  ;
+
 clause_list
   : clause ( ',' clause)*
   ;
 
 term_list
-  : term( ',' term)*
+  : term ( ',' term)*
   ;
 
 atom
   : val=Identifier
   ;
 
+natural
+  : numeral=Int // TODO: make natural use the Nat rule, or switch support from natural numbers to integers
+  ;
+
+string
+  : s=Str
+  ;
+
+list
+  : '[' constant_list ']'
+  ;
+
+constant_list
+  : constant ( ',' constant)*
+  ;
+
 variable
   : name=VarName
   ;
@@ -65,6 +102,15 @@ variable
  * Lexer Rules
  */
 
+fragment CHARACTER
+  : ALPHANUMERIC // TODO: expand to all characters that are permitted by Prolog strings
+  | '.' | ',' | ';' | '!' | '?' | ' '
+  | '\t' | '\\t'
+  | '\n' | '\\n'
+  | '\r' | '\\r'
+  | '"' | '\\"'
+  | '\\'
+  ;
 fragment ALPHANUMERIC: ALPHA | DIGIT ;
 fragment ALPHA: '_' | SMALL_LETTER | CAPITAL_LETTER ;
 fragment LEADER: '_' | CAPITAL_LETTER;
@@ -76,10 +122,25 @@ Port
   : 'call' | 'redo' | 'unify' | 'exit' | 'fail'
   ;
 
+Builtin
+  : 'split_string'
+  | 'sub_string'
+  | 'string_lower'
+  | 'string_chars'
+  | 'length'
+  | 'lists:member' | 'member'
+  | 'lists:reverse' | 'reverse'
+  | 'lists:nth1' | 'nth1'
+  ;
+
 Identifier
 	: SMALL_LETTER (Nondigit | Digit)*
 	;
 
+Operator
+  : '=' | '=<' | '>=' | '\\=' | '=\\=' | '<' | '>' | '=='
+  ;
+
 VarName
   : LEADER (Nondigit | Digit)*
   ;
@@ -88,8 +149,16 @@ Int
 	: ('-')? Digit+
 	;
 
+Nat
+  : Digit+
+  ;
+
+Str
+  : '"' CHARACTER* '"' 
+  ;
+
 fragment Nondigit
-	: [a-zA-Z]
+	: [a-zA-Z] | '_'
 	;
 
 fragment Digit

dafny/lcf/datalog/AstBuilder.cs

@@ -70,16 +70,88 @@ private static int RuleID(ParserRuleContext context) {
       return context.Start.Line;
     }
 
-    public override object VisitClause(datalogParser.ClauseContext context) {
-      var name = Sequence<char>.FromString(context.name.Text);
+    public override object VisitBuiltin(datalogParser.BuiltinContext context) {
       var terms = (Dafny.ISequence<_ITerm>) VisitTerm_list(context.term_list());
-      return new _module.Prop_App(name, terms);
+      switch (context.name.Text) {
+        case "split_string":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_SplitString(), terms);
+        case "sub_string":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_SubString(), terms);
+        case "string_lower":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_StringLower(), terms);
+        case "string_chars":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_StringChars(), terms);
+        case "length":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_Length(), terms);
+        case "lists:member":
+           return new _module.Prop_BuiltinOp(new _module.Builtin_Member(), terms);
+        case "member":
+           return new _module.Prop_BuiltinOp(new _module.Builtin_Member(), terms);
+        case "lists:reverse":
+           return new _module.Prop_BuiltinOp(new _module.Builtin_Reverse(), terms);
+        case "reverse":
+           return new _module.Prop_BuiltinOp(new _module.Builtin_Reverse(), terms);
+        case "lists:nth1":
+           return new _module.Prop_BuiltinOp(new _module.Builtin_Nth1(), terms);
+        case "nth1":
+           return new _module.Prop_BuiltinOp(new _module.Builtin_Nth1(), terms);
+        default:
+          return null;
+      }
+    }
+
+    public override object VisitExpression(datalogParser.ExpressionContext context) {
+      var left = (_module.Term)VisitTerm(context.left);
+      var right = (_module.Term)VisitTerm(context.right);
+      var terms = new List<_module.Term> { left, right };
+      var terms2 = (Dafny.ISequence<_ITerm>) Sequence<_module.Term>.Create(terms.Count, i => terms[(int) i]);
+      switch(context.name.Text) {
+        case "=<":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_NatLeq(), terms2);
+        case ">=":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_NatGeq(), terms2);
+        case "\\=":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_NatNeq(), terms2);
+        case "=\\=":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_NatNeq(), terms2);
+        case "<":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_NatLt(), terms2);
+        case ">":
+          return new _module.Prop_BuiltinOp(new _module.Builtin_NatGt(), terms2);
+        default:
+          return new _module.Prop_Eq(left, right);
+      }
+    }
+
+    public override object VisitApp(datalogParser.AppContext context) {
+      var name = Sequence<char>.FromString(context.name.Text);
+      if (context.term_list() == null ) {
+        var terms = new List<_module.Term>();
+        var terms2 = Sequence<_module.Term>.Create(terms.Count, i => terms[(int) i]);
+        return new _module.Prop_App(name, (Dafny.ISequence<_ITerm>) terms2);
+      } else {
+        var terms = (Dafny.ISequence<_ITerm>) VisitTerm_list(context.term_list());
+        return new _module.Prop_App(name, terms);
+      }
     }
 
     public override object VisitAtom(datalogParser.AtomContext context) {
       return new Term_Const(new Const_Atom(Sequence<char>.FromString(context.val.Text)));
     }
 
+    public override object VisitNatural(datalogParser.NaturalContext context) {
+      return new Term_Const(new Const_Nat(BigInteger.Parse(context.numeral.Text)));
+    }
+
+    public override object VisitString(datalogParser.StringContext context) {
+      return new Term_Const(new Const_Str(Sequence<char>.FromString(context.s.Text.Substring(1, context.s.Text.Length - 2))));
+      // A substring of the text is taken in order to remove the double quotes.
+    }
+
+    public override object VisitList(datalogParser.ListContext context) {
+      return new Term_Const(new Const_List( (Dafny.ISequence<_IConst>) VisitConstant_list(context.constant_list()) ));
+    }
+
     public override object VisitVariable(datalogParser.VariableContext context) {
       return new Term_Var(Sequence<char>.FromString(context.name.Text));
     }
@@ -101,6 +173,15 @@ public override object VisitTerm_list(datalogParser.Term_listContext context) {
       }
       return Sequence<_module.Term>.Create(terms.Count, i => terms[(int) i]);
     }
+
+    public override object VisitConstant_list(datalogParser.Constant_listContext context) {
+      var consts = new List<_module.Const>();
+      foreach (var constant in context.constant()) {
+        var dafny_const = (_module.Const) ((_module.Term_Const) VisitConstant(constant))._val;
+        consts.Add(dafny_const);
+      }
+      return Sequence<_module.Const>.Create(consts.Count, i => consts[(int) i]);
+    }
   }
 
   public partial class __default

dafny/lcf/datalog/Program.cs

@@ -18,12 +18,14 @@ static void Main(string[] args) {
       try {
         // Parse rule set.
         var rules_parser = BuildParser(args[0]);
+        rules_parser.ErrorHandler = new BailErrorStrategy();
         var rules_parse_tree = rules_parser.program();
         var rules_ast_builder = new AstBuilder();
         var rules = (Sequence<_module.Rule>)rules_ast_builder.VisitProgram(rules_parse_tree);
 
         // Parse trace.
         var trace_parser = BuildParser(args[1]);
+        trace_parser.ErrorHandler = new BailErrorStrategy();
         var trace_parse_tree = trace_parser.trace();
         var trace_ast_builder = new AstBuilder();
         var trace = (Sequence<_module.Event>)trace_ast_builder.VisitTrace(trace_parse_tree);