Skip to content

Improvements to SAW Lab Proofs and Makefiles#217

Merged
weaversa merged 12 commits intomasterfrom
relative-proofs
Jun 26, 2022
Merged

Improvements to SAW Lab Proofs and Makefiles#217
weaversa merged 12 commits intomasterfrom
relative-proofs

Conversation

@djmorel
Copy link
Collaborator

@djmorel djmorel commented Jun 25, 2022

Features

  • Updates the SAW labs based on @WeeknightMVP 's comments about relative paths for proofs and specifying targets for Makefiles.
    • Python proof scripts can now be called anywhere!
  • Updates the python-saw CI to run SAW labs in a make prove -C format without the need to change directories via cd
  • Updated the SAW lab Makefiles to be identical except for their LAB variables
  • Updated the SAW.md documentation to reflect these changes

@djmorel djmorel added the enhancement New feature or request label Jun 25, 2022
@djmorel djmorel requested review from WeeknightMVP and weaversa June 25, 2022 22:51
Copy link
Owner

@weaversa weaversa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great work @djmorel! This makes the dual tasks of development and CI integration work together seamlessly, and provides some very nice examples others can build off of.

I'll approve but wait for @WeeknightMVP to have a say before merging, seeing as he submitted the original issue.

Copy link
Collaborator

@WeeknightMVP WeeknightMVP left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Externalizing a LAB variable in Makefiles is nice, as it establishes a consistent process for SAW Remote API builds and proofs -- so consistent that their content after LAB=name is the same. (Except for rotl, where rotl.c would be renamed rotl1.c, and rotl3.c would be renamed rotl.c. Enumerating intermediate files and declaring the last one as the representative makes sense.) This suggests that each lab's Makefile could be DRYed to something like:

# labs/SAW/name/Makefile

LAB=name
# any other variables or rules specific to this lab

include "../prove.mk"  # Nested labs would require more `..`s
# labs/SAW/prove.mk

# Note: Makefile assumes user already started the SAW remote API
# $ start-saw-remote-api

# Variables to hold relative file paths
SRC=src
PROOF=proof
SPECS=specs
ARTIFACTS=artifacts

all: build

build: $(ARTIFACTS)/$(LAB).bc

prove: build
	python3 $(PROOF)/$(LAB).py

clean:
	rm -rf $(ARTIFACTS)

.PHONY: all build prove clean

$(ARTIFACTS)/$(LAB).bc: $(SRC)/$(LAB).c | $(ARTIFACTS)
	clang -c -g -emit-llvm -o $@ $<

$(ARTIFACTS):
	mkdir -p $(ARTIFACTS)

Repository owner deleted a comment from WeeknightMVP Jun 26, 2022
@weaversa weaversa merged commit 5ea7189 into master Jun 26, 2022
@weaversa weaversa deleted the relative-proofs branch June 26, 2022 22:05
@djmorel
Copy link
Collaborator Author

djmorel commented Jun 26, 2022

I'm going to temporarily restore the relative-proofs branch to make the rotl lab use the new Makefile format. I'll also take the opportunity to update SAW.md so to reflect the naming changes @WeeknightMVP proposed.

@djmorel djmorel restored the relative-proofs branch June 26, 2022 22:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants