Merge pull request #1943 from GaloisInc/T1938

`w4_abc_{aiger,verilog}`: Handle variable-less properties correctly

Author: mergify[bot]

intTests/test1938/Makefile

@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -frecord-command-line -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test1938/test.bc

@@ -0,0 +1,3 @@
+void test(int *x) {
+    *x = 2;
+}

intTests/test1938/test.c

@@ -0,0 +1,18 @@
+// Test that the `abc` and `w4_abc_verilog` proof scripts will report invalid
+// goals that do not contain any variables. We test this both directly (with the
+// trivial `False` property) as well as via an LLVM verification involving a
+// proof goal that evaluates to `False`.
+
+fails (prove_print abc            {{ False }});
+fails (prove_print w4_abc_verilog {{ False }});
+
+m <- llvm_load_module "test.bc";
+
+// This will generate a failing proof goal about `x` being read-only.
+let setup = do {
+  x <- llvm_alloc_readonly (llvm_int 32);
+  llvm_execute_func [x];
+};
+
+fails (llvm_verify m "test" [] true setup abc);
+fails (llvm_verify m "test" [] true setup w4_abc_verilog);

intTests/test1938/test.saw

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

intTests/test1938/test.sh

@@ -8,16 +8,16 @@ module SAWScript.Prover.ABC
 import Control.Monad (unless)
 import Control.Monad.IO.Class
 import qualified Data.ByteString.Char8 as C8
-import Data.Char (isSpace)
 import Data.List (isPrefixOf)
 import qualified Data.Map as Map
 import Data.Maybe
 import qualified Data.Text as Text
 import Text.Read (readMaybe)
 
 import System.Directory
+import System.FilePath ((</>))
 import System.IO
-import System.IO.Temp (emptySystemTempFile)
+import System.IO.Temp (createTempDirectory, getCanonicalTemporaryDirectory)
 import System.Process (readProcessWithExitCode)
 
 import qualified Data.AIG as AIG
@@ -105,30 +105,33 @@ w4AbcExternal ::
   SATQuery ->
   TopLevel (Maybe CEX, String)
 w4AbcExternal exporter argFn _hashcons satq =
-       -- Create temporary files
-    do let tpl = "abc_verilog.v"
-           tplCex = "abc_verilog.cex"
-       tmp <- liftIO $ emptySystemTempFile tpl
-       tmpCex <- liftIO $ emptySystemTempFile tplCex
+       -- Create a temporary directory to put input and output files
+    do canonTmpDir <- liftIO getCanonicalTemporaryDirectory
+       tmpDir <- liftIO $ createTempDirectory canonTmpDir "saw_abc_external"
+       let tmp = tmpDir </> "abc_verilog.v"
+           tmpCex = tmpDir </> "abc_verilog.cex"
 
        (argNames, argTys) <- unzip <$> exporter tmp satq
 
        -- Run ABC and remove temporaries
        let execName = "abc"
            args = ["-q", argFn tmp tmpCex]
        (_out, _err) <- liftIO $ readProcessExitIfFailure execName args
-       cexText <- liftIO $ C8.unpack <$> C8.readFile tmpCex
-       liftIO $ removeFile tmp
-       liftIO $ removeFile tmpCex
-
-       -- Parse and report results
-       res <- if all isSpace cexText
-              then return Nothing
-              else do cex <- liftIO $ parseAigerCex cexText argTys
-                      case cex of
-                        Left parseErr -> fail parseErr
-                        Right vs -> return $ Just model
-                          where model = zip argNames (map toFirstOrderValue vs)
+       cexExists <- liftIO $ doesFileExist tmpCex
+       res <-
+         if cexExists
+           then do
+             -- If a counterexample file exists, parse and report the results.
+             cexText <- liftIO $ C8.unpack <$> C8.readFile tmpCex
+             cex <- liftIO $ parseAigerCex cexText argTys
+             case cex of
+               Left parseErr -> fail parseErr
+               Right vs -> return $ Just model
+                 where model = zip argNames (map toFirstOrderValue vs)
+           else
+             -- Otherwise, there is no counterexample.
+             return Nothing
+       liftIO $ removeDirectoryRecursive tmpDir
        return (res, "abc_verilog")
 
 parseAigerCex :: String -> [FiniteType] -> IO (Either String [FiniteValue])
@@ -137,11 +140,15 @@ parseAigerCex text tys =
     -- Output from `write_cex`
     [cex] ->
       case words cex of
+        -- Queries with no variables will result in a blank line of output.
+        [] -> pure $ liftCexBB tys []
         [bits] -> liftCexBB tys <$> mapM bitToBool bits
         _ -> fail $ "invalid counterexample line: " ++ cex
     -- Output from `write_aiger_cex`
     [_, cex] ->
       case words cex of
+        -- Queries with no variables will result in an empty vector of output.
+        [_] -> pure $ liftCexBB tys []
         [bits, _] -> liftLECexBB tys <$> mapM bitToBool bits
         _ -> fail $ "invalid counterexample line: " ++ cex
     _ -> fail $ "invalid counterexample text: " ++ text