Skip to content

Commit 6e4570f

Browse files
mkannwischermkannwischer
authored
Merge pull request #481 from pq-code-package/cbmc-add-make-smt
Add Makefile targets to generate SMT files from CBMC
2 parents 2fed435 + 05b008f commit 6e4570f

File tree

1 file changed

+146
-4
lines changed

1 file changed

+146
-4
lines changed

‎proofs/cbmc/Makefile.common‎

Lines changed: 146 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,24 @@ CBMC_FLAG_UNWINDING_ASSERTIONS ?= # set to --no-unwinding-assertions to disable
262262
CBMC_DEFAULT_UNWIND ?= --unwind 1
263263
CBMC_FLAG_FLUSH ?= --flush
264264

265+
# Determine SMT back-end and prover combination chosen by the user
266+
ifeq ($(findstring --smt2,$(CBMCFLAGS)),--smt2) # User has chosen SMT2 (which defaults to Z3)
267+
CBMCFLAGS := $(subst --smt2,,$(CBMCFLAGS)) # Remove --smt2 from CBMCFLAGS
268+
BACKEND_OPTION := --smt2
269+
PROVER_NAME=Z3
270+
SMT_FORMAT := --z3
271+
else ifeq ($(findstring --bitwuzla,$(CBMCFLAGS)),--bitwuzla) # User has chosen Bitwuzla
272+
CBMCFLAGS := $(subst --bitwuzla,,$(CBMCFLAGS)) # Remove --bitwuzla from CBMCFLAGS
273+
BACKEND_OPTION := --bitwuzla
274+
PROVER_NAME=Bitwuzla
275+
SMT_FORMAT := --bitwuzla
276+
else ifeq ($(findstring --cvc5,$(CBMCFLAGS)),--cvc5) # User has chosen cvc5
277+
CBMCFLAGS := $(subst --cvc5,,$(CBMCFLAGS)) # Remove --cvc5 from CBMCFLAGS
278+
BACKEND_OPTION := --cvc5
279+
PROVER_NAME=cvc5
280+
SMT_FORMAT := --cvc5
281+
endif
282+
265283
# CBMC flags used for property checking and coverage checking
266284

