Shape analysis#58

Draft

lucaspena wants to merge 133 commits into

masterfrom

shape-analysis

Commits on May 8, 2020

build: Generate tests for t/*.smt and t/*.kore (these are not part of the smoke tests however)
nishantjr
committed

Commits on May 9, 2020

build: Replace ls_nonrec_entail_ls_{07 => 05}.sb.smt2 and add kore smoke test
nishantjr
committed
configuration: strategies are now in the <k> cell. goals in <claim>
nishantjr
committed
build: Work around different extensions being used by kore and smt tests
nishantjr
committed
build: uncomment out kore and smt tests, add some missing expected files

lucaspena
authored and
nishantjr
committed
add footprint analysis rule. modify matching to handle heap variable

lucaspena
authored and
nishantjr
committed
move footprint analysis from unfolding to matching

lucaspena
authored and
nishantjr
committed
matching: footprint analysis uses match to find instance of pto on LHS

lucaspena
authored and
nishantjr
committed
testlists: dll-vc05: Use kt as part of the search instead of manually specifying it.
nishantjr
committed
matching: #matchStuck is own sort now, results in stuck configuration if fires

lucaspena
authored and
nishantjr
committed
matching: remove spurious side condition in matchAssocComm rule causing rule not to fire

lucaspena
authored and
nishantjr
committed
begin nullity analysis strategy

lucaspena
authored and
nishantjr
committed
Fix claim vs strategy cell issues
nishantjr
committed
add strategy to abstract away LHS spatial part

lucaspena
authored and
nishantjr
committed
simplification: simplify substitute-equals-for-equals - call subst directly instead of substPatternsMap

lucaspena
authored and
nishantjr
committed
modify nullity analysis, kt-solve-implications

lucaspena
authored and
nishantjr
committed
extra dnfPs case: and(not(and))

lucaspena
authored and
nishantjr
committed
and-split-rhs added

lucaspena
authored and
nishantjr
committed
more general kt-collapse rule subsuming ad-hoc rule

lucaspena
authored and
nishantjr
committed
wip: somewhat ad-hoc strategy for abstract nil terms

lucaspena
authored and
nishantjr
committed
kt: added fail case for kt-collapse back

lucaspena
authored and
nishantjr
committed
simplification: fix small bug in #getNewVariables

lucaspena
authored and
nishantjr
committed
kt: ktForEachLRP(.Patterns) fails instead of noop

lucaspena
authored and
nishantjr
committed
WIP: knaster-tarski: substituting keeps predicate information after kt-unfold

lucaspena
authored and
nishantjr
committed
fix claim v strategy
nishantjr
committed
kt: split kt-unfold into kt-unfold and kt-subst

lucaspena
authored and
nishantjr
committed
wip: lift-constraints has incorrect canonical form

lucaspena
authored and
nishantjr
committed
completely reimplement lift-constraints (correctly this time)

lucaspena
authored and
nishantjr
committed
alpha rename in RHS of kt-subst

lucaspena
authored and
nishantjr
committed
incomplete: resolution rule
nishantjr
committed
fix kt-collapse rule
nishantjr
committed
knaster-tarski: dont call dnfPs until kt-collapse-unsat

lucaspena
authored and
nishantjr
committed
use substitution for kt-wrap, left-unfold instead of specialized FOL/SL rules

lucaspena
authored and
nishantjr
committed
wip on kt-collapse with resolution

lucaspena
authored and
nishantjr
committed
add test for matching over symbolic heap

lucaspena
authored and
nishantjr
committed
add constructor axiom

lucaspena
authored and
nishantjr
committed
check-lhs-constraint-unsat-debug strategy

lucaspena
authored and
nishantjr
committed
wip on match-assoc-comm test of match within a conjunction of multiple seps

lucaspena
authored and
nishantjr
committed
rename instantiate-axiom to instantiate-heap-axiom

lucaspena
authored and
nishantjr
committed
pto-is-injective strategy

lucaspena
authored and
nishantjr
committed
wip on abstracting nil

lucaspena
authored and
nishantjr
committed
nil no longer parameterized symbol

lucaspena
authored and
nishantjr
committed
matching with heap variable must be at end of pattern list

lucaspena
authored and
nishantjr
committed
move spatial-patterns-match strategy

lucaspena
authored and
nishantjr
committed
footprint-analysis: symbolic heap must be at end of sep

lucaspena
authored and
nishantjr
committed
dll-vc07 goes through

lucaspena
authored and
nishantjr
committed
Fix codeblock formatting
nishantjr
committed
right-unfold-all: base case is noop, falls back on search-bound base case

lucaspena
authored and
nishantjr
committed
spatial-patterns-match: iterates on all heaps on LHS

lucaspena
authored and
nishantjr
committed
search-bound: add spatial-patterns-match before smt call

lucaspena
authored and
nishantjr
committed
dll-vc11 goes through with footprint-analysis, abstract-nil

lucaspena
authored and
nishantjr
committed
filterVariablesBySort: move to kore-lang

lucaspena
authored and
nishantjr
committed
nullity-analysis: generalize to work over all location variables

lucaspena
authored and
nishantjr
committed
kt-collapse: failing rule does not rewrite claim cell

lucaspena
authored and
nishantjr
committed
kt-collapse-unsat: heap variable added at end of sep

lucaspena
authored and
nishantjr
committed
change #hole to VariableName instead of Variable

lucaspena
authored and
nishantjr
committed
kt-collapse: use subgoal to collapse context using full power of prover

lucaspena
authored and
nishantjr
committed
match: rotate heap variable when not at end of pattern list

lucaspena
authored and
nishantjr
committed
match: lhs can have multiple seps

lucaspena
authored and
nishantjr
committed
spatial-patterns-equal: wip on multiple seps on LHS

lucaspena
authored and
nishantjr
committed
spatial-patterns-match: works with multiple seps anywhere on lhs

lucaspena
authored and
nishantjr
committed
spatial-patterns-equal: handles case of multiple seps on RHS

lucaspena
authored and
nishantjr
committed
kt-collapse: add heap variable to rule 2a on LHS

lucaspena
authored and
nishantjr
committed
matching: match on multiple heaps on RHS

lucaspena
authored and
nishantjr
committed
spatial-patterns-equal: lift-constraints after removing heaps

lucaspena
authored and
nishantjr
committed
kt-collapse-resolve: still applies with empty constraints

lucaspena
authored and
nishantjr
committed
match: terms can be and(.Patterns)

lucaspena
authored and
nishantjr
committed
frame: use spatial-patterns-match instead of subsumes-spatial

lucaspena
authored and
nishantjr
committed
abstract: more general abstraction of nil, dll-vc17 goes through

lucaspena
authored and
nishantjr
committed
kt-collapse: Remove unneeded sidecondition on Univerals
nishantjr
committed
re-parameterize nil with sort (needed for nll cases with multiple heaps)

lucaspena
authored and
nishantjr
committed
strategy for nll-vc03

lucaspena
authored and
nishantjr
committed
strategies/kt: Split kt into multiple modular strategies; fix broken kt-resolve strategy
nishantjr
committed
simplification: lift-or: handle \implies(\and(\or()...)
nishantjr
committed
simplification: instantiate-existentials: also instantiate existentials in LHS of context
nishantjr
committed
core: and-split: \and(.Patterns) => success
nishantjr
committed
search-sl: Do a check-lhs-constraint-unsat since the kt-collapse-no-match is likely lhs-unsat
nishantjr
committed
Update notes about `kt-collapse`
nishantjr
committed
abstract: additional case for #createDisequalities

lucaspena
authored and
nishantjr
committed
strategy for nll-vc04

lucaspena
authored and
nishantjr
committed
frame of #hole goes to fail

lucaspena
authored and
nishantjr
committed
strategy for nll_vc08 and nll_vc10

lucaspena
authored and
nishantjr
committed
lib/render-proof-tree
nishantjr
committed
match-debug
nishantjr
committed
matching: match: Everything matches \top
nishantjr
committed
claim v strategy
nishantjr
committed
matching: spatial-patterns-match: Fix non-termination; Use #match
nishantjr
committed
kt: Number of fixes for:
nishantjr
committed
t/SL-COMP18/bench/qf_shid_entl/tseg_join_tree_entail_tseg.sb.smt2 passing
nishantjr
committed
Remove tests without expected results
nishantjr
committed
claim v strategy
nishantjr
committed
strategy to remove constraints from lhs, lsegex4_slk-1 goes through

lucaspena
authored and
nishantjr
committed
smt-driver: nil is a constructor

lucaspena
authored and
nishantjr
committed
simplification: fix comment on remove constraints

lucaspena
authored and
nishantjr
committed
testlists: skl3-vc10 goes through

lucaspena
authored and
nishantjr
committed
ltl test: until implies eventually

lucaspena
authored and
nishantjr
committed
t/: Place LTL test in own folder
nishantjr
committed
kt: Do not normalize in KT. This happens in the search in any case
nishantjr
committed
drivers/base: Fix typo in configuration format attribute
nishantjr
committed
begin work on mu/ltl
nishantjr
committed
kore: getReturnSort: Case of \mu, \or, \and
nishantjr
committed
wip on adding support for \mu for ltl example

lucaspena
authored and
nishantjr
committed
fix spacing right-unfold-Nth

lucaspena
authored and
nishantjr
committed
fix typo

lucaspena
authored and
nishantjr
committed
more wip on until implies eventually

lucaspena
authored and
nishantjr
committed

Commits on May 10, 2020

Commits on May 11, 2020

fix preprocessing for matching, until implies eventually goes through
lucaspena
committed

Commits on May 12, 2020

wip on gfp strategy for nu, base case for ltl ind rule goes through
lucaspena
committed

Commits

Commits on May 8, 2020

Commits on May 9, 2020

Commits on May 10, 2020

Commits on May 11, 2020

Commits on May 12, 2020

Commits on May 14, 2020

Commits on May 15, 2020