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

matching over heap variables #74

Merged
merged 12 commits into from
Jun 17, 2020
Merged

matching over heap variables #74

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
ce98bfa
matching: match over heap variable
lucaspena Jun 10, 2020
449aa2a
matching: #matchStuck is own sort now, results in stuck configuration…
lucaspena Mar 17, 2020
0425b75
matching: remove spurious side condition in matchAssocComm rule causi…
lucaspena Mar 17, 2020
65a620b
kore-lang: getSpatialPatterns and getPredicatePatterns
lucaspena Jun 3, 2020
3922c7a
matching: allow multiple heaps in terms
lucaspena Jun 3, 2020
b52dad9
matching with heap variable must be at end of pattern list
lucaspena Apr 15, 2020
75911fb
match: rotate heap variable when not at end of pattern list
lucaspena Jun 3, 2020
9f4b7bb
match: lhs can have multiple seps
lucaspena Jun 3, 2020
32177c5
matching: match on multiple heaps on RHS
lucaspena Jun 3, 2020
6557873
match-assoc-comm: H1 is a token
lucaspena Jun 3, 2020
4d2c0a4
matching: remove extraneous side condition
lucaspena Jun 10, 2020
2c3ab94
t/unit/match: fix test cases
lucaspena Jun 10, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions prover/lang/kore-lang.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -798,6 +798,19 @@ Simplifications
rule isSpatialPattern(\forall{_} implicationContext(_,_)) => false
[owise]

syntax Patterns ::= getSpatialPatterns(Patterns) [function]
rule getSpatialPatterns(.Patterns) => .Patterns
rule getSpatialPatterns(P, Ps) => P, getSpatialPatterns(Ps)
requires isSpatialPattern(P)
rule getSpatialPatterns(P, Ps) => getSpatialPatterns(Ps)
requires notBool isSpatialPattern(P)

syntax Patterns ::= getPredicatePatterns(Patterns) [function]
rule getPredicatePatterns(.Patterns) => .Patterns
rule getPredicatePatterns(P, Ps) => P, getPredicatePatterns(Ps)
requires isPredicatePattern(P)
rule getPredicatePatterns(P, Ps) => getPredicatePatterns(Ps)
requires notBool isPredicatePattern(P)
```

```k
Expand Down
130 changes: 93 additions & 37 deletions prover/strategies/matching.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,15 +36,23 @@ module MATCHING-FUNCTIONAL
rule (MR1, MR1s) ++MatchResults MR2s => MR1, (MR1s ++MatchResults MR2s)
rule .MatchResults ++MatchResults MR2s => MR2s

rule #match( terms: \and(sep(H), Hs), pattern: P, variables: Vs )
=> #match( terms: H, pattern: P, variables: Vs )
++MatchResults #match( terms: \and(Hs), pattern: P, variables: Vs )
requires Hs =/=K .Patterns

rule #match( terms: \and(sep(H), .Patterns), pattern: P, variables: Vs )
=> #match( terms: H, pattern: P, variables: Vs )

rule #match( terms: T, pattern: P, variables: Vs )
=> #filterErrors( #matchAssocComm( terms: T
, pattern: P
, variables: Vs
, results: .MatchResults
, subst: .Map
, rest: .Patterns
)
)
, pattern: P
, variables: Vs
, results: .MatchResults
, subst: .Map
, rest: .Patterns
)
)

syntax MatchResults ::= #filterErrors(MatchResults) [function]
rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs)
Expand All @@ -56,21 +64,23 @@ module MATCHING-FUNCTIONAL
Work around OCaml not producing reasonable error messages:

```k
syntax MatchResult ::= MatchStuck
syntax MatchStuck ::= "#matchStuck" "(" K ")"
syntax KItem ::= "\\n" [format(%n)]
rule #matchAssocComm(terms: T
, pattern: P
rule #matchAssocComm( terms: T
, pattern: P
, variables: Vs
, results: MRs
, subst: SUBST
, rest: REST
)
=> #error( "AC"
~> "terms:" ~> T
~> "pattern:" ~> P
~> "variables:" ~> Vs
~> "subst:" ~> SUBST
~> "rest:" ~> REST
~> "MRs:" ~> MRs )
=> #matchStuck( "AC"
~> "terms:" ~> T
~> "pattern:" ~> P
~> "variables:" ~> Vs
~> "subst:" ~> SUBST
~> "rest:" ~> REST
~> "MRs:" ~> MRs )
, .MatchResults
[owise]
```
Expand Down Expand Up @@ -184,6 +194,7 @@ Recurse over assoc-comm `sep`:
, rest: REST
)
=> #error( "Pattern larger than term" ), .MatchResults
requires notBool P in Vs

