Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Shape analysis #58

Draft
wants to merge 133 commits into
base: master
Choose a base branch
from
Draft

Shape analysis #58

wants to merge 133 commits into from

Conversation

lucaspena
Copy link
Contributor

OOPSLA (new kt-collapse rule, shape analysis rules, abstracting nil, etc.)

@xc93
Copy link
Collaborator

xc93 commented Apr 16, 2020

What's the plan for this PR? It looks too big to be merged given its current status.

@nishantjr
Copy link
Member

Yes, we're putting it here so that the CI runs the tests. We're going to break this apart into multiple PRs later (the subst PR is one of them)

@lucaspena lucaspena force-pushed the shape-analysis branch 3 times, most recently from 98e7f3b to b8bc773 Compare April 23, 2020 21:29
@nishantjr
build: Replace ls_nonrec_entail_ls_{07 => 05}.sb.smt2 and add kore sm…
0ba6ffa 
…oke test
@nishantjr
configuration: strategies are now in the <k> cell. goals in <claim>
7cbf5f9 
This fixes issues in the various drivers. This logically makes more sense
since it is the strategy cell that controls the execution.
nishantjr and others added 19 commits May 9, 2020 11:42
@nishantjr
build: Work around different extensions being used by kore and smt tests
d1a7233
@lucaspena @nishantjr
build: uncomment out kore and smt tests, add some missing expected files
28fcf3d
@lucaspena @nishantjr
add footprint analysis rule. modify matching to handle heap variable
69979e4
@lucaspena @nishantjr
move footprint analysis from unfolding to matching
6db13f4
@lucaspena @nishantjr
matching: footprint analysis uses match to find instance of pto on LHS
ff505cb
@nishantjr
testlists: dll-vc05: Use kt as part of the search instead of manually…
98e3e03 
… specifying it.
@lucaspena @nishantjr
matching: #matchStuck is own sort now, results in stuck configuration…
004cdcb 
… if fires
@lucaspena @nishantjr
matching: remove spurious side condition in matchAssocComm rule causi…
7047989 
…ng rule not to fire
@lucaspena @nishantjr
begin nullity analysis strategy
3fadad9
@nishantjr
Fix claim vs strategy cell issues
86f67d5
@lucaspena @nishantjr
add strategy to abstract away LHS spatial part
3eaf17a
@lucaspena @nishantjr
simplification: simplify substitute-equals-for-equals - call subst di…
74d2276 
…rectly instead of substPatternsMap
@lucaspena @nishantjr
modify nullity analysis, kt-solve-implications
3d92359
@lucaspena @nishantjr
extra dnfPs case: and(not(and))
d1272d5
@lucaspena @nishantjr
and-split-rhs added
504a007
@lucaspena @nishantjr
more general kt-collapse rule subsuming ad-hoc rule
411ab33
@lucaspena @nishantjr
wip: somewhat ad-hoc strategy for abstract nil terms
cbf688f
@lucaspena @nishantjr
kt: added fail case for kt-collapse back
be3faf6
@lucaspena @nishantjr
simplification: fix small bug in #getNewVariables
14c2357
nishantjr and others added 12 commits May 10, 2020 13:53
@nishantjr
driver/base: configuration: Claim cell is \bottom rather than top ini…
85bc0db 
…tially to avoid confusion
@nishantjr
drivers/smt-driver: Rename #rest => #mutualRecUnfold to avoid amb…
6691808 
…iguity
@nishantjr
lang/kore: Reimplement #dnf
2b76620
@nishantjr
t/unit/match-assoc: Fix missing { Data }
0b37030
@nishantjr
matching: #match: Fix missing side condition
7c9b6d4
@nishantjr
!!! t/unit/match-assoc-comm: Regression test for match failing when i…
1894ca5 
…t shouldn't be
@nishantjr
kore-helpers :#liftOr: combine multiple bases cases by using isDnfAtom
39e7a6b
@nishantjr
t/unit/match-assoc-comm: Test should be calling #match, not #matchAss…
8352db3 
…ocComm
@lucaspena
matching over mu
106ca3e
@lucaspena
fix bugs in dnf, wip on until implies eventually
b2dda5f
@lucaspena
fix preprocessing for matching, until implies eventually goes through
c866c11
@lucaspena
wip on gfp strategy for nu, base case for ltl ind rule goes through
f58cc74
nishantjr and others added 16 commits May 14, 2020 11:03
@nishantjr
kore: Extend subst and getFreeVariables to \nu
24f1fcf
@nishantjr
kore: #nnf handles \exists { .Patterns }
d3eeec8
@nishantjr
strategies/core: rhs-top: Add failure case
cfb9c33
@nishantjr
strategy: constradiction: Look for a contradiction between the first …
f503385 
…clause and any other clause
@nishantjr
matching: #matchAssoc: Syntactically match on \not
22631ad
@nishantjr
matching: Use #nnf to allow handeling more cases such as \implies
94da501
@nishantjr
matching: #matchAssoc: Patterns may use set variables too
150e5a9
@nishantjr
t/ltl/always-propagates.kore
286e3ca
@lucaspena
fix bugs in dnf, remove need for liftconstraints
9a34a4a
@nishantjr
Update README
01904b6
@lucaspena
nu is not a predicate pattern
6f47f37
@lucaspena
fix match case with error, ind goes through again
5298d3f
@lucaspena @nishantjr
render-proof-tree env specifies python3
702d741
@lucaspena @nishantjr
render-proof-tree: goals no longer have active cell, first goal is ac…
34c4a6d 
…tive
@lucaspena @nishantjr
kt-collapse: fix bug where substitution in match case is not applied …
74f6a1c 
…fully
@nishantjr
build: Uniform extensions for all tests
0befca9
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@lucaspena @xc93 @nishantjr