Shape analysis

prover/README.md

@@ -1,39 +1,64 @@
-Build Instructions
+Building
+========
+
+Besides the normal K dependencies, the matching logic prover also depends on
+`pandoc-tangle`, `python3` and `ninja-build`.
+On an Ubuntu Bionic (18.04) system you can install the following packages:
+
+```
+apt install autoconf curl flex gcc libffi-dev libmpfr-dev libtool make         \                        
+            maven ninja-build opam openjdk-8-jdk pandoc pkg-config python3     \                        
+            time zlib1g-dev                           
+```
+
+Source organization
+===================
+
+The source code is organized under the following directories:
+
+* `drivers/`: Modules for reading input formats and converting them to the
+   matching logic `kore` format, and loading them into the configuration.
+* `lang/`: Tools for working with the source languages (kore and smtlib)
+* `strategies/`: The various proof rules are implemented as "strategies".
+
+  * `strategies/core.md`: Core strategies, such as composition and choice.
+  * `strategies/knaster-tarski.md`: Strategies relating to using the Knaster Tarki rule
+    and contexts.
+  * `strategies/unfolding.md`: Strategies relating to unfolding fixed points.
+  * `strategies/matching.md`: Strategies relating to pattern matching
+  * `strategies/smt.md`: Strategies that utilize an SMT solver.
+
+Tests & Benchmarks
 ==================
 
-Install these dependencies:
+Organization
+-------------
 
-* pandoc
-* ninja-build
-* opam
-* maven
-* openjdk-11-jdk
+The tests and benchmarks are stored under the `t/` directory in the following
+subdirectories:
 
-Run `./build` to run all tests.
-Run `./build .build/t/TEST-NAME.smt2.prover-smt-krun` to run an individual test.
+* `t/ltl`: LTL Tests.
+* `t/sl`: Separation Logic tests and benchmarks.
+    * `t/sl/SL-COMP18/`: This is a git submodule containing all the `SL-COMP` tests.
+    * `t/sl/SL-COMP18/bench/qf_shid_entl/`: These are the benchmarks we aim to complete.
+* `t/fol`: FOL Tests.
 
-Repository Layout
-=================
+In addition, unit tests are stored under `t/unit/`
 
- * `prover.md` contains the implementation
- * `direct-proof.md` contains solutions to domain specific queries that
-   can be checked against an SMT solver.
- * The `t/` directory contains a number of tests and experiments, detailed below.
+File formats
+------------
 
-Tests & Experiments
-===================
+The prover accepts two file formats:
+
+1. `.kore`: This is the "native" matching logic based format that the prover accepts.
+2. `.smt`: This is the [SMT-LIB 2.6 format] with the [extensions for SL-COMP]
+
+[SMT-LIB 2.6 format]: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
+[extensions for SL-COMP]: https://sl-comp.github.io/docs/smtlib-sl.pdf
+
+Running tests
+=============
 
-In the `t/` directory, we have a number of tests. Each test consists of a
-"claim" (the matching logic pattern that we are trying to prove), and a
-strategy. The strategy directs the prover in choosing which axioms to apply. The
-`search-bound(N)` strategy causes the prover to begin a bounded depth first
-search for a proof of the claim. All lemmas named in the paper except one
-(`t/lsegright-list-implies-list`; see below) are proved with a search depth of 5
-or lower. The program verification example is proved with a search up to depth
-3. In addition, there is an example of a coninductive proof
-(`t/zip-zeros-ones-implies-alters.prover`; see below).
-
-The `t/zip-zeros-ones-implies-alters.prover` test proof is at a depth of 17,
-and so we specify the strategy to reduce the search space.
-The `t/lsegright-list-implies-list` test needs some help in instantiating
-existential variables, which is done by specifying a strategy as a substitution.
+* To run a select group of tests, called the "smoke-tests", run: `./build smoke-tests`.
+* To run a single kore test named "t/foo.kore", run `./build .build/t/foo.kore.prover-kore-run`
+* To run a single smt test named "t/foo.smt", run `./build .build/t/foo.kore.prover-smt-run`

prover/build

@@ -61,8 +61,9 @@ prover_smt  = prover('prover-smt',  '--main-module DRIVER-SMT  --syntax-module D
 # Functional tests
 # ----------------
 
-# prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
-# prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
+prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
+prover_kore.tests(inputs = glob('t/ltl/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
+prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
 
 def log_on_success(file, message):
     return proj.rule( 'log-to-success'
@@ -105,7 +106,7 @@ def make_test(rule, test):
 
 def sl_comp_test(test, log_file):
     global tests_with_timeout
-    test_no_timeout   = make_test(prover_smt.krun(), test)
+    test_no_timeout   = make_test(prover_smt.krun().ext('prover-smt-run'), test)
     test_with_timeout = make_test(krun_with_timeout(timeout_for_test(test)), test) \
                           .then(log_on_success(log_file, test))
     return (test_no_timeout, test_with_timeout)
@@ -131,8 +132,11 @@ secondary_tests('qf_shidlia_entl_unsat_tests', 't/test-lists/qf_shidlia_entl.uns
 secondary_tests('qf_shlid_entl_unsat_tests',   't/test-lists/qf_shlid_entl.unsat')
 secondary_tests('shid_entl_unsat_tests',       't/test-lists/shid_entl.unsat')
 
+# TODO: Why are smt tests `-krun` and kore tests `-run`?
+def test_path(name, type):
+    return ".build/t/%s.%s" % (name, type)
 def sl_comp_test_path(name):
-    return ".build/t/SL-COMP18/bench/qf_shid_entl/%s.prover-smt-krun" % (name)
+    return test_path("SL-COMP18/bench/qf_shid_entl/%s" % name, 'prover-smt-krun')
 
 proj.alias('smoke-tests', list(map( sl_comp_test_path, [ 
            "02.tst.smt2"                         , # RList trans 
@@ -145,9 +149,12 @@ proj.alias('smoke-tests', list(map( sl_comp_test_path, [
            "skl2-vc03.smt2"                      , # needs framing but not match-pto 
            "odd-lseg3_slk-5.smt2"                , # needs framing and match-pto 
            "nll-vc01.smt2"                       , # needs large number of unfolding but no kt
-           "ls_nonrec_entail_ls_07.sb.smt2"      , # 6 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5)  - needs large number of kts and unfolding
+           "ls_nonrec_entail_ls_05.sb.smt2"      , # 4 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5)  - needs large number of kts and unfolding
            "ls_lsrev_concat_entail_ls_1.sb.smt2" , # need unfolding within implication context
-          ])))
+          ])) +
+          [ test_path('listSegmentLeft-implies-listSegmentRight.kore', 'prover-kore-run')
+          ]
+          )
 
 # Unit Tests
 # ----------

prover/drivers/base.md

@@ -2,8 +2,8 @@ Configuration
 =============
 
 The configuration consists of a list of goals. The first goal is considered
-active. The `<k>` cell contains the Matching Logic Pattern for which we are
-searching for a proof. The `<strategy>` cell contains an imperative language
+active. The `<claim>` cell contains the Matching Logic Pattern for which we are
+searching for a proof. The `<k>` cell contains an imperative language
 that controls which (high-level) proof rules are used to complete the goal. The
 `<trace>` cell stores a log of the strategies used in the search of a proof and
 other debug information. Eventually, this could be used for constructing a proof
@@ -23,11 +23,11 @@ module PROVER-CONFIGURATION
       <prover>
         <exit-code exit=""> 1 </exit-code>
         <goals>
-          <goal multiplicity="*" type="List" format="%1%i%n%2, %3%n%4%n%5n%6%n%7%n%d%8">
+          <goal multiplicity="*" type="List" format="%1%i%n%2, %3%n%4%n%5%n%6%n%7%n%d%8">
             <id format="id: %2"> .K </id>
             <parent format="parent: %2"> .K </parent>
+            <claim> \or(.Patterns) </claim> // TODO: make this optional instead?
             <k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>
-            <strategy> .K </strategy>
             <expected> .K </expected>
             <local-context>
               <local-decl multiplicity="*" type="Set">  .K </local-decl>
@@ -91,7 +91,7 @@ module DRIVER-BASE
          <goal>
            <id> .K </id>
            <expected> .K </expected>
-           <strategy> .K </strategy>
+           <k> .K </k>
            ...
          </goal>
        </goals>

prover/drivers/kore-driver.md

@@ -71,6 +71,7 @@ in the subgoal and the claim of the named goal remains intact.
         => subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT))
            ...
        </k>
+  rule <k> (success => .K) ~> D:Declarations ... </k>
 ```
 
 ```k

prover/drivers/smt-driver.md

@@ -138,9 +138,10 @@ module DRIVER-SMT
        </k>
        <declarations> ( .Bag
                      => <declaration> symbol pto(SMTLIB2SortToSort(LOC), SMTLIB2SortToSort(DATA)) : Heap </declaration>
-                        <declaration> symbol parameterizedSymbol(nil, SMTLIB2SortToSort(LOC)) ( .Sorts ) : SMTLIB2SortToSort(LOC) </declaration>
+                        <declaration> symbol nil { SMTLIB2SortToSort(LOC) } (.Sorts) : SMTLIB2SortToSort(LOC) </declaration>
                         <declaration> axiom !N:AxiomName : heap(SMTLIB2SortToSort(LOC), SMTLIB2SortToSort(DATA)) </declaration>
-                        <declaration> axiom !N:AxiomName : functional(parameterizedSymbol(nil, SMTLIB2SortToSort(LOC))) </declaration>
+                        <declaration> axiom !M:AxiomName : functional(nil { SMTLIB2SortToSort(LOC) }) </declaration>
+                        <declaration> axiom !P:AxiomName : constructor(nil { SMTLIB2SortToSort(LOC) }) </declaration>
                       ) ...
        </declarations>
 
@@ -159,6 +160,7 @@ module DRIVER-SMT
                      => <declaration> sort SMTLIB2SortToSort(SORT1) </declaration>
                         <declaration> symbol SMTLIB2SimpleSymbolToSymbol(CTOR)(SelectorDecListToSorts(SELDECs)) : SMTLIB2SortToSort(SORT1) </declaration>
                         <declaration> axiom !N:AxiomName : functional(SMTLIB2SimpleSymbolToSymbol(CTOR)) </declaration>
+                        <declaration> axiom !M:AxiomName : constructor(SMTLIB2SimpleSymbolToSymbol(CTOR)) </declaration>
                       ) ...
        </declarations>
 
@@ -185,18 +187,18 @@ module DRIVER-SMT
                       ) ...
        </declarations>
 
-  syntax K ::= #rest(SMTLIB2FunctionDecList, SMTLIB2TermList)
+  syntax K ::= #mutualRecUnfold(SMTLIB2FunctionDecList, SMTLIB2TermList)
 
   rule <k> _:GoalBuilder
-        ~> ( #rest(_, _)
+        ~> ( #mutualRecUnfold(_, _)
           ~> (define-funs-rec ( .SMTLIB2FunctionDecList ) ( .SMTLIB2TermList ) )
           => .K
            )
            ...
        </k>
 
   rule <k> #goal( goal: _, strategy: unfold-mut-recs . REST_STRAT, expected: _ )
-        ~> (.K => #rest(FDs, BODIEs))
+        ~> (.K => #mutualRecUnfold(FDs, BODIEs))
         ~> (define-funs-rec ( FDs ) ( BODIEs ) )
            ...
        </k>
@@ -217,7 +219,7 @@ module DRIVER-SMT
        </k>
     requires notBool #matchesUnfoldMutRecs(STRAT)
 
-  rule <strategy> unfold-mut-recs => noop ... </strategy>
+  rule <k> unfold-mut-recs => noop ... </k>
 
   syntax Bool ::= #matchesUnfoldMutRecs(Strategy) [function]
   rule #matchesUnfoldMutRecs(unfold-mut-recs) => true
@@ -226,7 +228,7 @@ module DRIVER-SMT
     [owise]
 
   rule <k> _:GoalBuilder
-        ~> #rest(FDALLs, BODYALLs)
+        ~> #mutualRecUnfold(FDALLs, BODYALLs)
         ~> ( (define-funs-rec ( (ID (ARGs) RET) FDs ) ( BODY BODIEs ) )
           => unfoldMR( SMTLIB2SimpleSymbolToSymbol(ID)(SMTLIB2SortedVarListToPatterns(ARGs))
                      , SMTLIB2TermToPattern(BODY, SMTLIB2SortedVarListToPatterns(ARGs))
@@ -252,7 +254,7 @@ module DRIVER-SMT
        ), #gatherRest(FDs, BODIEs)
 
   syntax K ::= unfoldMR(Pattern, Pattern, PatternTupleList)
-  rule <k> _:GoalBuilder ~> #rest(_, _)
+  rule <k> _:GoalBuilder ~> #mutualRecUnfold(_, _)
         ~> ( unfoldMR(ID:Symbol(ARGs), BODY, .PatternTupleList)
           => .K
            )
@@ -267,14 +269,14 @@ module DRIVER-SMT
                       ) ...
        </declarations>
 
-  rule <k> _:GoalBuilder ~> #rest(_, _)
+  rule <k> _:GoalBuilder ~> #mutualRecUnfold(_, _)
         ~> ( unfoldMR(ID:Symbol(ARGs1), BODY1, ((ID:Symbol(ARGs2), BODY2), REST))
           => unfoldMR(ID:Symbol(ARGs1), BODY1, REST)
            )
            ...
        </k>
 
-  rule <k> _:GoalBuilder ~> #rest(_, _)
+  rule <k> _:GoalBuilder ~> #mutualRecUnfold(_, _)
         ~> ( unfoldMR(ID1:Symbol(ARGs1), BODY1, ((ID2:Symbol(ARGs2), BODY2), REST))
           => unfoldMR(ID1:Symbol(ARGs1), substituteBRPs(BODY1, ID2, ARGs2, BODY2), REST)
            )
@@ -319,23 +321,20 @@ module DRIVER-SMT
   rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S)
 
   syntax KItem ::= "expect" TerminalStrategy
-  rule <strategy> S ~> expect S => .K ... </strategy>
+  rule <k> S ~> expect S => .K ... </k>
 
-  rule <goals>
-         <k> #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
+  rule <k> ( #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
           ~> (check-sat)
-          => #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
-             ...
-         </k>
-         <strategy> .K
-                 => subgoal(\implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
-                           , STRAT
-                           )
-                 ~> expect EXPECTED
-         </strategy>
-         ...
-       </goals>
-   requires notBool PATTERN ==K  \exists { .Patterns } \and ( .Patterns )
+           )
+        => ( subgoal(\implies( \and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
+                    , STRAT
+                    )
+        ~>   #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
+           )
+           ...
+       </k>
+    requires notBool PATTERN ==K  \exists { .Patterns } \and ( .Patterns )
+  rule <k> (success => .K) ~> #goal( goal: _, strategy: _, expected: _) ... </k>
 ```
 
 ```k
@@ -404,13 +403,9 @@ Clear the `<k>` cell once we are done:
   rule #removeExistentialsPatterns(P, Ps) => #removeExistentials(P) ++Patterns #removeExistentialsPatterns(Ps)
   rule #removeExistentialsPatterns(.Patterns) => .Patterns
 
-  syntax Pattern ::= #normalizeQFree(Pattern) [function]
-                   | #normalizeDefinition(Pattern) [function]
+  syntax Pattern ::= #normalizeDefinition(Pattern) [function]
                    | #pushExistentialsDisjunction(Pattern) [function]
-  rule #normalizeDefinition(P) => #pushExistentialsDisjunction(\exists { #getExistentialVariables(P) } #normalizeQFree(#removeExistentials(P)))
-  rule #normalizeQFree(\or(Ps)) => \or(#flattenOrs(#dnfPs(Ps)))
-  rule #normalizeQFree(P) => #normalizeQFree(\or(P, .Patterns))
-    [owise]
+  rule #normalizeDefinition(P) => #pushExistentialsDisjunction(\exists { #getExistentialVariables(P) } #flattenAssoc(#liftOr(#nnf(\or(\and(#removeExistentials(P)))))))
   rule #pushExistentialsDisjunction(\exists{Vs} \or(Ps)) => \or(#exists(Ps, Vs))
 
   syntax Strategy ::= #statusToTerminalStrategy(CheckSATResult) [function]
@@ -437,7 +432,7 @@ Clear the `<k>` cell once we are done:
   rule SMTLIB2TermToPattern(I:Int, _) => I
   rule SMTLIB2TermToPattern(#token("true", "LowerName"), _) => \top()
   rule SMTLIB2TermToPattern(#token("false", "LowerName"), _) => \bottom()
-  rule SMTLIB2TermToPattern((as nil SORT), _) => parameterizedSymbol(nil, SMTLIB2SortToSort(SORT))(.Patterns)
+  rule SMTLIB2TermToPattern((as nil SORT), _) => nil { SMTLIB2SortToSort(SORT) } (.Patterns)
   rule SMTLIB2TermToPattern((underscore emp _ _), _) => emp(.Patterns)
 
   rule SMTLIB2TermToPattern((ID Ts), Vs) => SMTLIB2SimpleSymbolToSymbol(ID)(SMTLIB2TermListToPatterns(Ts, Vs))

prover/drivers/unit-tests.md

@@ -8,11 +8,13 @@ requires "t/unit/match-assoc-comm.k"
 requires "t/unit/subst.k"
 requires "t/unit/syntactic-match.k"
 requires "t/unit/visitor.k"
+requires "t/unit/dnf.k"
 ```
 
 ```k
 module DRIVER-UNIT-TEST
   imports TEST-CHECKSAT
+  imports TEST-DNF
   imports TEST-MATCH-ASSOC
   imports TEST-MATCH-ASSOC-COMM
   imports TEST-SUBST
@@ -27,7 +29,7 @@ module UNIT-TEST
 
   syntax Declaration ::= "suite" String
   rule <k> suite(SUITE) => next-test(SUITE, 1) ... </k>
-  
+
   syntax Declaration ::= "next-test" "(" String "," Int ")"
   rule <k> next-test(SUITE, N)
         => test(SUITE, N)