Draft: GameDLC Improvements

[djmorel]

Added a new branch for Game/DLC/. This branch serves as a workspace for improving documentation and examples already present in Game/DLC/.

Updates will include:

• Improving the documentation in GameDLC.md to make the "Lessons Learned" for the covered functions clearer.
• Include additional sections in GameDLC.md for functions that appear in DLC/src/, but are not already covered.
• Reorganize and simplify the functions in DLC/src/.
• Reorganize and simplify the proofs in DLC/proofs/.
• Add additional functions and their corresponding SAW contracts to provide more examples of the SAW Python API.

[WeeknightMVP]

Python scripts that use bitcode, specs, or other data in files should refer to them relative to the script's location rather than the current working directory, as a user could try to run the script from different locations. So code like this:

base = os.getcwd()

bcname = base + '/build/foo.bc'
cryname = base + '/spec/Foo.cry'

m = llvm_load_module(bcname)
load_cryptol_file(cryname)

...should be refactored to...

if __name__ == '__main__':
    base = Path(__file__).parents[1]  # whichever parent is common to other filenames in the script
    bcpath = base/"build/foo.bc"
    crypath = base/"spec/Foo.cry"

    m = load_module(str(bcpath))
    load_cryptol_file(str(crypath))

...for portability to multiple platforms and initial working directories. It would be nice if Cryptol/SAW APIs accepted other pathlike filenames, but for now these have to be converted to strs.

Afterward, cd ... commands can be removed from Makefiles and one can simply run the Python scripts. If you need to run a Makefile in a different directory, there are a couple of useful command line options:

       -C dir, --directory=dir
            Change to directory dir before reading the makefiles or
            doing anything else.  If multiple -C options are specified,
            each is interpreted relative to the previous one: -C / -C
            etc is equivalent to -C /etc.  This is typically used with
            recursive invocations of make.
       -f file, --file=file, --makefile=FILE
            Use file as a makefile.

This is better as it restores the initial working directory even if a build error occurs.

[WeeknightMVP]

Also, a Makefile should specify a target for any file that any recipes generate (e.g. an LLVM bitcode module or log file), declare any target that is not an actual file (e.g. all, build, prove) as .PHONY, and declare a directory as an order-only prerequisite with a distinct target, e.g.:

all: build

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

build:
	mkdir -p $(ARTIFACTS)
	clang -c -g -emit-llvm -o $(ARTIFACTS)/ceilLog2.bc $(SRC)/ceilLog2.c

clean:
	rm -r $(ARTIFACTS)

...should be changed to...

all: build

build: $(ARTIFACTS)/ceilLog2.bc

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

clean:
	rm -rf $(ARTIFACTS)

.PHONY: all build prove clean

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

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

[djmorel]

Excellent points @WeeknightMVP! I added both of your suggestions to #217 for an immediate fix. Always good to make things more portable :)