runtimeverification · MirceaS · Sep 24, 2020 · Sep 28, 2020 · Sep 28, 2020 · Sep 29, 2020
diff --git a/Dockerfile b/Dockerfile
@@ -20,6 +20,7 @@ RUN    curl -sSL https://github.com/github/hub/releases/download/v$HUB/hub-linux
     && rm -fr hub-linux-amd64-$HUB
 
 ENV LC_ALL=C.UTF-8
+ADD ./src/main/kore/prelude.kore /usr/include/kframework/kore/prelude.kore
 
 ARG USER_ID=1000
 ARG GROUP_ID=1000

diff --git a/kore/kore.cabal b/kore/kore.cabal
@@ -289,6 +289,7 @@ library
     Kore.Equation.Registry
     Kore.Equation.Sentence
     Kore.Equation.Simplification
+    Kore.Equation.Validate
     Kore.Error
     Kore.Exec
     Kore.IndexedModule.Error

diff --git a/kore/src/Kore/ASTVerifier/SentenceVerifier.hs b/kore/src/Kore/ASTVerifier/SentenceVerifier.hs
@@ -68,10 +68,11 @@ import qualified Kore.Attribute.Sort.HasDomainValues as Attribute.HasDomainValue
 import qualified Kore.Attribute.Symbol as Attribute
 import qualified Kore.Attribute.Symbol as Attribute.Symbol
 import qualified Kore.Builtin as Builtin
+import Kore.Equation.Validate
 import Kore.Error
 import Kore.IndexedModule.IndexedModule
 import Kore.IndexedModule.Resolvers as Resolvers
-import qualified Kore.Internal.Symbol as Internal.Symbol
+import qualified Kore.Internal.Symbol as Symbol
 import Kore.Internal.TermLike.TermLike (
     freeVariables,
  )
@@ -356,6 +357,7 @@ verifyAxiomSentence sentence =
                 verifiedModule'
                 (freeVariables sentence)
                 (sentenceAxiomAttributes sentence)
+        validateAxiom attrs verified
         State.modify $ addAxiom verified attrs
   where
     addAxiom verified attrs =
@@ -483,7 +485,7 @@ parseAndVerifyAxiomAttributes ::
     IndexedModule Verified.Pattern Attribute.Symbol attrs ->
     FreeVariables VariableName ->
     Attributes ->
-    error (Attribute.Axiom Internal.Symbol.Symbol VariableName)
+    error (Attribute.Axiom Symbol.Symbol VariableName)
 parseAndVerifyAxiomAttributes indexModule freeVars attrs =
     parseAxiomAttributes' attrs >>= verifyAxiomAttributes indexModule
   where

diff --git a/kore/src/Kore/Equation/Registry.hs b/kore/src/Kore/Equation/Registry.hs
@@ -27,7 +27,6 @@ import Kore.Attribute.Axiom (
  )
 import qualified Kore.Attribute.Axiom as Attribute
 import Kore.Attribute.Overload
-import qualified Kore.Attribute.Pattern as Pattern
 import Kore.Attribute.Symbol (
     StepperAttributes,
  )
@@ -50,7 +49,6 @@ import Kore.Syntax.Sentence (
  )
 import qualified Kore.Verified as Verified
 import Prelude.Kore
-import qualified Pretty
 
 -- | Create a mapping from symbol identifiers to their defining axioms.
 extractEquations ::
@@ -112,11 +110,10 @@ partitionEquations equations =
     equations' =
         equations
             & filter (not . ignoreEquation)
-    (simplificationRules, unProcessedFunctionRules) =
+    (simplificationRules, functionRules) =
         partition Equation.isSimplificationRule
             . sortOn Equation.equationPriority
             $ equations'
