diff --git a/.github/ci.sh b/.github/ci.sh new file mode 100755 index 0000000..4db364f --- /dev/null +++ b/.github/ci.sh @@ -0,0 +1,34 @@ +#!/usr/bin/env bash +set -Eeuxo pipefail + +DATE=$(date "+%Y-%m-%d") +[[ "$RUNNER_OS" == 'Windows' ]] && IS_WIN=true || IS_WIN=false +BIN=bin +EXT="" +$IS_WIN && EXT=".exe" +mkdir -p "$BIN" + +is_exe() { [[ -x "$1/$2$EXT" ]] || command -v "$2" > /dev/null 2>&1; } + +install_solvers() { + (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BUILD_TARGET_OS-$BUILD_TARGET_ARCH-bin.zip" && unzip -o bins.zip && rm bins.zip) + cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT + chmod +x $BIN/* +} + +install_system_deps() { + install_solvers + export PATH=$PWD/$BIN:$PATH + echo "$PWD/$BIN" >> $GITHUB_PATH + is_exe "$BIN" boolector && \ + is_exe "$BIN" bitwuzla && \ + is_exe "$BIN" cvc4 && \ + is_exe "$BIN" cvc5 && \ + is_exe "$BIN" yices && \ + is_exe "$BIN" z3 +} + +COMMAND="$1" +shift + +"$COMMAND" "$@" diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 988fcb1..b69ae7a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -6,6 +6,7 @@ permissions: contents: read env: + SOLVER_PKG_VERSION: "snapshot-20241119" # The NAME makes it easier to copy/paste snippets from other CI configs NAME: stubs @@ -94,7 +95,28 @@ jobs: key: ${{ env.key }}-plan-${{ hashFiles('**/plan.json') }} restore-keys: ${{ env.key }}- - - run: cabal build + - shell: bash + name: Install system dependencies + run: .github/ci.sh install_system_deps + env: + BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip + BUILD_TARGET_OS: ${{ matrix.os }} + BUILD_TARGET_ARCH: ${{ runner.arch }} + + - name: Configure + run: cabal configure -j2 --enable-tests + + - name: Build + run: cabal build + + - name: Run parser tests + run: cabal test parser-tests + + - name: Run translator tests + run: cabal test translator-tests + + - name: Run stubs tests + run: cabal test stubs-tests - name: Cache dependencies uses: actions/cache/save@v3 diff --git a/stubs-translator/tests/Main.hs b/stubs-translator/tests/Main.hs index 419857c..ad8f159 100644 --- a/stubs-translator/tests/Main.hs +++ b/stubs-translator/tests/Main.hs @@ -17,7 +17,6 @@ import qualified Data.Parameterized.Context as Ctx import qualified Stubs.Translate as ST import qualified Data.Macaw.X86 as DMX import Data.Macaw.X86.Symbolic () -import qualified Lang.Crucible.Syntax.Concrete as LCSC import qualified Data.Parameterized as P import qualified Lang.Crucible.CFG.Core as LCCC import qualified Data.Parameterized.NatRepr as PN @@ -31,7 +30,7 @@ import qualified Data.Macaw.CFG as DMC testEnv = STC.StubsEnv @DMX.X86_64 (DMC.memWidthNatRepr @(DMC.ArchAddrWidth DMX.X86_64)) MapF.empty MapF.empty testFnTranslationBasic :: TestTree -testFnTranslationBasic = testCase "Basic Translation" $ do +testFnTranslationBasic = testCase "Basic Translation" $ do hAlloc <- LCF.newHandleAllocator Some ng <- PN.newIONonceGenerator let fn = SA.StubsFunction { @@ -43,18 +42,19 @@ testFnTranslationBasic = testCase "Basic Translation" $ do SA.stubFnBody=[SA.Assignment (SA.StubsVar "v" SA.StubsIntRepr) (SA.LitExpr $ SA.IntLit 20),SA.Return (SA.LitExpr $ SA.IntLit 20)] } p <- ST.translateDecls @DMX.X86_64 ng hAlloc [] [] testEnv MapF.empty [] [SA.SomeStubsFunction fn] - let cfgs = map fst p + let cfgs = map fst p -- Expect single CFG assertEqual "Unexpected CFG count" (length cfgs) 1 - LCSC.ACFG _ r _ <- return $ head cfgs + LCCR.AnyCFG m <- return $ head cfgs + let r = cfgReturnType m -- Expect Int to be BV 32 on X86_64 -- TODO: make less brittle - Just P.Refl <- return $ P.testEquality r $ LCCC.BVRepr (PN.knownNat @32) + Just P.Refl <- return $ P.testEquality r $ LCCC.BVRepr (PN.knownNat @32) return () -testFnTranslationITE :: TestTree -testFnTranslationITE = testCase "ITE Translation" $ do +testFnTranslationITE :: TestTree +testFnTranslationITE = testCase "ITE Translation" $ do hAlloc <- LCF.newHandleAllocator Some ng <- PN.newIONonceGenerator let fn = SA.StubsFunction { @@ -66,17 +66,17 @@ testFnTranslationITE = testCase "ITE Translation" $ do SA.stubFnBody=[SA.ITE (SA.LitExpr $ SA.BoolLit True) [SA.Assignment (SA.StubsVar "v" SA.StubsIntRepr) (SA.LitExpr $ SA.IntLit 20)] [SA.Assignment (SA.StubsVar "v" SA.StubsIntRepr) (SA.LitExpr $ SA.IntLit 40)],SA.Return (SA.LitExpr $ SA.IntLit 20)] } p <- ST.translateDecls @DMX.X86_64 ng hAlloc [] [] testEnv MapF.empty [] [SA.SomeStubsFunction fn] - let cfgs = map fst p + let cfgs = map fst p -- Expect single CFG assertEqual "Unexpected CFG count" 1 (length cfgs) - LCSC.ACFG _ _ m <- return $ head cfgs - + LCCR.AnyCFG m <- return $ head cfgs + let blocks = LCCR.cfgBlocks m assertEqual "Unexpected Block count" 4 (length blocks) -testFnTranslationLoop :: TestTree -testFnTranslationLoop = testCase "Loop Translation" $ do +testFnTranslationLoop :: TestTree +testFnTranslationLoop = testCase "Loop Translation" $ do hAlloc <- LCF.newHandleAllocator Some ng <- PN.newIONonceGenerator let fn = SA.StubsFunction { @@ -92,13 +92,13 @@ testFnTranslationLoop = testCase "Loop Translation" $ do -- Expect single CFG assertEqual "Unexpected CFG count" 1 (length cfgs) - LCSC.ACFG _ _ m <- return $ head cfgs + LCCR.AnyCFG m <- return $ head cfgs let blocks = LCCR.cfgBlocks m assertEqual "Unexpected Block count" 4 (length blocks) -- While this could be only 3, due to the Generator's implementation 4 blocks are made total -testOpaquenessCheckRet :: TestTree -testOpaquenessCheckRet = testCase "Catch Opaqueness Violation in return" $ do +testOpaquenessCheckRet :: TestTree +testOpaquenessCheckRet = testCase "Catch Opaqueness Violation in return" $ do Some counter <- return $ LCCC.someSymbol "Counter" let lib = SA.mkStubsModule "counter" [ SA.SomeStubsFunction @@ -112,8 +112,8 @@ testOpaquenessCheckRet = testCase "Catch Opaqueness Violation in return" $ do ] [] [] assertBool "Failed to catch opaqueness violation in return stmt" (not (SO.satOpaque lib)) -testOpaquenessCheckArg :: TestTree -testOpaquenessCheckArg = testCase "Catch Opaqueness Violation in argument" $ do +testOpaquenessCheckArg :: TestTree +testOpaquenessCheckArg = testCase "Catch Opaqueness Violation in argument" $ do Some counter <- return $ LCCC.someSymbol "Counter" let lib = SA.mkStubsModule "counter" [ SA.SomeStubsFunction @@ -135,8 +135,8 @@ testOpaquenessCheckArg = testCase "Catch Opaqueness Violation in argument" $ do ] [] [] assertBool "Failed to catch opaqueness violation in argument" (not (SO.satOpaque lib)) -testOpaquenessCheckAssignmentBad :: TestTree -testOpaquenessCheckAssignmentBad = testCase "Catch Opaqueness Violation in variable assignment" $ do +testOpaquenessCheckAssignmentBad :: TestTree +testOpaquenessCheckAssignmentBad = testCase "Catch Opaqueness Violation in variable assignment" $ do Some counter <- return $ LCCC.someSymbol "Counter" let lib = SA.mkStubsModule "counter" [ SA.SomeStubsFunction SA.StubsFunction { @@ -150,8 +150,8 @@ testOpaquenessCheckAssignmentBad = testCase "Catch Opaqueness Violation in varia ] [] [] assertBool "Failed to catch opaqueness violation in variable assignment" (not (SO.satOpaque lib)) -testOpaquenessCheckAssignmentOK :: TestTree -testOpaquenessCheckAssignmentOK = testCase "Allow type changing with decl" $ do +testOpaquenessCheckAssignmentOK :: TestTree +testOpaquenessCheckAssignmentOK = testCase "Allow type changing with decl" $ do Some counter <- return $ LCCC.someSymbol "Counter" let lib = SA.mkStubsModule "counter" [ SA.SomeStubsFunction SA.StubsFunction { @@ -167,4 +167,4 @@ testOpaquenessCheckAssignmentOK = testCase "Allow type changing with decl" $ do main :: IO () main = defaultMain $ do - testGroup "" [testFnTranslationBasic, testFnTranslationITE, testFnTranslationLoop, testOpaquenessCheckRet, testOpaquenessCheckArg, testOpaquenessCheckAssignmentBad, testOpaquenessCheckAssignmentOK] \ No newline at end of file + testGroup "" [testFnTranslationBasic, testFnTranslationITE, testFnTranslationLoop, testOpaquenessCheckRet, testOpaquenessCheckArg, testOpaquenessCheckAssignmentBad, testOpaquenessCheckAssignmentOK]