|
| 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 | + ) |
0 commit comments