-    functionRules = filter (not . ignoreDefinition) unProcessedFunctionRules
 
 {- | Should we ignore the 'EqualityRule' for evaluation or simplification?
 
@@ -140,17 +137,3 @@ ignoreEquation Equation{attributes}
     Unit{isUnit} = Attribute.unit attributes
     Idem{isIdem} = Attribute.idem attributes
     Overload{getOverload} = Attribute.overload attributes
-
--- | Should we ignore the 'EqualityRule' for evaluating function definitions?
-ignoreDefinition :: Equation RewritingVariableName -> Bool
-ignoreDefinition Equation{attributes, left}
-    | isLeftFunctionLike = False
-    | otherwise =
-        (error . show . Pretty.vsep)
-            [ "left-hand side of equation was not function-like at:"
-            , Pretty.indent 4 $ Pretty.pretty sourceLocation
-            ]
-  where
-    Attribute.Axiom{sourceLocation} = attributes
-    isLeftFunctionLike =
-        (Pattern.isFunction . Pattern.function) (extractAttributes left)
diff --git a/kore/src/Kore/Equation/Sentence.hs b/kore/src/Kore/Equation/Sentence.hs
@@ -38,8 +38,12 @@ import qualified Kore.Internal.TermLike as TermLike
 import Kore.Syntax.Sentence (
     SentenceAxiom (..),
  )
+import Kore.Unparser (
+    unparse,
+ )
 import qualified Kore.Verified as Verified
 import Prelude.Kore
+import Pretty
 
 fromSentenceAxiom ::
     (Attribute.Axiom Symbol VariableName, Verified.SentenceAxiom) ->
@@ -60,6 +64,40 @@ data MatchEquationError variable
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
     deriving anyclass (Debug)
 
+instance InternalVariable variable => Pretty (MatchEquationError variable) where
+    pretty (NotEquation term) =
+        Pretty.vsep
+            [ "The given term is not an equation:"
+            , unparse term
+            ]
+    pretty (RequiresError notPred) =
+        Pretty.vsep
+            [ "The equation's requires clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty (ArgumentError notPred) =
+        Pretty.vsep
+            [ "The equation's argument clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty (AntiLeftError notPred) =
+        Pretty.vsep
+            [ "The equation's anti-left clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty (EnsuresError notPred) =
+        Pretty.vsep
+            [ "The equation's ensures clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty FunctionalAxiom = "The term is a functional axiom."
+    pretty ConstructorAxiom = "The term is a constructor axiom."
+    pretty SubsortAxiom = "The term is a subsort axiom."
+
 matchEquation ::
     forall variable.
     InternalVariable variable =>

diff --git a/kore/src/Kore/Equation/Validate.hs b/kore/src/Kore/Equation/Validate.hs
@@ -0,0 +1,188 @@
+{- |
+Copyright   : (c) Runtime Verification, 2021
+License     : NCSA
+-}
+module Kore.Equation.Validate (
+    validateAxiom,
+) where
+
+import Control.Monad.State.Strict (
+    StateT,
+ )
+import qualified Data.Functor.Foldable as Recursive
+import Data.Text (
+    pack,
+ )
+import Kore.AST.Error
+import Kore.ASTVerifier.Verifier
+import Kore.Attribute.Axiom (
+    Assoc (..),
+    Comm (..),
+    Idem (..),
+    Overload (..),
+    Unit (..),
+ )
+import qualified Kore.Attribute.Axiom as Attribute (
+    Axiom (..),
+ )
+import qualified Kore.Builtin.List.List as List
+import qualified Kore.Builtin.Map.Map as Map
+import qualified Kore.Builtin.Set.Set as Set
+import Kore.Equation.Equation (
+    Equation (..),
+    isSimplificationRule,
+ )
+import Kore.Equation.Sentence (
+    MatchEquationError (..),
+    fromSentenceAxiom,
+ )
+import Kore.Internal.Predicate (
+    pattern PredicateCeil,
+    pattern PredicateIn,
+ )
+import qualified Kore.Internal.Predicate as Predicate
+import qualified Kore.Internal.Symbol as Symbol
+import qualified Kore.Internal.TermLike as TermLike
+import Kore.Syntax.Definition
+import Kore.Syntax.Variable
+import Kore.Unparser (
+    unparse,
+ )
+import qualified Kore.Verified as Verified
+import Prelude.Kore
+import qualified Pretty
+
+validateAxiom ::
+    Attribute.Axiom TermLike.Symbol VariableName ->
+    Verified.SentenceAxiom ->
+    StateT VerifiedModule' Verifier ()
+validateAxiom attrs verified =
+    case fromSentenceAxiom (attrs, verified) of
+        Right eq@Equation{left, argument} ->
+            when (needsVerification eq) $
+                checkLHS eq left >> checkArg eq argument
+        Left err@(RequiresError _) -> failWithBadEquation err
+        Left err@(ArgumentError _) -> failWithBadEquation err
+        Left err@(AntiLeftError _) -> failWithBadEquation err
+        Left err@(EnsuresError _) -> failWithBadEquation err
+        Left (NotEquation _) -> return ()
+        Left FunctionalAxiom -> return ()
+        Left ConstructorAxiom -> return ()
+        Left SubsortAxiom -> return ()
+  where
+    failWithBadEquation =
+        koreFailWithLocations [sentenceAxiomPattern verified]
+            . pack
+            . show
+            . Pretty.pretty
+
+    needsVerification eq@Equation{attributes} =
+        not
+            ( isSimplificationRule eq
+                || isAssoc
+                || isComm
+                || isUnit
+                || isIdem
+                || isJust getOverload
+            )
+      where
+        Assoc{isAssoc} = Attribute.assoc attributes
+        Comm{isComm} = Attribute.comm attributes
+        Unit{isUnit} = Attribute.unit attributes
+        Idem{isIdem} = Attribute.idem attributes
+        Overload{getOverload} = Attribute.overload attributes
+
+    checkLHS eq termLike = do
+        checkAllowedFunctionSymbol
+        checkVarFunctionArguments
+      where
+        _ :< termLikeF = Recursive.project termLike
+
+        checkAllowedFunctionSymbol
+            | TermLike.App_ sym _ <- termLike =
+                unless
+                    (isAllowedFunctionSymbol sym)
+                    (throwIllegalFunctionSymbol sym)
+            | otherwise = return ()
+          where
+            isAllowedFunctionSymbol sym =
+                Symbol.isFunction sym && not (Symbol.isConstructorLike sym)
+
+        throwIllegalFunctionSymbol sym =
+            koreFailWithLocations [eq] $
+                pack $
+                    show $
+                        Pretty.vsep
+                            [ "Expected function symbol, but found constructor symbol:"
+                            , unparse sym
+                            ]
+
+        checkVarFunctionArguments =
+            failOnJust
+                eq
+                "Expected variable, but found:"
+                $ asum $ getNotVar <$> termLikeF
+
+        getNotVar (TermLike.Var_ _) = Nothing
+        getNotVar term = Just term
+
+    checkArg _ Nothing = return ()
+    checkArg eq (Just arg) =
+        traverse_
+            ( failOnJust eq "Found invalid subterm in argument of function equation:"
+                . checkArgIn
+            )
+            $ Predicate.getMultiAndPredicate arg
+      where
+        checkArgIn (PredicateIn (TermLike.Var_ _) term) =
+            findBadArgSubterm term
+        checkArgIn (PredicateCeil (TermLike.And_ _ (TermLike.Var_ _) term)) =
+            findBadArgSubterm term
+        checkArgIn badArg = Just $ Predicate.fromPredicate_ badArg
+
+        findBadArgSubterm term = case term of
+            _
+                | TermLike.isConstructorLike term -> descend
+            TermLike.App_ sym _
+                | isGoodSymbol sym -> descend
+                | otherwise -> Just term
+            TermLike.InternalBytes_ _ _ -> Nothing
+            TermLike.InternalBool_ _ -> Nothing
+            TermLike.InternalInt_ _ -> Nothing
+            TermLike.InternalString_ _ -> Nothing
+            TermLike.DV_ _ (TermLike.StringLiteral_ _) -> Nothing
+            TermLike.And_ _ _ _ -> descend
+            TermLike.Var_ _ -> Nothing
+            TermLike.Inj_ _ -> descend
+            _ -> Just term
+          where
+            _ :< termF = Recursive.project term
+            isGoodSymbol sym =
+                or
+                    [ Symbol.isConstructorLike sym
+                    , Symbol.isAnywhere sym && Symbol.isInjective sym
+                    , Map.isSymbolConcat sym
+                    , Map.isSymbolElement sym
+                    , Map.isSymbolUnit sym
+                    , Set.isSymbolConcat sym
+                    , Set.isSymbolElement sym
+                    , Set.isSymbolUnit sym
+                    , List.isSymbolConcat sym
+                    , List.isSymbolElement sym
+                    , List.isSymbolUnit sym
+                    ]
+            descend = asum $ findBadArgSubterm <$> termF
+
+    failOnJust _ _ Nothing = return ()
+    failOnJust eq errorMessage (Just term) =
+        koreFailWithLocations
+            [term]
+            ( pack $
+                show $
+                    Pretty.vsep
+                        [ errorMessage
+                        , Pretty.indent 4 $ unparse term
+                        , "The equation that the above occurs in is:"
+                        , Pretty.indent 4 $ Pretty.pretty eq
+                        ]
+            )
diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs
@@ -1105,12 +1105,6 @@ hasFreeVariable ::
     Bool
 hasFreeVariable variableName = isFreeVariable variableName . freeVariables
 
-{- | Traverse the predicate from the top down and apply substitutions.
-
-The 'freeVariables' annotation is used to avoid traversing subterms that
-contain none of the targeted variables.
--}
-
 -- !!  TODO The following is just a temporary solution and  !!
 -- !!  the code using wrapPredicate should be refactored    !!
 
@@ -1124,6 +1118,11 @@ wrapPredicate =
         id
         . makePredicate
 
+{- | Traverse the predicate from the top down and apply substitutions.
+
+The 'freeVariables' annotation is used to avoid traversing subterms that
+contain none of the targeted variables.
+-}
 substitute ::
     InternalVariable variable =>
     Map (SomeVariableName variable) (TermLike variable) ->

diff --git a/kore/src/Kore/Internal/Symbol.hs b/kore/src/Kore/Internal/Symbol.hs
@@ -14,6 +14,7 @@ module Kore.Internal.Symbol (
     isTotal,
     isInjective,
     isMemo,
+    isAnywhere,
     noEvaluators,
     symbolHook,
     constructor,
@@ -170,6 +171,9 @@ isTotal = Attribute.isTotal . symbolAttributes
 isMemo :: Symbol -> Bool
 isMemo = Attribute.isMemo . Attribute.memo . symbolAttributes
 
+isAnywhere :: Symbol -> Bool
+isAnywhere = Attribute.isAnywhere . Attribute.anywhere . symbolAttributes
+
 noEvaluators :: Symbol -> Bool
 noEvaluators =
     Attribute.hasNoEvaluators . Attribute.noEvaluators . symbolAttributes