Skip to content

Commit 7b24709

Browse files
feliperodrifeliperodri
authored
Upgrade to CBMC Starter Kit 2.10 (#144)
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 360cfcd commit 7b24709

File tree

2 files changed

+54
-18
lines changed

2 files changed

+54
-18
lines changed

‎test/cbmc/proofs/Makefile.common‎

Lines changed: 35 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
55
# SPDX-License-Identifier: MIT-0
66

7-
CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.8
7+
CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.10
88

99
################################################################
1010
# The CBMC Starter Kit depends on the files Makefile.common and
@@ -450,6 +450,24 @@ ifdef APPLY_LOOP_CONTRACTS
450450
endif
451451
endif
452452

453+
# The default unwind should only be used in DFCC mode without loop contracts.
454+
# When loop contracts are applied, we only unwind specified loops.
455+
# If any loops remain after loop contracts have been applied, CBMC might try
456+
# to unwind the program indefinetly, because we do not pass default unwind
457+
# (i.e., --unwind 1) to CBMC when in DFCC mode.
458+
# We must not use a default unwind command in DFCC mode, because contract instrumentation
459+
# introduces loops encoding write set inclusion checks that must be dynamically unwound during
460+
# symex.
461+
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
462+
ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
463+
UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
464+
UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops"
465+
else
466+
UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
467+
UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops"
468+
endif
469+
endif
470+
453471
# Silence makefile output (eg, long litani commands) unless VERBOSE is set.
454472
ifndef VERBOSE
455473
MAKEFLAGS := $(MAKEFLAGS) -s
@@ -604,7 +622,7 @@ $(REWRITTEN_SOURCES):
604622
# Build targets that make the relevant .goto files
605623

606624
# Compile project sources
607-
$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
625+
$(PROJECT_GOTO)0100.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
608626
$(LITANI) add-job \
609627
--command \
610628
'$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -616,7 +634,7 @@ $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
616634
--description "$(PROOF_UID): building project binary"
617635

618636
# Compile proof sources
619-
$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
637+
$(PROOF_GOTO)0100.goto: $(PROOF_SOURCES)
620638
$(LITANI) add-job \
621639
--command \
622640
'$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -628,7 +646,7 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
628646
--description "$(PROOF_UID): building proof binary"
629647

630648
# Remove function bodies from project sources
631-
$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
649+
$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto
632650
$(LITANI) add-job \
633651
--command \
634652
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
@@ -640,7 +658,7 @@ $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
640658
--description "$(PROOF_UID): removing function bodies from project sources"
641659

642660
# Link project and proof sources into the proof harness
643-
$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
661+
$(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto
644662
$(LITANI) add-job \
645663
--command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
646664
--inputs $^ \
@@ -651,7 +669,7 @@ $(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
651669
--description "$(PROOF_UID): linking project to proof"
652670

653671
# Restrict function pointers
654-
$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
672+
$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto
655673
$(LITANI) add-job \
656674
--command \
657675
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
@@ -663,7 +681,7 @@ $(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
663681
--description "$(PROOF_UID): restricting function pointers in project sources"
664682

665683
# Fill static variable with unconstrained values
666-
$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
684+
$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto
667685
ifneq ($(strip $(CODE_CONTRACTS)),)
668686
$(LITANI) add-job \
669687
--command 'cp $^ $@' \
@@ -686,7 +704,7 @@ else
686704
endif
687705

688706
# Link CPROVER library if DFCC mode is on
689-
$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
707+
$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto
690708
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
691709
$(LITANI) add-job \
692710
--command \
@@ -709,17 +727,17 @@ else
709727
endif
710728

711729
# Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code
712-
$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
730+
$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto
713731
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
714732
$(LITANI) add-job \
715733
--command \
716-
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
734+
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
717735
--inputs $^ \
718736
--outputs $@ \
719737
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
720738
--pipeline-name "$(PROOF_UID)" \
721739
--ci-stage build \
722-
--description "$(PROOF_UID): unwinding all loops"
740+
--description $(UNWIND_0500_DESC)
723741
else ifneq ($(strip $(CODE_CONTRACTS)),)
724742
$(LITANI) add-job \
725743
--command \
@@ -735,14 +753,14 @@ else
735753
--command 'cp $^ $@' \
736754
--inputs $^ \
737755
--outputs $@ \
738-
--stdout-file $(LOGDIR)/linking-library-models-log.txt \
756+
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
739757
--pipeline-name "$(PROOF_UID)" \
740758
--ci-stage build \
741759
--description "$(PROOF_UID): not unwinding loops"
742760
endif
743761

744762
# Replace function contracts, check function contracts, instrument for loop contracts
745-
$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
763+
$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
746764
$(LITANI) add-job \
747765
--command \
748766
'$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
@@ -754,7 +772,7 @@ $(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
754772
--description "$(PROOF_UID): checking function contracts"
755773

756774
# Omit initialization of unused global variables (reduces problem size)
757-
$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
775+
$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
758776
$(LITANI) add-job \
759777
--command \
760778
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
@@ -766,7 +784,7 @@ $(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
766784
--description "$(PROOF_UID): slicing global initializations"
767785

768786
# Omit unused functions (sharpens coverage calculations)
769-
$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
787+
$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto
770788
$(LITANI) add-job \
771789
--command \
772790
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
@@ -778,7 +796,7 @@ $(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
778796
--description "$(PROOF_UID): dropping unused functions"
779797

780798
# Final name for proof harness
781-
$(HARNESS_GOTO).goto: $(HARNESS_GOTO)8.goto
799+
$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto
782800
$(LITANI) add-job \
783801
--command 'cp $< $@' \
784802
--inputs $^ \
@@ -794,7 +812,7 @@ ifdef CBMCFLAGS
794812
ifeq ($(strip $(CODE_CONTRACTS)),)
795813
CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
796814
else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),)
797-
CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
815+
CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY)
798816
endif
799817
endif
800818

‎test/cbmc/proofs/run-cbmc-proofs.py‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ def get_args():
154154
}, {
155155
"flags": ["--version"],
156156
"action": "version",
157-
"version": "CBMC starter kit 2.8",
157+
"version": "CBMC starter kit 2.10",
158158
"help": "display version and exit"
159159
}, {
160160
"flags": ["--no-coverage"],
@@ -334,6 +334,22 @@ async def configure_proof_dirs( # pylint: disable=too-many-arguments
334334
queue.task_done()
335335

336336

337+
def add_tool_version_job():
338+
cmd = [
339+
"litani", "add-job",
340+
"--command", "./lib/print_tool_versions.py .",
341+
"--description", "printing out tool versions",
342+
"--phony-outputs", str(uuid.uuid4()),
343+
"--pipeline-name", "print_tool_versions",
344+
"--ci-stage", "report",
345+
"--tags", "front-page-text",
346+
]
347+
proc = subprocess.run(cmd)
348+
if proc.returncode:
349+
logging.critical("Could not add tool version printing job")
350+
sys.exit(1)
351+
352+
337353
async def main(): # pylint: disable=too-many-locals
338354
args = get_args()
339355
set_up_logging(args.verbose)
@@ -403,6 +419,8 @@ async def main(): # pylint: disable=too-many-locals
403419

404420
await proof_queue.join()
405421

422+
add_tool_version_job()
423+
406424
print_counter(counter)
407425
print("", file=sys.stderr)
408426

0 commit comments

Comments
 (0)