Build with Nix (#2259)

Author: ttuegel

.github/workflows/test.yml

@@ -0,0 +1,18 @@
+name: "Test"
+on:
+  pull_request:
+  push:
+jobs:
+  tests:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/[email protected]
+      with:
+        submodules: recursive
+    - uses: cachix/install-nix-action@v11
+    - uses: cachix/cachix-action@v7
+      with:
+        name: runtimeverification
+        signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+    - run: nix-build -A kore -A project.kore.checks
+    - run: nix-shell --run "echo OK"

default.nix

@@ -12,6 +12,7 @@ let
       inherit (haskell-nix) nixpkgsArgs;
       args = nixpkgsArgs // { };
     in import haskell-nix.sources.nixpkgs-2003 args;
+  inherit (pkgs) lib;
 
   local =
     if builtins.pathExists ./local.nix
@@ -34,6 +35,11 @@ let
             enableLibraryProfiling = profiling;
             enableExecutableProfiling = profiling;
             profilingDetail = "toplevel-functions";
+
+            # Add Z3 to PATH for unit tests.
+            components.tests.kore-test.preCheck = ''
+              export PATH="$PATH''${PATH:+:}${lib.getBin pkgs.z3}/bin"
+            '';
           };
         }
       ];

kore/test/Paths.hs

@@ -360,7 +360,7 @@ makeEvaluate termLike = do
     return actualPredicates
   where
     makeEvaluate' =
-        runSimplifierNoSMT mockEnv
+        runSimplifier mockEnv
         . Ceil.makeEvaluate SideCondition.top
         . Pattern.fromTermLike
     mockEnv = Mock.env { simplifierAxioms = mempty }

kore/test/Test/Kore/Builtin/AssocComm/CeilSimplifier.hs

@@ -128,7 +128,7 @@ import qualified Test.Kore.Builtin.List as Test.List
 import qualified Test.Kore.Builtin.Set as Test.Set
 import qualified Test.Kore.Step.MockSymbols as Mock
 import Test.Kore.Step.Simplification
-    ( runSimplifierNoSMT
+    ( runSimplifier
     )
 import Test.SMT
 import Test.Tasty.HUnit.Ext
@@ -1384,7 +1384,7 @@ test_inKeys =
         output <-
             Map.evalInKeys boolSort [termKey, termMap]
             & runMaybeT
-            & runSimplifierNoSMT testEnv
+            & runSimplifier testEnv
         case output of
             Nothing -> return Nothing
             Just result -> do

kore/test/Test/Kore/Builtin/Map.hs

@@ -489,7 +489,7 @@ test_difference_symbolic =
         actual <-
             Set.evalDifference (Application differenceSetSymbol args)
             & runMaybeT
-            & runSimplifierNoSMT testEnv
+            & runSimplifier testEnv
         assertEqual "" expect actual
 
 test_toList :: TestTree

kore/test/Test/Kore/Builtin/Set.hs

@@ -79,7 +79,7 @@ attemptEquation
     -> IO AttemptEquationResult'
 attemptEquation sideCondition termLike equation =
     Equation.attemptEquation sideCondition termLike' equation
-    & runSimplifier Mock.env
+    & runSimplifierSMT Mock.env
   where
     termLike' = TermLike.mapVariables Target.mkUnifiedNonTarget termLike
 

kore/test/Test/Kore/Equation/Application.hs

@@ -57,7 +57,7 @@ import qualified Logic
 
 import qualified Test.Kore.Step.MockSymbols as Mock
 import Test.Kore.Step.Simplification
-    ( runSimplifier
+    ( runSimplifierSMT
     )
 
 test_checkImplication :: [TestTree]
@@ -252,7 +252,7 @@ test_simplifyRightHandSide =
                 id
                 SideCondition.top
                 claim
-            & runSimplifier Mock.env
+            & runSimplifierSMT Mock.env
         assertEqual "" expected actual
     ]
 
@@ -281,4 +281,4 @@ checkImplication :: ClaimPattern -> IO [CheckImplicationResult ClaimPattern]
 checkImplication claim =
     checkImplicationWorker claim
     & Logic.observeAllT
-    & runSimplifier Mock.env
+    & runSimplifierSMT Mock.env

kore/test/Test/Kore/Parser/Regression.hs

@@ -863,7 +863,7 @@ runSteps
     strategy'
   =
     (<$>) picker
-    $ runSimplifier mockEnv
+    $ runSimplifierSMT mockEnv
     $ fromMaybe (error "Unexpected missing tree") . graphFilter
     <$> runStrategy
             breadthLimit

kore/test/Test/Kore/Reachability/Claim.hs

@@ -744,7 +744,7 @@ proveClaims breadthLimit depthLimit axioms claims alreadyProven =
         (Axioms axioms)
         (AlreadyProven (map unparseToText2 alreadyProven))
         (ToProve (map applyDepthLimit . selectUntrusted $ claims))
-    & runSimplifier mockEnv
+    & runSimplifierSMT mockEnv
   where
     mockEnv = Mock.env
     applyDepthLimit claim = (claim, depthLimit)

kore/test/Test/Kore/Reachability/OnePathStrategy.hs

@@ -374,7 +374,7 @@ test_SMT =
         -- Normal axiom: constr10(b) => a | f(b) < 0
         -- Start pattern: constr10(b) | f(b) < 0
         -- Expected: a | f(b) < 0
-        [ _actual1 ] <- runStepMockEnv
+        [ _actual1 ] <- runStepSMT
             (smtPattern Mock.b PredicatePositive)
             [ mkRewritingRule $ RewriteRule RulePattern
                 { left = smtTerm (TermLike.mkElemVar Mock.x)
@@ -405,7 +405,7 @@ test_SMT =
         -- Normal axiom: constr10(b) => a | f(b) < 0
         -- Start pattern: constr10(b) | f(b) < 0
         -- Expected: a | f(b) < 0
-        [ _actual1 ] <- runStepMockEnv
+        [ _actual1 ] <- runStepSMT
             Conditional
                 { term = Mock.functionalConstr10 Mock.b
                 , predicate = makeEqualsPredicate_
@@ -476,7 +476,7 @@ mockMetadataTools = MetadataTools
     , sortConstructors = undefined
     }
 
-mockEnv :: Env Simplifier
+mockEnv :: MonadSimplify simplifier => Env simplifier
 mockEnv = Mock.env { metadataTools = mockMetadataTools }
 
 sigmaSymbol :: Symbol
@@ -497,8 +497,8 @@ axiomMetaSigmaId :: RewriteRule VariableName
 axiomMetaSigmaId =
     RewriteRule $ rulePattern
         (metaSigma
-                (mkElemVar $ x1 Mock.testSort)
-                (mkElemVar $ x1 Mock.testSort)
+            (mkElemVar $ x1 Mock.testSort)
+            (mkElemVar $ x1 Mock.testSort)
         )
         (mkElemVar $ x1 Mock.testSort)
 
@@ -537,15 +537,15 @@ runStep
     -> IO [Pattern RewritingVariableName]
 runStep configuration axioms =
     (<$>) pickFinal
-    $ runSimplifier mockEnv
+    $ runSimplifierSMT mockEnv
     $ runStrategy Unlimited transitionRule [priorityAllStrategy axioms] (mkRewritingPattern configuration)
 
-runStepMockEnv
+runStepSMT
     :: Pattern VariableName
     -- ^left-hand-side of unification
     -> [RewriteRule RewritingVariableName]
     -> IO [Pattern RewritingVariableName]
-runStepMockEnv configuration axioms =
+runStepSMT configuration axioms =
     (<$>) pickFinal
-    $ runSimplifier Mock.env
+    $ runSimplifierSMT Mock.env
     $ runStrategy Unlimited transitionRule [priorityAllStrategy axioms] (mkRewritingPattern configuration)

kore/test/Test/Kore/Reachability/Prove.hs

@@ -637,5 +637,5 @@ evaluateWithPredicate
     -> Predicate VariableName
     -> IO CommonAttemptedAxiom
 evaluateWithPredicate (BuiltinAndAxiomSimplifier simplifier) term predicate =
-    runSimplifier Mock.env
+    runSimplifierSMT Mock.env
     $ simplifier term (SideCondition.assumeTruePredicate predicate)

kore/test/Test/Kore/Step.hs

@@ -1049,7 +1049,7 @@ match
 match first second =
     runSimplifier Mock.env matchResult
   where
-    matchResult :: Simplifier MatchResult
+    matchResult :: SimplifierT NoSMT MatchResult
     matchResult = matchIncremental first second
 
 withMatch

kore/test/Test/Kore/Step/Axiom/EvaluationStrategy.hs

@@ -400,7 +400,7 @@ testProcessedAxiomPatterns =
 testMetadataTools :: SmtMetadataTools Attribute.Symbol
 testMetadataTools = MetadataTools.build testIndexedModule
 
-testEnv :: Env Simplifier
+testEnv :: Env (SimplifierT NoSMT)
 testEnv =
     Mock.env
         { metadataTools = testMetadataTools

kore/test/Test/Kore/Step/Axiom/Matcher.hs

@@ -119,5 +119,5 @@ simplifierAxioms = Map.fromList [ (fId, fEvaluator) ]
   where
     fId = Axiom.Identifier.Application (TermLike.symbolConstructor fSymbol)
 
-env :: Test.Env Test.Simplifier
+env :: Test.Env (Test.SimplifierT Test.NoSMT)
 env = Mock.env { Test.simplifierAxioms = simplifierAxioms }