Skip to content

Updates on atomic_semantics #863

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mansky1 merged 6 commits into from
Jul 17, 2026
Merged

Updates on atomic_semantics #863

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
678ec37
add option to use cascompcert as VST's compcert option
dkxb Jul 15, 2026
de6d021
include alloc and free in memory event definition; (somewhat) general…
dkxb Jul 16, 2026
abd7f87
add translation from event_semantics events to atomic machine events
dkxb Jul 16, 2026
341a66a
change unrsv to fin; rw_map for Free should be updated at fin time
dkxb Jul 16, 2026
8cadf5e
use the bundled Clight in makefile
dkxb Jul 16, 2026
d502ee1
update build instructions, allow for dev version of ora
dkxb Jul 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,3 +4,7 @@
[submodule "fcf"]
path = fcf
url = https://github.com/adampetcher/fcf.git
[submodule "cascompcert"]
path = cascompcert
url = git@github.com:dkxb/CompCert.git
branch = ccc_on_3.17
32 changes: 27 additions & 5 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ endif
# COMPCERT=platform (default, choose 32 or 64 bit platform supplied x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86)
# COMPCERT=bundled (build and use bundled 32 or 64 x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86)
# COMPCERT=bundled_new (build and use bundled compcert_new 32 or 64 x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86)
# COMPCERT=cascompcert (use CASCompCert variant)
# COMPCERT=src_dir (build and use in source folder COMPCERT_SRC_DIR the variant specified by ARCH and BITSIZE)
# COMPCERT=inst_dir (use prebuilt CompCert in COMPCERT_INST_DIR - BITSIZE and ARCH can be left empty or must match)
#
Expand Down Expand Up @@ -106,6 +107,16 @@ else ifeq ($(COMPCERT),bundled_new)
COMPCERT_NEW = true
COMPCERT_INFO_PATH_REF = compcert_new
COMPCERT_BUILD_FROM_SRC = true
else ifeq ($(COMPCERT),cascompcert)
# Bundled CASCompCert variant
ifeq ($(strip $(wildcard cascompcert/* cascompcert/.[!.]* cascompcert/..?*)),)
$(warning COMPCERT=cascompcert, but the cascompcert directory does not exist or is empty. Update git submodules and try again.)
$(error Cannot continue without the CASCompCert sources)
endif
COMPCERT_SRC_DIR = cascompcert
COMPCERT_INST_DIR = cascompcert
COMPCERT_BUILD_FROM_SRC = true
FLOCQ = bundled
else ifeq ($(COMPCERT),src_dir)
# Compile CompCert from source dir
ifeq ($(COMPCERT_SRC_DIR),)
Expand Down Expand Up @@ -227,8 +238,8 @@ endif


ifeq ($(FLOCQ),bundled)
override FLOCQ= -R $(COMPCERT_INST_DIR)/flocq Flocq
COMPCERTFLOCQDIRS= compcert/flocq/*/*.v
override FLOCQ= -R $(COMPCERT_INST_DIR)/flocq Flocq
COMPCERTFLOCQDIRS= $(COMPCERT_SRC_DIR)/flocq/*/*.v
# this mode to use the flocq built into compcert
endif
ifeq ($(FLOCQ),platform)
Expand Down Expand Up @@ -272,13 +283,20 @@ ifeq ($(ZLIST),platform)
else
VSTDIRS= shared msl sepcomp veric zlist floyd $(PROGSDIR) concurrency ccc26x86 atomics
endif
OTHERDIRS= wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox boringssl_fips_20180730
OTHERDIRS= wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox boringssl_fips_20180730 atomic_machine
DIRS = $(VSTDIRS) $(OTHERDIRS)

# ##### Compcert Flags #####

COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend export $(BACKEND)

# CASCompCert carries additional proofs under the compcert.concurrency
# namespace. Include them when they are present so that individual modules
# can be built directly from this Makefile.
ifneq ($(wildcard $(COMPCERT_SRC_DIR)/concurrency),)
COMPCERTDIRS += concurrency
endif

ifeq ($(COMPCERT_EXPLICIT_PATH),true)
COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT_INST_DIR)/$(d) compcert.$(d)) $(FLOCQ)
EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_DIR)/$(d) compcert.$(d)) $(FLOCQ)
Expand Down Expand Up @@ -921,7 +939,12 @@ endif
wc .depend

clean:
rm -f $(addprefix veric/version., v vo vos vok glob) .lia.cache .nia.cache floyd/floyd.coq .depend _CoqProject _CoqProject-export $(wildcard */.*.aux) $(wildcard */*.glob) $(wildcard */*.vo */*.vos */*.vok) compcert/*/*.{vo,vos,vok} compcert/*/*/*.{vo,vos,vok} compcert_new/*/*.{vo,vos,vok} compcert_new/*/*/*.{vo,vos,vok}
rm -f $(addprefix veric/version., v vo vos vok glob) .lia.cache .nia.cache floyd/floyd.coq .depend _CoqProject _CoqProject-export $(wildcard */.*.aux) $(wildcard */*.glob) $(wildcard */*.vo */*.vos */*.vok)
for d in compcert compcert_new cascompcert; do \
if [ -d "$$d" ]; then \
find "$$d" -type f \( -name '*.vo' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' \) -delete; \
fi; \
done
rm -f progs/VSUpile/{*,*/*}.{vo,vos,vok,glob}
rm -f progs64/VSUpile/{*,*/*}.{vo,vos,vok,glob}
rm -f progs/memmgr/*.{vo,vos,vok,glob}
Expand Down Expand Up @@ -985,4 +1008,3 @@ assumptions.txt: veric/tcb.vo
# such problem, not sure exactly. -- Andrew)
include .depend
-include .depend-concur

Loading