From a0f2dc95ed9b3c7606ceea5a17db97ce40c08048 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Sat, 23 Oct 2021 15:39:16 -0300 Subject: [PATCH 1/4] Check the tree-like invariant in PLE. --- src/Language/Fixpoint/Solver/PLE.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs index 5b08dee5c..1e96fb696 100644 --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -327,7 +327,7 @@ updCtxRes res iMb ctx = (ctx, res') updRes :: InstRes -> Maybe BindId -> Expr -> InstRes -updRes res (Just i) e = M.insert i e res +updRes res (Just i) e = M.insertWith (error "tree-like invariant broken in ple. See https://github.com/ucsd-progsys/liquid-fixpoint/issues/496") i e res updRes res Nothing _ = res ---------------------------------------------------------------------------------------------- From 07e45cfeb9b316b43a70e18509efa03de9a0e3c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Mon, 4 Oct 2021 18:25:45 -0300 Subject: [PATCH 2/4] Have sendConcreteBindingsToSMT pass the state from the continuation --- src/Language/Fixpoint/Solver/Monad.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Language/Fixpoint/Solver/Monad.hs b/src/Language/Fixpoint/Solver/Monad.hs index 348433577..a63d3bebd 100644 --- a/src/Language/Fixpoint/Solver/Monad.hs +++ b/src/Language/Fixpoint/Solver/Monad.hs @@ -144,11 +144,13 @@ sendConcreteBindingsToSMT known act = do , not (F.memberIBindEnv i known) ] st <- get - withContext $ \me -> do + (a, st') <- withContext $ \me -> do smtBracket me "" $ do forM_ concretePreds $ \(i, e) -> smtDefineFunc me (F.bindSymbol (fromIntegral i)) [] F.boolSort e - flip evalStateT st $ act $ F.unionIBindEnv known $ F.fromListIBindEnv $ map fst concretePreds + flip runStateT st $ act $ F.unionIBindEnv known $ F.fromListIBindEnv $ map fst concretePreds + put st' + return a where isShortExpr F.PTrue = True isShortExpr F.PTop = True From 6ea3c59b39e06468635ce437a1b9eb79d5768794 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Wed, 6 Oct 2021 19:46:38 -0300 Subject: [PATCH 3/4] Remove redundant constraint from sinfoToFInfo --- src/Language/Fixpoint/Types/Constraints.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs index d3d8f11e2..663607d44 100644 --- a/src/Language/Fixpoint/Types/Constraints.hs +++ b/src/Language/Fixpoint/Types/Constraints.hs @@ -850,7 +850,7 @@ outVV (m, fi) i c = (m', fi') type BindM = M.HashMap Integer BindId -sinfoToFInfo :: Fixpoint a => SInfo a -> FInfo a +sinfoToFInfo :: SInfo a -> FInfo a sinfoToFInfo fi = fi { bs = envWithoutLhss , cm = simpcToSubc (bs fi) <$> cm fi From 19023238851010b537eab4f81f09fdd862f9a4b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Tue, 26 Oct 2021 21:50:09 -0300 Subject: [PATCH 4/4] Use a VM in CI instead of docker images --- .circleci/config.yml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index c9669531b..cf8caa225 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -3,9 +3,10 @@ version: 2.0 jobs: build: - docker: - - image: fpco/stack-build:lts-16.8 + machine: + image: ubuntu-2004:202107-02 steps: + - run: sudo apt-get update && sudo apt-get install -y curl git ssh unzip wget libtinfo-dev gcc make - add_ssh_keys - run: name: Install z3 @@ -13,24 +14,25 @@ jobs: wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-ubuntu-16.04.zip unzip z3-4.8.7-x64-ubuntu-16.04.zip rm -f z3-4.8.7-x64-ubuntu-16.04.zip - cp z3-4.8.7-x64-ubuntu-16.04/bin/libz3.a /usr/local/lib - cp z3-4.8.7-x64-ubuntu-16.04/bin/z3 /usr/local/bin - cp z3-4.8.7-x64-ubuntu-16.04/include/* /usr/local/include + sudo cp z3-4.8.7-x64-ubuntu-16.04/bin/libz3.a /usr/local/lib + sudo cp z3-4.8.7-x64-ubuntu-16.04/bin/z3 /usr/local/bin + sudo cp z3-4.8.7-x64-ubuntu-16.04/include/* /usr/local/include rm -rf z3-4.8.7-x64-ubuntu-16.04 z3 --version - checkout - restore_cache: keys: - - stack-{{ checksum "stack.yaml" }}-{{ checksum "liquid-fixpoint.cabal" }} - - stack-{{ checksum "stack.yaml" }} + - stack-cache-v1-{{ checksum "stack.yaml" }}-{{ checksum "liquid-fixpoint.cabal" }} + - stack-cache-v1-{{ checksum "stack.yaml" }} - run: name: Dependencies command: | + wget -qO- https://get.haskellstack.org/ | sudo sh stack --no-terminal setup stack --no-terminal build -j2 liquid-fixpoint --only-dependencies --test --no-run-tests - save_cache: - key: stack-{{ checksum "stack.yaml" }}-{{ checksum "liquid-fixpoint.cabal" }} + key: stack-cache-v1-{{ checksum "stack.yaml" }}-{{ checksum "liquid-fixpoint.cabal" }} paths: - ~/.stack - ./.stack-work @@ -43,10 +45,9 @@ jobs: command: | mkdir -p /tmp/junit stack --no-terminal test -j2 liquid-fixpoint:test --flag liquid-fixpoint:devel --test-arguments="--xml=/tmp/junit/main-test-results.xml": - stack --no-terminal haddock --flag liquid-fixpoint:devel - stack --no-terminal sdist + stack --no-terminal haddock --flag liquid-fixpoint:devel --test --no-run-tests --no-haddock-deps --haddock-arguments="--no-print-missing-docs" # mkdir -p $CIRCLE_TEST_REPORTS/tasty # cp -r tests/logs/cur $CIRCLE_TEST_REPORTS/tasty/log - run: name: Dist - command: stack sdist + command: stack --no-terminal sdist