From 5e2e626e7e22682fc2386783a9e6a4e55a197928 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 27 Jun 2022 19:54:09 -0500 Subject: [PATCH] New simplification rules (#2659) * make set and map items injective * notBool simplification * in_keys simplification * ==K simplification * and/or simplification * use set variables for boolean simplification * add ==Int simplification * refactor out simplification rules from java backend * disable simplification on llvm backend due to frontend bug involving coverage * fix fragile test * Update k-distribution/include/kframework/builtin/domains.md Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> * update test outputs * add tests that assert necessity of set variables * test for ==K Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> Co-authored-by: rv-jenkins --- .../include/kframework/builtin/domains.md | 59 ++++++++++++++++--- .../lookup-14-spec.k.out | 4 +- .../lookup-3-spec.k.out | 2 +- .../unification-lemmas/Makefile | 5 ++ .../unification-lemmas/test-spec.k | 12 ++++ .../unification-lemmas/test-spec.k.out | 1 + .../regression-new/unification-lemmas/test.k | 44 ++++++++++++++ .../unification-lemmas/test2-spec.k | 10 ++++ .../unification-lemmas/test2-spec.k.out | 1 + .../unification-lemmas2/Makefile | 5 ++ .../unification-lemmas2/owise-spec.k | 14 +++++ .../unification-lemmas2/owise-spec.k.out | 1 + .../unification-lemmas2/with-config.k | 39 ++++++++++++ 13 files changed, 185 insertions(+), 12 deletions(-) create mode 100644 k-distribution/tests/regression-new/unification-lemmas/Makefile create mode 100644 k-distribution/tests/regression-new/unification-lemmas/test-spec.k create mode 100644 k-distribution/tests/regression-new/unification-lemmas/test-spec.k.out create mode 100644 k-distribution/tests/regression-new/unification-lemmas/test.k create mode 100644 k-distribution/tests/regression-new/unification-lemmas/test2-spec.k create mode 100644 k-distribution/tests/regression-new/unification-lemmas/test2-spec.k.out create mode 100644 k-distribution/tests/regression-new/unification-lemmas2/Makefile create mode 100644 k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k create mode 100644 k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k.out create mode 100644 k-distribution/tests/regression-new/unification-lemmas2/with-config.k diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index de51db23c6f..df9260f713a 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -254,7 +254,7 @@ An element of a `Map` is constructed via the `|->` operator. The key is on the left and the value is on the right. ```k - syntax Map ::= KItem "|->" KItem [function, functional, hook(MAP.element), klabel(_|->_), symbol, latex({#1}\mapsto{#2})] + syntax Map ::= KItem "|->" KItem [function, functional, hook(MAP.element), klabel(_|->_), symbol, latex({#1}\mapsto{#2}), injective] syntax priorities _|->_ > _Map_ .Map syntax non-assoc _|->_ @@ -440,6 +440,11 @@ module MAP-KORE-SYMBOLIC [kore,symbolic] rule K1 in_keys(M [ K2 <- _ ]) => true requires K1 ==K K2 orBool K1 in_keys(M) [simplification] rule K1 in_keys(M [ K2 <- _ ]) => K1 in_keys(M) requires K1 =/=K K2 [simplification] + rule {false #Equals @Key in_keys(.Map)} => #Ceil(@Key) [simplification] + rule {@Key in_keys(.Map) #Equals false} => #Ceil(@Key) [simplification] + rule {false #Equals @Key in_keys(Key' |-> Val @M)} => #Ceil(@Key) #And #Ceil(Key' |-> Val @M) #And #Not({@Key #Equals Key'}) #And {false #Equals @Key in_keys(@M)} [simplification] + rule {@Key in_keys(Key' |-> Val @M) #Equals false} => #Ceil(@Key) #And #Ceil(Key' |-> Val @M) #And #Not({@Key #Equals Key'}) #And {@Key in_keys(@M) #Equals false} [simplification] + /* // The rule below is automatically generated by the frontend for every sort // hooked to MAP.Map. It is left here to serve as documentation. @@ -533,7 +538,7 @@ The set with zero elements is represented by `.Set`. An element of a `Set` is constructed via the `SetItem` operator. ```k - syntax Set ::= SetItem(KItem) [function, functional, hook(SET.element), klabel(SetItem), symbol] + syntax Set ::= SetItem(KItem) [function, functional, hook(SET.element), klabel(SetItem), symbol, injective] ``` ### Set union @@ -785,7 +790,7 @@ module BOOL-SYNTAX syntax Bool ::= "false" [token] endmodule -module BOOL +module BOOL-COMMON imports private BASIC-K imports BOOL-SYNTAX ``` @@ -860,6 +865,25 @@ operations listed above. rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2) endmodule + +module BOOL-KORE [kore, symbolic] + imports BOOL-COMMON + + rule {true #Equals notBool @B} => {false #Equals @B} [simplification] + rule {notBool @B #Equals true} => {@B #Equals false} [simplification] + rule {false #Equals notBool @B} => {true #Equals @B} [simplification] + rule {notBool @B #Equals false} => {@B #Equals true} [simplification] + + rule {true #Equals @B1 andBool @B2} => {true #Equals @B1} #And {true #Equals @B2} [simplification] + rule {@B1 andBool @B2 #Equals true} => {@B1 #Equals true} #And {@B2 #Equals true} [simplification] + rule {false #Equals @B1 orBool @B2} => {false #Equals @B1} #And {false #Equals @B2} [simplification] + rule {@B1 orBool @B2 #Equals false} => {@B1 #Equals false} #And {@B2 #Equals false} [simplification] +endmodule + +module BOOL + imports BOOL-COMMON + imports BOOL-KORE +endmodule ``` Integers @@ -1089,11 +1113,20 @@ module INT-KAST [kast] endmodule -module INT-KORE [kore] +module INT-KORE [kore, symbolic] imports private K-EQUAL + imports private BOOL imports INT-COMMON - rule I1:Int ==K I2:Int => I1 ==Int I2 + rule I1:Int ==K I2:Int => I1 ==Int I2 [simplification] + rule {K1 ==Int K2 #Equals true} => {K1 #Equals K2} [simplification] + rule {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification] + rule {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification] + rule {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification] + rule {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification] + rule {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification] + rule {K1 =/=Int K2 #Equals false} => {K1 #Equals K2} [simplification] + rule {false #Equals K1 =/=Int K2} => {K1 #Equals K2} [simplification] endmodule @@ -1592,11 +1625,11 @@ module STRING-KAST [kast] endmodule -module STRING-KORE [kore] +module STRING-KORE [kore, symbolic] imports private K-EQUAL imports STRING-COMMON - rule S1:String ==K S2:String => S1 ==String S2 + rule S1:String ==K S2:String => S1 ==String S2 [simplification] endmodule @@ -2060,11 +2093,19 @@ module K-EQUAL-SYNTAX endmodule -module K-EQUAL-KORE [kore] +module K-EQUAL-KORE [kore, symbolic] import private BOOL import K-EQUAL-SYNTAX - rule K1:Bool ==K K2:Bool => K1 ==Bool K2 + rule K1:Bool ==K K2:Bool => K1 ==Bool K2 [simplification] + rule {K1 ==K K2 #Equals true} => {K1 #Equals K2} [simplification] + rule {true #Equals K1 ==K K2} => {K1 #Equals K2} [simplification] + rule {K1 ==K K2 #Equals false} => #Not({K1 #Equals K2}) [simplification] + rule {false #Equals K1 ==K K2} => #Not({K1 #Equals K2}) [simplification] + rule {K1 =/=K K2 #Equals true} => #Not({K1 #Equals K2}) [simplification] + rule {true #Equals K1 =/=K K2} => #Not({K1 #Equals K2}) [simplification] + rule {K1 =/=K K2 #Equals false} => {K1 #Equals K2} [simplification] + rule {false #Equals K1 =/=K K2} => {K1 #Equals K2} [simplification] endmodule diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-14-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-14-spec.k.out index eed195f4d29..2c4d6772026 100644 --- a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-14-spec.k.out +++ b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-14-spec.k.out @@ -23,8 +23,8 @@ { true #Equals - Z:MyId in_keys ( MAP - ( X:MyId |-> 1 ) ) + Z:MyId in_keys ( ( MAP + X:MyId |-> 1 ) [ Y:MyId <- 2 ] ) } #And { diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-3-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-3-spec.k.out index e4a63b52814..2f7ede0b796 100644 --- a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-3-spec.k.out +++ b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/lookup-3-spec.k.out @@ -18,7 +18,7 @@ true #Equals Z:MyId in_keys ( MAP - ( Y:MyId |-> 1 ) ) + ( Y:MyId |-> 2 ) ) } #And { diff --git a/k-distribution/tests/regression-new/unification-lemmas/Makefile b/k-distribution/tests/regression-new/unification-lemmas/Makefile new file mode 100644 index 00000000000..ebe62f53831 --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas/Makefile @@ -0,0 +1,5 @@ +DEF=test +TESTDIR=. +KOMPILE_BACKEND=haskell + +include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/unification-lemmas/test-spec.k b/k-distribution/tests/regression-new/unification-lemmas/test-spec.k new file mode 100644 index 00000000000..3a8d28fbd2a --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas/test-spec.k @@ -0,0 +1,12 @@ +// Copyright (c) 2022 K Team. All Rights Reserved. + +requires "test.k" + +module TEST-SPEC + imports TEST + + claim makeLookup(B) => 1 ... + requires lookup(#hashedLocation(B .IntList)) ==Int 1 + andBool #rangeUInt(B) + +endmodule diff --git a/k-distribution/tests/regression-new/unification-lemmas/test-spec.k.out b/k-distribution/tests/regression-new/unification-lemmas/test-spec.k.out new file mode 100644 index 00000000000..17a1d4510e5 --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas/test-spec.k.out @@ -0,0 +1 @@ +#Top diff --git a/k-distribution/tests/regression-new/unification-lemmas/test.k b/k-distribution/tests/regression-new/unification-lemmas/test.k new file mode 100644 index 00000000000..5d0d88d409d --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas/test.k @@ -0,0 +1,44 @@ +// Copyright (c) 2020 K Team. All Rights Reserved. + +module TEST-SYNTAX +endmodule + +module TEST + imports TEST-SYNTAX + imports BOOL + imports INT + imports MAP + imports STRING + imports MAP-SYMBOLIC + + configuration $PGM:KItem + + syntax KItem ::= makeLookup(Int) + rule makeLookup(B) => lookup(#hash(B)) + + syntax Int ::= lookup(Hash) [function, no-evaluators] + | #lookupMemory ( Map , Int ) [function, functional, smtlib(lookupMemory)] + syntax Int ::= "pow256" [alias] /* 2 ^Int 256 */ + rule pow256 => 115792089237316195423570985008687907853269984665640564039457584007913129639936 + + syntax KItem ::= runLemma(Int) | doneLemma(Int) + rule runLemma(T) => doneLemma(T) + + // ------------------------------------------- + syntax IntList ::= List{Int, ""} + + syntax Bool ::= #rangeUInt(Int) [function, no-evaluators] + + syntax Hash ::= #hash(Int) + | #hashedLocation( IntList ) [function] + + rule #hashedLocation( .IntList) => #hash(0) + rule #hashedLocation(OFFSET .IntList) => #hash(OFFSET) + requires #rangeUInt(OFFSET) + + rule [#lookupMemory.some]: #lookupMemory( (KEY |-> VAL:Int) _M, KEY ) => VAL modInt 256 + rule [#lookupMemory.none]: #lookupMemory( M, KEY ) => 0 requires notBool KEY in_keys(M) + //Impossible case, for completeness + rule [#lookupMemory.notInt]: #lookupMemory( (KEY |-> VAL ) _M, KEY ) => 0 requires notBool isInt(VAL) + +endmodule diff --git a/k-distribution/tests/regression-new/unification-lemmas/test2-spec.k b/k-distribution/tests/regression-new/unification-lemmas/test2-spec.k new file mode 100644 index 00000000000..05e07464e6f --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas/test2-spec.k @@ -0,0 +1,10 @@ +// Copyright (c) 2022 K Team. All Rights Reserved. + +requires "test.k" + +module TEST2-SPEC + imports TEST + + claim runLemma ( #lookupMemory(( KEY |-> 33) (_KEY' |-> 728) (_KEY'' |-> (pow256 +Int 5)) (_KEY''' |-> "hello"), KEY) ) => doneLemma ( 33 ) ... + +endmodule diff --git a/k-distribution/tests/regression-new/unification-lemmas/test2-spec.k.out b/k-distribution/tests/regression-new/unification-lemmas/test2-spec.k.out new file mode 100644 index 00000000000..17a1d4510e5 --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas/test2-spec.k.out @@ -0,0 +1 @@ +#Top diff --git a/k-distribution/tests/regression-new/unification-lemmas2/Makefile b/k-distribution/tests/regression-new/unification-lemmas2/Makefile new file mode 100644 index 00000000000..461d69a5868 --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas2/Makefile @@ -0,0 +1,5 @@ +DEF=with-config +TESTDIR=. +KOMPILE_BACKEND=haskell + +include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k b/k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k new file mode 100644 index 00000000000..215c5c04277 --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k @@ -0,0 +1,14 @@ +requires "with-config.k" + +module OWISE-SPEC + imports WITH-CONFIG + + claim a(AID) => 0 + + + BID + 30 + + + requires AID =/=K BID +endmodule diff --git a/k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k.out b/k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k.out new file mode 100644 index 00000000000..17a1d4510e5 --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas2/owise-spec.k.out @@ -0,0 +1 @@ +#Top diff --git a/k-distribution/tests/regression-new/unification-lemmas2/with-config.k b/k-distribution/tests/regression-new/unification-lemmas2/with-config.k new file mode 100644 index 00000000000..5c2e85715c9 --- /dev/null +++ b/k-distribution/tests/regression-new/unification-lemmas2/with-config.k @@ -0,0 +1,39 @@ +module WITH-CONFIG + imports INT + imports COLLECTIONS + imports K-EQUAL + + configuration + + $PGM:KItem + + + .AccountId:AccountId + 0 + + + + + syntax KItem ::= Int + + syntax AccountId ::= ".AccountId" | Int + // --------------------------------------- + + syntax Int ::= "total_balance" "(" AccountId ")" [function, functional] + // ----------------------------------------------------------------------- + rule total_balance(WHO) => 0 [owise] + rule [[ total_balance(WHO) => FREE_BALANCE ]] + + WHO + FREE_BALANCE + + + // for one-spec + syntax KItem ::= "aa" "(" AccountId ")" + rule aa(AID) => total_balance(AID) + + // for owise-spec + syntax KItem ::= "a" "(" AccountId ")" + rule a(AID) => total_balance(AID) + +endmodule