diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5f08806864..5e88f61ad0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -197,6 +197,40 @@ jobs: name: "saw-${{ runner.os }}-${{ matrix.ghc }}" path: "dist/bin/saw" + mr-solver-tests: + needs: [build] + strategy: + fail-fast: false + matrix: + os: [ubuntu-latest, macos-10.15] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v2 + with: + submodules: true + + - shell: bash + run: .github/ci.sh install_system_deps + env: + BUILD_TARGET_OS: ${{ matrix.os }} + + - uses: actions/download-artifact@v2 + with: + name: "${{ runner.os }}-bins" + path: dist/bin + + - name: Update PATH to include SAW + shell: bash + run: | + chmod +x dist/bin/* + echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH + + - working-directory: examples/mr_solver + shell: bash + run: | + saw monadify.saw + saw mr_solver_unit_tests.saw + heapster-tests: needs: [build] strategy: diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw index 5b5ba8974e..37e0e54d28 100644 --- a/examples/mr_solver/monadify.saw +++ b/examples/mr_solver/monadify.saw @@ -2,50 +2,113 @@ enable_experimental; import "SpecPrims.cry" as SpecPrims; import "monadify.cry"; +load_sawcore_from_file "../../cryptol-saw-core/saw/CryptolM.sawcore"; set_monadification "SpecPrims::exists" "Prelude.existsM"; set_monadification "SpecPrims::forall" "Prelude.forallM"; +let run_test name cry_term mon_term_expected = + do { print (str_concat "Test: " name); + print "Original term:"; + print_term cry_term; + mon_term <- monadify_term cry_term; + print "Monadified term:"; + print_term mon_term; + success <- is_convertible mon_term mon_term_expected; + if success then print "Success - monadified term matched expected\n" else + do { print "Test failed - did not match expected monadified term:"; + print_term mon_term_expected; + exit 1; }; }; + my_abs <- unfold_term ["my_abs"] {{ my_abs }}; -print "[my_abs] original term:"; -print_term my_abs; -my_absM <- monadify_term my_abs; -print "[my_abs] monadified term:"; -print_term my_absM; +my_abs_M <- parse_core_mod "CryptolM" "\ +\ \\(x : (mseq (TCNum 64) Bool)) -> \ +\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x' : (isFinite (TCNum 64))) -> \ +\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x'' : (isFinite (TCNum 64))) -> \ +\ ite (CompM (mseq (TCNum 64) Bool)) \ +\ (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \ +\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \ +\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x''' : (isFinite (TCNum 64))) -> \ +\ returnM (mseq (TCNum 64) Bool) (ecNeg (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x))) \ +\ (returnM (mseq (TCNum 64) Bool) x)))"; +run_test "my_abs" my_abs my_abs_M; -/* err_if_lt0 <- unfold_term ["err_if_lt0"] {{ err_if_lt0 }}; -print "[err_if_lt0] original term:"; -err_if_lt0M <- monadify_term err_if_lt0; -print "[err_if_lt0] monadified term:"; -print_term err_if_lt0M; -*/ +err_if_lt0_M <- parse_core_mod "CryptolM" "\ +\ \\(x : (mseq (TCNum 64) Bool)) -> \ +\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x' : (isFinite (TCNum 64))) -> \ +\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x'' : (isFinite (TCNum 64))) -> \ +\ ite (CompM (mseq (TCNum 64) Bool)) \ +\ (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \ +\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \ +\ (bindM (isFinite (TCNum 8)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 8)) \ +\ (\\(x''' : (isFinite (TCNum 8))) -> \ +\ ecErrorM (mseq (TCNum 64) Bool) (TCNum 5) \ +\ (seqToMseq (TCNum 5) (mseq (TCNum 8) Bool) \ +\ [ ecNumber (TCNum 120) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \ +\ , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \ +\ , ecNumber (TCNum 60) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \ +\ , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \ +\ , ecNumber (TCNum 48) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') ]))) \ +\ (returnM (mseq (TCNum 64) Bool) x)))"; +run_test "err_if_lt0" err_if_lt0 err_if_lt0_M; /* sha1 <- {{ sha1 }}; -print "[SHA1] original term:"; +print "Test: sha1"; +print "Original term:"; print_term sha1; -mtrm <- monadify_term sha1; -print "[SHA1] monadified term:"; -print_term mtrm; +sha1M <- monadify_term sha1; +print "Monadified term:"; +print_term sha1M; */ fib <- unfold_term ["fib"] {{ fib }}; -print "[fib] original term:"; -print_term fib; -fibM <- monadify_term fib; -print "[fib] monadified term:"; -print_term fibM; +fibM <- parse_core_mod "CryptolM" "\ +\ \\(_x : (mseq (TCNum 64) Bool)) -> \ +\ multiArgFixM (LRT_Fun (mseq (TCNum 64) Bool) (\\(_ : (mseq (TCNum 64) Bool)) -> LRT_Ret (mseq (TCNum 64) Bool))) \ +\ (\\(fib : ((mseq (TCNum 64) Bool) -> (CompM (mseq (TCNum 64) Bool)))) -> \ +\ \\(x : (mseq (TCNum 64) Bool)) -> \ +\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x' : (isFinite (TCNum 64))) -> \ +\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x'' : (isFinite (TCNum 64))) -> \ +\ ite (CompM (mseq (TCNum 64) Bool)) \ +\ (ecEq (mseq (TCNum 64) Bool) (PEqMSeqBool (TCNum 64) x') x \ +\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \ +\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x''' : (isFinite (TCNum 64))) -> \ +\ returnM (mseq (TCNum 64) Bool) \ +\ (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \ +\ (PLiteralSeqBoolM (TCNum 64) x''')))) \ +\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x''' : (isFinite (TCNum 64))) -> \ +\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ (\\(x'''' : (isFinite (TCNum 64))) -> \ +\ bindM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \ +\ (fib \ +\ (ecMinus (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \ +\ (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \ +\ (PLiteralSeqBoolM (TCNum 64) x'''')))) \ +\ (\\(x''''' : (mseq (TCNum 64) Bool)) -> \ +\ returnM (mseq (TCNum 64) Bool) \ +\ (ecMul (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \ +\ x''''')))))))) \ +\ _x"; +run_test "fib" fib fibM; noErrors <- unfold_term ["noErrors"] {{ SpecPrims::noErrors }}; -print "[noErrors] original term:"; -print_term noErrors; -noErrorsM <- monadify_term noErrors; -print "[noErrors] monadified term:"; -print_term noErrorsM; +noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsM a a (\\(x : a) -> returnM a x)"; +run_test "noErrors" noErrors noErrorsM; fibSpecNoErrors <- unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }}; -print "[fibSpecNoErrors] original term:"; -print_term fibSpecNoErrors; -fibSpecNoErrorsM <- monadify_term fibSpecNoErrors; -print "[fibSpecNoErrors] monadified term:"; -print_term fibSpecNoErrorsM; +fibSpecNoErrorsM <- parse_core_mod "CryptolM" "\ +\ \\(__p1 : (mseq (TCNum 64) Bool)) -> \ +\ existsM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \ +\ (\\(x : (mseq (TCNum 64) Bool)) -> \ +\ returnM (mseq (TCNum 64) Bool) x)"; +run_test "fibSpecNoErrors" fibSpecNoErrors fibSpecNoErrorsM; diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 22e4565920..9454f86a72 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -323,15 +323,17 @@ hoistIfsPrim t = do return t{ ttTerm = t' } +isConvertiblePrim :: TypedTerm -> TypedTerm -> TopLevel Bool +isConvertiblePrim x y = do + sc <- getSharedContext + io $ scConvertible sc False (ttTerm x) (ttTerm y) + checkConvertiblePrim :: TypedTerm -> TypedTerm -> TopLevel () checkConvertiblePrim x y = do - sc <- getSharedContext - str <- io $ do - c <- scConvertible sc False (ttTerm x) (ttTerm y) - pure (if c - then "Convertible" - else "Not convertible") - printOutLnTop Info str + c <- isConvertiblePrim x y + printOutLnTop Info (if c + then "Convertible" + else "Not convertible") readCore :: FilePath -> TopLevel TypedTerm diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 6d5dd09139..e53db153db 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1071,10 +1071,15 @@ primitives = Map.fromList , "object that can be passed to 'read_sbv'." ] + , prim "is_convertible" "Term -> Term -> TopLevel Bool" + (pureVal isConvertiblePrim) + Current + [ "Returns true iff the two terms are convertible." ] + , prim "check_convertible" "Term -> Term -> TopLevel ()" (pureVal checkConvertiblePrim) Current - [ "Check if two terms are convertible." ] + [ "Check if two terms are convertible and print the result." ] , prim "replace" "Term -> Term -> Term -> TopLevel Term" (pureVal replacePrim)