// Base case: emp matches all heaps
rule #matchAssocComm( terms: Ts
Expand All @@ -195,7 +206,7 @@ Recurse over assoc-comm `sep`:
)
=> #matchResult(subst: SUBST, rest: REST ++Patterns Ts), .MatchResults

// Base case: If matching a single term, agains an atomic pattern, use Assoc Matching
// Base case: If matching a single term against an atomic pattern, use Assoc Matching
rule #matchAssocComm( terms: T, .Patterns
, pattern: P, .Patterns
, variables: Vs
Expand All @@ -209,6 +220,7 @@ Recurse over assoc-comm `sep`:
, subst: SUBST
, rest: REST
)
requires notBool P in Vs
```

Matching an atomic pattern against multiple terms: return a disjunction of the solutions
Expand Down Expand Up @@ -236,6 +248,7 @@ Matching an atomic pattern against multiple terms: return a disjunction of the s
, rest: T, REST
)
requires Ts =/=K .Patterns
andBool notBool P in Vs
```

Matching a non-atomic pattern against multiple terms: Match the first
Expand Down Expand Up @@ -264,23 +277,59 @@ atom in the pattern against any of the terms, and then extend those solutions.
)
requires ARGs =/=K .Patterns
andBool P_ARGs =/=K .Patterns
andBool notBool P_ARG in Vs
```

Base case: If matching a single term against a heap variable, return REST
TODO: if there are multiple heap variables, we need to return all possible partitions.
Currently, the entire REST is constrained to a single heap variable
TODO: other corner cases probably

```k
rule #matchAssocComm( terms: Ts
, pattern: (H:Variable, P, Ps)
=> ((P, Ps) ++Patterns H)
, variables: Vs
, results: .MatchResults
, subst: SUBST
, rest: .Patterns
)
requires notBool isVariable(P)

rule #matchAssocComm( terms: Ts
, pattern: H:Variable, .Patterns
, variables: Vs
, results: .MatchResults
, subst: SUBST
, rest: .Patterns
)
=> #matchResult( subst: SUBST H |-> sep(Ts)
, rest: .Patterns
)
, .MatchResults
requires H in Vs
```

With each returned result, we apply the substitution and continue matching over
the unmatched part of the term:

```k
// TODO: don't want to call substUnsafe directly (obviously)
rule #matchAssocComm( terms: Ts => REST
, pattern: P => substPatternsMap(P, SUBST1)
, variables: Vs => Vs -Patterns fst(unzip(SUBST1))
, results: #matchResult(subst: SUBST1, rest: REST), .MatchResults
=> .MatchResults
, subst: SUBST2
=> (SUBST1 SUBST2)
, rest: _
rule #matchAssocComm( terms: Ts
, pattern: P
, variables: Vs
, results: #matchResult(subst: SUBST_INNER, rest: REST_INNER), .MatchResults
, subst: SUBST
, rest: REST
)
requires intersectSet(keys(SUBST1), keys(SUBST2)) ==K .Set
=> #matchAssocComm( terms: REST_INNER
, pattern: substPatternsMap(P, SUBST_INNER)
, variables: Vs -Patterns fst(unzip(SUBST_INNER))
, results: .MatchResults
, subst: SUBST_INNER SUBST
, rest: REST
)
requires intersectSet(keys(SUBST_INNER), keys(SUBST)) ==K .Set
```

Failures are propagated:
Expand Down Expand Up @@ -367,26 +416,33 @@ The `with-each-match` strategy
Instantiate existentials using matching on the spatial part of goals:

```k
rule <claim> \implies(\and(sep(LSPATIAL), LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) </claim>
rule <claim> \implies(\and(LHS) , \exists { Vs } \and(sep(RSPATIAL), RHS)) </claim>
<k> match
=> with-each-match(#match( terms: LSPATIAL
=> with-each-match(#match( terms: \and(getSpatialPatterns(LHS))
, pattern: RSPATIAL
, variables: Vs
)
, match
)
...
, match
)
...
</k>
requires isSpatialPattern(sep(LSPATIAL))
andBool isSpatialPattern(sep(RSPATIAL))
requires isSpatialPattern(sep(RSPATIAL))
andBool getFreeVariables(getSpatialPatterns(sep(RSPATIAL), RHS)) intersect Vs =/=K .Patterns
rule <claim> \implies(\and(LHS) , \exists { Vs } \and(RHS)) </claim>
<k> match => noop ... </k>
requires getFreeVariables(getSpatialPatterns(RHS)) intersect Vs ==K .Patterns
rule <claim> \implies( \and( LSPATIAL, LHS)
, \exists { Vs } \and( RHS )
=> \exists { Vs -Patterns fst(unzip(SUBST)) } substMap(\and(RHS), SUBST)
, \exists { Vs } \and(sep(RSPATIAL), RHS)
=> \exists { Vs -Patterns fst(unzip(SUBST)) }
#flattenAnd(substMap( \and(getSpatialPatterns(RHS) ++Patterns (sep(RSPATIAL), (RHS -Patterns getSpatialPatterns(RHS))))
, SUBST
)
)
)
</claim>
<k> ( #matchResult(subst: SUBST, rest: .Patterns) ~> match )
=> noop
...
=> match
...
</k>

rule <claim> \implies(LHS, \exists { Vs } \and(RSPATIAL, RHS)) </claim>
Expand Down
97 changes: 95 additions & 2 deletions prover/t/unit/match-assoc-comm.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@ module TEST-MATCH-ASSOC-COMM
| "d" [token]
syntax UpperName ::= "Data" [token]
| "Loc" [token]
| "W" [token] | "W1" [token] | "W2" [token]
| "W" [token] | "W0" [token] | "W1" [token] | "W2" [token]
| "X0" [token] | "X1" [token] | "X2" [token]
| "Y0" [token] | "Y1" [token] | "Y2" [token]
| "Z" [token] | "Z1" [token] | "Z2" [token]
| "H0" [token]
| "H0" [token] | "H1" [token]

rule test("match-assoc-comm", 1)
=> assert( #matchResult( subst: .Map , rest: pto( Z { Loc }, W { Data }))
Expand Down Expand Up @@ -133,4 +133,97 @@ module TEST-MATCH-ASSOC-COMM
)
)
.Declarations

