From 8f7319885ce43e2b63170b1c42e308d203fb41f0 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 19 Sep 2023 15:05:01 -0400 Subject: [PATCH] w4_abc_{aiger,verilog}: Handle variable-less properties correctly Previously, any proofs involving the `w4_abc_aiger` (a.k.a., `abc`) or `w4_abc_verilog` proof scripts would succeed if they did not involve any variables, even false properties (e.g., `False`). This happened for a very silly reason: the counterexamples that the `abc` would generate contained a blank output (since there are no variables to describe), and SAW was misinterpreting this as a successful proof. Oops! With this patch, SAW now properly distinguishes between an successful proof (in which case no counterexample file will be generated) and a unsuccessful proof involving no variables (in which case a blank counterexample file will be generated). This is admittedly a bit fiddly, as it requires making some assumptions about the format of the counterexample files that `abc` produces. Nevertheless, this does work on all the examples that I have tried. Fixes #1938. --- intTests/test1938/Makefile | 11 +++++++++ intTests/test1938/test.bc | Bin 0 -> 2524 bytes intTests/test1938/test.c | 3 +++ intTests/test1938/test.saw | 18 +++++++++++++++ intTests/test1938/test.sh | 3 +++ src/SAWScript/Prover/ABC.hs | 45 +++++++++++++++++++++--------------- 6 files changed, 61 insertions(+), 19 deletions(-) create mode 100644 intTests/test1938/Makefile create mode 100644 intTests/test1938/test.bc create mode 100644 intTests/test1938/test.c create mode 100644 intTests/test1938/test.saw create mode 100755 intTests/test1938/test.sh diff --git a/intTests/test1938/Makefile b/intTests/test1938/Makefile new file mode 100644 index 0000000000..ebf9cc47cc --- /dev/null +++ b/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 diff --git a/intTests/test1938/test.bc b/intTests/test1938/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..31829aa3f559f4658b6502403e0993e71af7459c GIT binary patch literal 2524 zcmXvQe@q+a^*he+8L-bLL5*q7?l~r%m(}>pufPl&*eQVxt*SQLmsqY=S|*kC)h$xhcPr{G)7}1Mt?twzVMf_` zwZxs3eo)O=yQZ0siF(VV>V*D8!gO)|+!bay3-`XmAS4G`e@t4=IJ=Pc8?|#v?QuXg zUz1H;PuMN)b4;y!f~g_qbcn3baceS(s^tAkGZJ)0g-|b?J=&#v_7wo(N9B5wkx7FI z!9O4b2FPes2>EeLkH=9uuHGP+`&#v8O1_bz?`Y|blsuoJSK^wjPR;#o&3c^PC)B6~ zNh49AIf=)mILg6sAvnN?r8w4sIn7>5vq~@z;{hLg=Q6w z-oV@R>XI51Sa;Bzd{T+7&o9;d7d-QG^c+1SJ4*CPiu)Go0l$fHJv`Ylr-WD^eic4w zepYHu^39wuIzWcIapVTRIKT(}LTtlc@nEg&Q4#|_U~mNC7>ff*9Axk?QUv^Xv@jQi z#SILO*>Na|!yR}yK>-%owX%mC_9yWugQII@k2xGu;&Aa`Vf8~L4siHot!%J&vhmAw zqJk+aDhYZbDJoHYzbZjUIFTzr2Rd|Aa_LhkLhiUIz%c4HkTq4kiJ9_OPp?RT?f9($d{RtSe3BD$#c#)9Jq|xB zg=-_6a9%2ms)PWM7X(U3ZTHy!kd64utN zwRNt5Z)I9$tu51}c{XE&k3OF;|D80?XJmgJ6#RWcz|V&UaMUh@R6-~z)ZF=j;xSS@ zu~B;oYPUnN!%%s!g3+rtm&9aU*V3DD&E__}x1;`?(0Em6TIQ|ayvCbzw%Y$2VizJ& z9GyGU`!t~tJ)rq%p**zettIu(2&f-Ar&S*~%Fa&lExC+&-r5chd7f_Dvzn)Y&CGmM z0hS68&<9FRj{|e@bGu3^zeqi>QD3mSrS(qD-p-MY9rYF{&|PDm=i3+fqm!AI8Eb1U z({^jAHJbq&+j89tqf!i7je-OFgqnY>P=ynt$JCjh6wI!U-2@(Hs7|k-y&OQ`PN+DZHPV?8v{MN zg@_*#aGXJC0&*;%>1M3cvYPTheK(_v&s@23_f%4;cek19E$=0?zsa)KOWyuE7q4l& zdbRd+urlNchU#3#fstX4F);4%1zjVdknz-rYi!u#3k8kc4%dZ2Uq8^`1<%lsG3baG zg08@zKV%&Ah0en1pi#WT)Y{O}e6rD1@Af)Po|A07$pKt*Lt~TM*)9t;`8b4<}qjA5iWbGmfW zI6I+~>7;~dLRk$Q5Zd}CVXcB7hz}V6gAi*YBo;QuHcmBU4peJ0YpAzk`xsn^wA-$54?{|u=2GVT5P$Mrj?%Ju(Y*2cNJ+S~4pV_FV^IRN{>kFMBDnM3? zbt^fj0O`~-9p wWuRM7)) 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,11 +105,11 @@ 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 @@ -117,18 +117,21 @@ w4AbcExternal exporter argFn _hashcons satq = 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