Skip to content

Commit 8cf981d

Browse files
ttuegelMirceaS
ttuegel
and
MirceaS
authored
Validate functions (#2585)
* Replay "Validate function definitions (#2168)" This reverts commit 8782a70. * Trim source paths from regression tests * Replay "Issue 2100 follow up (#2574)" This reverts commit 97494af. * Added another case for \or patterns Co-authored-by: Octavian Mircea Sebe <[email protected]>
1 parent 0362cce commit 8cf981d

36 files changed

+2225
-1497
lines changed

‎Dockerfile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ RUN curl -sSL https://github.com/github/hub/releases/download/v$HUB/hub-linux
2020
&& rm -fr hub-linux-amd64-$HUB
2121

2222
ENV LC_ALL=C.UTF-8
23+
ADD ./src/main/kore/prelude.kore /usr/include/kframework/kore/prelude.kore
2324

2425
ARG USER_ID=1000
2526
ARG GROUP_ID=1000

‎kore/kore.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -288,6 +288,7 @@ library
288288
Kore.Equation.Registry
289289
Kore.Equation.Sentence
290290
Kore.Equation.Simplification
291+
Kore.Equation.Validate
291292
Kore.Error
292293
Kore.Exec
293294
Kore.IndexedModule.Error

‎kore/src/Kore/ASTVerifier/SentenceVerifier.hs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,10 +68,11 @@ import qualified Kore.Attribute.Sort.HasDomainValues as Attribute.HasDomainValue
6868
import qualified Kore.Attribute.Symbol as Attribute
6969
import qualified Kore.Attribute.Symbol as Attribute.Symbol
7070
import qualified Kore.Builtin as Builtin
71+
import Kore.Equation.Validate
7172
import Kore.Error
7273
import Kore.IndexedModule.IndexedModule
7374
import Kore.IndexedModule.Resolvers as Resolvers
74-
import qualified Kore.Internal.Symbol as Internal.Symbol
75+
import qualified Kore.Internal.Symbol as Symbol
7576
import Kore.Internal.TermLike.TermLike (
7677
freeVariables,
7778
)
@@ -356,6 +357,7 @@ verifyAxiomSentence sentence =
356357
verifiedModule'
357358
(freeVariables sentence)
358359
(sentenceAxiomAttributes sentence)
360+
validateAxiom attrs verified
359361
State.modify $ addAxiom verified attrs
360362
where
361363
addAxiom verified attrs =
@@ -483,7 +485,7 @@ parseAndVerifyAxiomAttributes ::
483485
IndexedModule Verified.Pattern Attribute.Symbol attrs ->
484486
FreeVariables VariableName ->
485487
Attributes ->
486-
error (Attribute.Axiom Internal.Symbol.Symbol VariableName)
488+
error (Attribute.Axiom Symbol.Symbol VariableName)
487489
parseAndVerifyAxiomAttributes indexModule freeVars attrs =
488490
parseAxiomAttributes' attrs >>= verifyAxiomAttributes indexModule
489491
where

‎kore/src/Kore/Equation/Registry.hs

Lines changed: 1 addition & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,6 @@ import Kore.Attribute.Axiom (
2727
)
2828
import qualified Kore.Attribute.Axiom as Attribute
2929
import Kore.Attribute.Overload
30-
import qualified Kore.Attribute.Pattern as Pattern
3130
import Kore.Attribute.Symbol (
3231
StepperAttributes,
3332
)
@@ -50,7 +49,6 @@ import Kore.Syntax.Sentence (
5049
)
5150
import qualified Kore.Verified as Verified
5251
import Prelude.Kore
53-
import qualified Pretty
5452

5553
-- | Create a mapping from symbol identifiers to their defining axioms.
5654
extractEquations ::
@@ -112,11 +110,10 @@ partitionEquations equations =
112110
equations' =
113111
equations
114112
& filter (not . ignoreEquation)
115-
(simplificationRules, unProcessedFunctionRules) =
113+
(simplificationRules, functionRules) =
116114
partition Equation.isSimplificationRule
117115
. sortOn Equation.equationPriority
118116
$ equations'
119-
functionRules = filter (not . ignoreDefinition) unProcessedFunctionRules
120117

121118
{- | Should we ignore the 'EqualityRule' for evaluation or simplification?
122119
@@ -140,17 +137,3 @@ ignoreEquation Equation{attributes}
140137
Unit{isUnit} = Attribute.unit attributes
141138
Idem{isIdem} = Attribute.idem attributes
142139
Overload{getOverload} = Attribute.overload attributes
143-
144-
-- | Should we ignore the 'EqualityRule' for evaluating function definitions?
145-
ignoreDefinition :: Equation RewritingVariableName -> Bool
146-
ignoreDefinition Equation{attributes, left}
147-
| isLeftFunctionLike = False
148-
| otherwise =
149-
(error . show . Pretty.vsep)
150-
[ "left-hand side of equation was not function-like at:"
151-
, Pretty.indent 4 $ Pretty.pretty sourceLocation
152-
]
153-
where
154-
Attribute.Axiom{sourceLocation} = attributes
155-
isLeftFunctionLike =
156-
(Pattern.isFunction . Pattern.function) (extractAttributes left)

‎kore/src/Kore/Equation/Sentence.hs

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,8 +38,12 @@ import qualified Kore.Internal.TermLike as TermLike
3838
import Kore.Syntax.Sentence (
3939
SentenceAxiom (..),
4040
)
41+
import Kore.Unparser (
42+
unparse,
43+
)
4144
import qualified Kore.Verified as Verified
4245
import Prelude.Kore
46+
import Pretty
4347

4448
fromSentenceAxiom ::
4549
(Attribute.Axiom Symbol VariableName, Verified.SentenceAxiom) ->
@@ -60,6 +64,40 @@ data MatchEquationError variable
6064
deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
6165
deriving anyclass (Debug)
6266

67+
instance InternalVariable variable => Pretty (MatchEquationError variable) where
68+
pretty (NotEquation term) =
69+
Pretty.vsep
70+
[ "The given term is not an equation:"
71+
, unparse term
72+
]
73+
pretty (RequiresError notPred) =
74+
Pretty.vsep
75+
[ "The equation's requires clause is not a predicate:"
76+
, pretty notPred
77+
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
78+
]
79+
pretty (ArgumentError notPred) =
80+
Pretty.vsep
81+
[ "The equation's argument clause is not a predicate:"
82+
, pretty notPred
83+
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
84+
]
85+
pretty (AntiLeftError notPred) =
86+
Pretty.vsep
87+
[ "The equation's anti-left clause is not a predicate:"
88+
, pretty notPred
89+
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
90+
]
91+
pretty (EnsuresError notPred) =
92+
Pretty.vsep
93+
[ "The equation's ensures clause is not a predicate:"
94+
, pretty notPred
95+
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
96+
]
97+
pretty FunctionalAxiom = "The term is a functional axiom."
98+
pretty ConstructorAxiom = "The term is a constructor axiom."
99+
pretty SubsortAxiom = "The term is a subsort axiom."
100+
63101
matchEquation ::
64102
forall variable.
65103
InternalVariable variable =>

‎kore/src/Kore/Equation/Validate.hs

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2021
3+
License : NCSA
4+
-}
5+
module Kore.Equation.Validate (
6+
validateAxiom,
7+
) where
8+
9+
import Control.Monad.State.Strict (
10+
StateT,
11+
)
12+
import qualified Data.Functor.Foldable as Recursive
13+
import Data.Text (
14+
pack,
15+
)
16+
import Kore.AST.Error
17+
import Kore.ASTVerifier.Verifier
18+
import Kore.Attribute.Axiom (
19+
Assoc (..),
20+
Comm (..),
21+
Idem (..),
22+
Overload (..),
23+
Unit (..),
24+
)
25+
import qualified Kore.Attribute.Axiom as Attribute (
26+
Axiom (..),
27+
)
28+
import qualified Kore.Builtin.List.List as List
29+
import qualified Kore.Builtin.Map.Map as Map
30+
import qualified Kore.Builtin.Set.Set as Set
31+
import Kore.Equation.Equation (
32+
Equation (..),
33+
isSimplificationRule,
34+
)
35+
import Kore.Equation.Sentence (
36+
MatchEquationError (..),
37+
fromSentenceAxiom,
38+
)
39+
import Kore.Internal.Predicate (
40+
pattern PredicateCeil,
41+
pattern PredicateIn,
42+
)
43+
import qualified Kore.Internal.Predicate as Predicate
44+
import qualified Kore.Internal.Symbol as Symbol
45+
import qualified Kore.Internal.TermLike as TermLike
46+
import Kore.Syntax.Definition
47+
import Kore.Syntax.Variable
48+
import Kore.Unparser (
49+
unparse,
50+
)
51+
import qualified Kore.Verified as Verified
52+
import Prelude.Kore
53+
import qualified Pretty
54+
55+
validateAxiom ::
56+
Attribute.Axiom TermLike.Symbol VariableName ->
57+
Verified.SentenceAxiom ->
58+
StateT VerifiedModule' Verifier ()
59+
validateAxiom attrs verified =
60+
case fromSentenceAxiom (attrs, verified) of
61+
Right eq@Equation{left, argument} ->
62+
when (needsVerification eq) $
63+
checkLHS eq left >> checkArg eq argument
64+
Left err@(RequiresError _) -> failWithBadEquation err
65+
Left err@(ArgumentError _) -> failWithBadEquation err
66+
Left err@(AntiLeftError _) -> failWithBadEquation err
67+
Left err@(EnsuresError _) -> failWithBadEquation err
68+
Left (NotEquation _) -> return ()
69+
Left FunctionalAxiom -> return ()
70+
Left ConstructorAxiom -> return ()
71+
Left SubsortAxiom -> return ()
72+
where
73+
failWithBadEquation =
74+
koreFailWithLocations [sentenceAxiomPattern verified]
75+
. pack
76+
. show
77+
. Pretty.pretty
78+
79+
needsVerification eq@Equation{attributes} =
80+
not
81+
( isSimplificationRule eq
82+
|| isAssoc
83+
|| isComm
84+
|| isUnit
85+
|| isIdem
86+
|| isJust getOverload
87+
)
88+
where
89+
Assoc{isAssoc} = Attribute.assoc attributes
90+
Comm{isComm} = Attribute.comm attributes
91+
Unit{isUnit} = Attribute.unit attributes
92+
Idem{isIdem} = Attribute.idem attributes
93+
Overload{getOverload} = Attribute.overload attributes
94+
95+
checkLHS eq termLike = do
96+
checkAllowedFunctionSymbol
97+
checkVarFunctionArguments
98+
where
99+
_ :< termLikeF = Recursive.project termLike
100+
101+
checkAllowedFunctionSymbol
102+
| TermLike.App_ sym _ <- termLike =
103+
unless
104+
(isAllowedFunctionSymbol sym)
105+
(throwIllegalFunctionSymbol sym)
106+
| otherwise = return ()
107+
where
108+
isAllowedFunctionSymbol sym =
109+
Symbol.isFunction sym && not (Symbol.isConstructorLike sym)
110+
111+
throwIllegalFunctionSymbol sym =
112+
koreFailWithLocations [eq] $
113+
pack $
114+
show $
115+
Pretty.vsep
116+
[ "Expected function symbol, but found constructor symbol:"
117+
, unparse sym
118+
]
119+
120+
checkVarFunctionArguments =
121+
failOnJust
122+
eq
123+
"Expected variable, but found:"
124+
$ asum $ getNotVar <$> termLikeF
125+
126+
getNotVar (TermLike.Var_ _) = Nothing
127+
getNotVar term = Just term
128+
129+
checkArg _ Nothing = return ()
130+
checkArg eq (Just arg) =
131+
traverse_
132+
( failOnJust eq "Found invalid subterm in argument of function equation:"
133+
. checkArgIn
134+
)
135+
$ Predicate.getMultiAndPredicate arg
136+
where
137+
checkArgIn (PredicateIn (TermLike.Var_ _) term) =
138+
findBadArgSubterm term
139+
checkArgIn (PredicateCeil (TermLike.And_ _ (TermLike.Var_ _) term)) =
140+
findBadArgSubterm term
141+
checkArgIn badArg = Just $ Predicate.fromPredicate_ badArg
142+
143+
findBadArgSubterm term = case term of
144+
_
145+
| TermLike.isConstructorLike term -> descend
146+
TermLike.App_ sym _
147+
| isGoodSymbol sym -> descend
148+
| otherwise -> Just term
149+
TermLike.InternalBytes_ _ _ -> Nothing
150+
TermLike.InternalBool_ _ -> Nothing
151+
TermLike.InternalInt_ _ -> Nothing
152+
TermLike.InternalString_ _ -> Nothing
153+
TermLike.DV_ _ (TermLike.StringLiteral_ _) -> Nothing
154+
TermLike.And_ _ _ _ -> descend
155+
TermLike.Or_ _ _ _ -> descend
156+
TermLike.Var_ _ -> Nothing
157+
TermLike.Inj_ _ -> descend
158+
_ -> Just term
159+
where
160+
_ :< termF = Recursive.project term
161+
isGoodSymbol sym =
162+
or
163+
[ Symbol.isConstructorLike sym
164+
, Symbol.isAnywhere sym && Symbol.isInjective sym
165+
, Map.isSymbolConcat sym
166+
, Map.isSymbolElement sym
167+
, Map.isSymbolUnit sym
168+
, Set.isSymbolConcat sym
169+
, Set.isSymbolElement sym
170+
, Set.isSymbolUnit sym
171+
, List.isSymbolConcat sym
172+
, List.isSymbolElement sym
173+
, List.isSymbolUnit sym
174+
]
175+
descend = asum $ findBadArgSubterm <$> termF
176+
177+
failOnJust _ _ Nothing = return ()
178+
failOnJust eq errorMessage (Just term) =
179+
koreFailWithLocations
180+
[term]
181+
( pack $
182+
show $
183+
Pretty.vsep
184+
[ errorMessage
185+
, Pretty.indent 4 $ unparse term
186+
, "The equation that the above occurs in is:"
187+
, Pretty.indent 4 $ Pretty.pretty eq
188+
]
189+
)

‎kore/src/Kore/Internal/Predicate.hs

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1105,12 +1105,6 @@ hasFreeVariable ::
11051105
Bool
11061106
hasFreeVariable variableName = isFreeVariable variableName . freeVariables
11071107

1108-
{- | Traverse the predicate from the top down and apply substitutions.
1109-
1110-
The 'freeVariables' annotation is used to avoid traversing subterms that
1111-
contain none of the targeted variables.
1112-
-}
1113-
11141108
-- !! TODO The following is just a temporary solution and !!
11151109
-- !! the code using wrapPredicate should be refactored !!
11161110

@@ -1124,6 +1118,11 @@ wrapPredicate =
11241118
id
11251119
. makePredicate
11261120

1121+
{- | Traverse the predicate from the top down and apply substitutions.
1122+
1123+
The 'freeVariables' annotation is used to avoid traversing subterms that
1124+
contain none of the targeted variables.
1125+
-}
11271126
substitute ::
11281127
InternalVariable variable =>
11291128
Map (SomeVariableName variable) (TermLike variable) ->

‎kore/src/Kore/Internal/Symbol.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ module Kore.Internal.Symbol (
1414
isTotal,
1515
isInjective,
1616
isMemo,
17+
isAnywhere,
1718
noEvaluators,
1819
symbolHook,
1920
constructor,
@@ -170,6 +171,9 @@ isTotal = Attribute.isTotal . symbolAttributes
170171
isMemo :: Symbol -> Bool
171172
isMemo = Attribute.isMemo . Attribute.memo . symbolAttributes
172173

174+
isAnywhere :: Symbol -> Bool
175+
isAnywhere = Attribute.isAnywhere . Attribute.anywhere . symbolAttributes
176+
173177
noEvaluators :: Symbol -> Bool
174178
noEvaluators =
175179
Attribute.hasNoEvaluators . Attribute.noEvaluators . symbolAttributes

0 commit comments

Comments
 (0)