267285
CBMCFLAGS += $(CBMC_FLAG_FLUSH)
@@ -843,7 +861,7 @@ $(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
843861
$(LITANI) add-job \
844862
$(POOL) \
845863
--command \
846-
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
864+
'$(CBMC) $(CBMC_VERBOSITY) $(BACKEND_OPTION) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
847865
--inputs $^ \
848866
--outputs $@ \
849867
--ci-stage test \
@@ -860,7 +878,7 @@ $(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
860878
$(LITANI) add-job \
861879
$(POOL) \
862880
--command \
863-
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
881+
'$(CBMC) $(CBMC_VERBOSITY) $(BACKEND_OPTION) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
864882
--inputs $^ \
865883
--outputs $@ \
866884
--ci-stage test \
@@ -873,10 +891,82 @@ $(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
873891
--stderr-file $(LOGDIR)/result-err-log.txt \
874892
--description "$(PROOF_UID): checking safety properties"
875893

894+
# Force SMT generation to file using whatever backend (one of Z3, Bitwuzla, or cvc5) that the user specified
895+
$(HARNESS_GOTO).smt2: $(HARNESS_GOTO).goto
896+
$(LITANI) add-job \
897+
$(POOL) \
898+
--command \
899+
'$(CBMC) $(CBMC_VERBOSITY) $(BACKEND_OPTION) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --outfile $@ $(SMT_FORMAT) $<' \
900+
--inputs $^ \
901+
--outputs $@ \
902+
--ci-stage test \
903+
--stdout-file $(LOGDIR)/smt2-log.txt \
904+
$(MEMORY_PROFILING) \
905+
--ignore-returns 10 \
906+
--timeout $(CBMC_TIMEOUT) \
907+
--pipeline-name "$(PROOF_UID)" \
908+
--tags "stats-group:safety checks" \
909+
--stderr-file $(LOGDIR)/smt2-err-log.txt \
910+
--description "$(PROOF_UID): checking safety properties (SMT to file only)"
911+
912+
# Force SMT generation to file, but for Z3, ignoring whatever back-end the user specified
913+
$(HARNESS_GOTO).smtz: $(HARNESS_GOTO).goto
914+
$(LITANI) add-job \
915+
$(POOL) \
916+
--command \
917+
'$(CBMC) $(CBMC_VERBOSITY) --smt2 $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --outfile $@ --z3 $<' \
918+
--inputs $^ \
919+
--outputs $@ \
920+
--ci-stage test \
921+
--stdout-file $(LOGDIR)/smtz-log.txt \
922+
$(MEMORY_PROFILING) \
923+
--ignore-returns 10 \
924+
--timeout $(CBMC_TIMEOUT) \
925+
--pipeline-name "$(PROOF_UID)" \
926+
--tags "stats-group:safety checks" \
927+
--stderr-file $(LOGDIR)/smtz-err-log.txt \
928+
--description "$(PROOF_UID): checking safety properties (SMT for Z3 only)"
929+
930+
# Force SMT generation to file, but for Bitwuzla, ignoring whatever back-end the user specified
931+
$(HARNESS_GOTO).smtb: $(HARNESS_GOTO).goto
932+
$(LITANI) add-job \
933+
$(POOL) \
934+
--command \
935+
'$(CBMC) $(CBMC_VERBOSITY) --bitwuzla $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --outfile $@ --bitwuzla $<' \
936+
--inputs $^ \
937+
--outputs $@ \
938+
--ci-stage test \
939+
--stdout-file $(LOGDIR)/smtb-log.txt \
940+
$(MEMORY_PROFILING) \
941+
--ignore-returns 10 \
942+
--timeout $(CBMC_TIMEOUT) \
943+
--pipeline-name "$(PROOF_UID)" \
944+
--tags "stats-group:safety checks" \
945+
--stderr-file $(LOGDIR)/smtb-err-log.txt \
946+
--description "$(PROOF_UID): checking safety properties (SMT for Bitwuzla only)"
947+
948+
# Force SMT generation to file, but for cvc5, ignoring whatever back-end the user specified
949+
$(HARNESS_GOTO).smtc: $(HARNESS_GOTO).goto
950+
$(LITANI) add-job \
951+
$(POOL) \
952+
--command \
953+
'$(CBMC) $(CBMC_VERBOSITY) --cvc5 $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --outfile $@ --cvc5 $<' \
954+
--inputs $^ \
955+
--outputs $@ \
956+
--ci-stage test \
957+
--stdout-file $(LOGDIR)/smtc-log.txt \
958+
$(MEMORY_PROFILING) \
959+
--ignore-returns 10 \
960+
--timeout $(CBMC_TIMEOUT) \
961+
--pipeline-name "$(PROOF_UID)" \
962+
--tags "stats-group:safety checks" \
963+
--stderr-file $(LOGDIR)/smtc-err-log.txt \
964+
--description "$(PROOF_UID): checking safety properties (SMT for cvc5 only)"
965+
876966
$(LOGDIR)/property.xml: $(HARNESS_GOTO).goto
877967
$(LITANI) add-job \
878968
--command \
879-
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --show-properties --xml-ui $<' \
969+
'$(CBMC) $(CBMC_VERBOSITY) $(BACKEND_OPTION) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --show-properties --xml-ui $<' \
880970
--inputs $^ \
881971
--outputs $@ \
882972
--ci-stage test \
@@ -890,7 +980,7 @@ $(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto
890980
$(LITANI) add-job \
891981
$(POOL) \
892982
--command \
893-
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \
983+
'$(CBMC) $(CBMC_VERBOSITY) $(BACKEND_OPTION) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \
894984
--inputs $^ \
895985
--outputs $@ \
896986
--ci-stage test \
@@ -955,6 +1045,58 @@ result:
9551045
tail -4 $(LOGDIR)/result.txt
9561046
-grep FAILURE $(LOGDIR)/result.txt
9571047

1048+
_smt: $(HARNESS_GOTO).smt2
1049+
smt:
1050+
@ echo Running 'litani init'
1051+
$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
1052+
@ echo Running 'litani add-job'
1053+
$(MAKE) -B _smt
1054+
@ echo Running 'litani build'
1055+
$(LITANI) run-build
1056+
@ echo Generated SMT file for prover $(PROVER_NAME) in $(HARNESS_GOTO).smt2
1057+
1058+
_smtz: $(HARNESS_GOTO).smtz
1059+
smtz:
1060+
@ echo Running 'litani init'
1061+
$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
1062+
@ echo Running 'litani add-job'
1063+
$(MAKE) -B _smtz
1064+
@ echo Running 'litani build'
1065+
$(LITANI) run-build
1066+
@ echo Generated SMT file for Z3 in $(HARNESS_GOTO).smtz
1067+
1068+
_smtb: $(HARNESS_GOTO).smtb
1069+
smtb:
1070+
@ echo Running 'litani init'
1071+
$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
1072+
@ echo Running 'litani add-job'
1073+
$(MAKE) -B _smtb
1074+
@ echo Running 'litani build'
1075+
$(LITANI) run-build
1076+
@ echo Generated SMT file for Bitwuzla in $(HARNESS_GOTO).smtb
1077+
1078+
_smtc: $(HARNESS_GOTO).smtc
1079+
smtc:
1080+
@ echo Running 'litani init'
1081+
$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
1082+
@ echo Running 'litani add-job'
1083+
$(MAKE) -B _smtc
1084+
@ echo Running 'litani build'
1085+
$(LITANI) run-build
1086+
@ echo Generated SMT file for cvc5 in $(HARNESS_GOTO).smtc
1087+
1088+
_smtall: $(HARNESS_GOTO).smtz $(HARNESS_GOTO).smtb $(HARNESS_GOTO).smtc
1089+
smtall:
1090+
@ echo Running 'litani init'
1091+
$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
1092+
@ echo Running 'litani add-job'
1093+
$(MAKE) -B _smtall
1094+
@ echo Running 'litani build'
1095+
$(LITANI) run-build
1096+
@ echo Generated SMT files for provers Z3, Bitwuzla, and cvc5 in
1097+
@ echo $(HARNESS_GOTO).smtz
1098+
@ echo $(HARNESS_GOTO).smtb
1099+
@ echo $(HARNESS_GOTO).smtc
9581100

9591101
_property: $(LOGDIR)/property.xml
9601102
property:

0 commit comments

Comments
 (0)