rule test("match-assoc-comm", 9)
=> assert( #matchResult( subst: Y2 { Data } |-> Y1 { Data }
H1 { Heap } |-> sep( pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) ), H0 { Heap } )
, rest: .Patterns
)
, .MatchResults
== #filterErrors( #matchAssocComm( terms: H0 { Heap }
, pto ( X1 { Loc } , Y1 { Data } )
, pto ( X2 { Loc } , c( W1 { Loc } , Z1 { Loc }) )
, pattern: pto ( X1 { Loc } , Y2 { Data } )
, H1 { Heap }
, variables: Y2 { Data }
, H1 { Heap }
, results: .MatchResults
, subst: .Map
, rest: .Patterns
)
)
)
.Declarations

// Matching on a symbolic heap
rule test("match-assoc-comm", 10)
=> assert( #matchResult( subst: H0 { Heap } |-> sep ( pto ( X2 { Loc } , Y2 { Data } ) )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: .Patterns
)
, #matchResult( subst: H0 { Heap } |-> sep ( pto ( X1 { Loc } , Y1 { Data } ) )
W { Loc } |-> X2 { Loc }
Z { Data } |-> Y2 { Data }
, rest: .Patterns
)
// TODO: we need to be getting these results as well
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X2 { Loc } , Y2 { Data } )
// )
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X1 { Loc } , Y1 { Data } )
// )
, .MatchResults
== #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } )
, pto ( X2 { Loc } , Y2 { Data } )
, pattern: H0 { Heap }
, pto ( W { Loc } , Z { Data } )
, variables: H0 { Heap }, W { Loc }, Z { Data }
, results: .MatchResults
, subst: .Map
, rest: .Patterns
)
)
.Declarations

// Matching on a symbolic heap
rule test("match-assoc-comm", 11)
=> assert( #matchResult( subst: H0 { Heap } |-> sep ( pto ( X2 { Loc } , Y2 { Data } ) )
W { Loc } |-> X1 { Loc }
Z { Data } |-> Y1 { Data }
, rest: .Patterns
)
, #matchResult( subst: H0 { Heap } |-> sep ( pto ( X1 { Loc } , Y1 { Data } ) )
W { Loc } |-> X2 { Loc }
Z { Data } |-> Y2 { Data }
, rest: .Patterns
)
// TODO : we need to be getting these results as well
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X2 { Loc } , Y2 { Data } )
// )
// , #matchResult( subst: H0 { Heap } |-> sep ( .Patterns )
// W { Loc } |-> X1 { Loc }
// Z { Data } |-> Y1 { Data }
// , rest: pto ( X1 { Loc } , Y1 { Data } )
// )
, .MatchResults
== #matchAssocComm( terms: pto ( X1 { Loc } , Y1 { Data } )
, pto ( X2 { Loc } , Y2 { Data } )
, pattern: H0 { Heap }
, pto ( W { Loc } , Z { Data } )
, variables: H0 { Heap }, W { Loc }, Z { Data }
, results: .MatchResults
, subst: .Map
, rest: .Patterns
)
)
.Declarations
endmodule