Verification fix and Makefile changes

[lnarmour]

Previously generateVerificationCode and generateWriteC did not work together because they both use the same eval_ prefix in the generated code. Now the verification code uses the prefix eval_verify_ instead.

Previously generateMakefile would produce a Makefile that looked something like this:

...
all: plain check
...
verify: ...

verify-rand: ...

and when you run make, only the plain and check targets are built. You have to manually run make verify to have it also build the verification code (if it was generated). But if you haven't generated the verification code, and try to run make verify then compilation will fail (obviously) because there are no C files for the verification code.

I don't think it makes sense to put verification targets in the generated Makefile if generateVerificationCode has not also been run. However, there is not a good way to determine if generateVerificationCode has been run because the system does not really keep track of state during the execution of command scripts. Instead, now this can be controlled with an additional parameter to the generateMakefile command.

There are two new commands (with the following signatures):

GenerateMakefile(Program program, String system, String outDir, boolean withVerification)
GenerateMakefile(Program program, String system, CodeGenOptions CodeGenOptions, String outDir, boolean withVerification)

The default behavior is to generate no verification targets/commands in the Makefile if withVerification is not specified.

Default behavior (no verification targets)

This command...

generateMakefile(prog, system, out);

will generate a Makefile like this:

CFLAGS= -O3  -std=c99  -I/usr/include/malloc/
LIBRARIES=-lm
CC?=gcc
OBJS = matmult.o 
all: plain check

debug: CFLAGS =-DDEBUG -g -Wall -Wextra -std=c99 -I/usr/include/malloc/
debug: all

plain: $(OBJS)
    $(CC) matmult-wrapper.c -o matmult $(OBJS) $(CFLAGS) $(LIBRARIES)

check: $(OBJS)
    $(CC) matmult-wrapper.c -o matmult.check $(OBJS) $(CFLAGS) $(LIBRARIES) -DCHECKING
clean:
    rm -f *.o matmult matmult.check

How to generate verification targets

This command passing withVerification as true...

generateMakefile(prog, system, out, true);

will generate a Makefile like this:

CFLAGS= -O3  -std=c99  -I/usr/include/malloc/
LIBRARIES=-lm
CC?=gcc
OBJS = matmult.o 
all: plain check verify verify-rand

debug: CFLAGS =-DDEBUG -g -Wall -Wextra -std=c99 -I/usr/include/malloc/
debug: all

plain: $(OBJS)
    $(CC) matmult-wrapper.c -o matmult $(OBJS) $(CFLAGS) $(LIBRARIES)

check: $(OBJS)
    $(CC) matmult-wrapper.c -o matmult.check $(OBJS) $(CFLAGS) $(LIBRARIES) -DCHECKING
verify: $(OBJS) matmult_verify.o
    $(CC) matmult-wrapper.c -o matmult.verify $(OBJS) matmult_verify.o $(CFLAGS) $(LIBRARIES) -DVERIFY

verify-rand: $(OBJS) matmult_verify.o
    $(CC) matmult-wrapper.c -o matmult.verify-rand $(OBJS) matmult_verify.o $(CFLAGS) $(LIBRARIES) -DVERIFY -DRANDOM

matmult.o : matmult.c
    $(CC) matmult.c -o matmult.o $(CFLAGS) $(LIBRARIES) -c

matmult_verify.o : matmult_verify.c
    $(CC) matmult_verify.c -o matmult_verify.o $(CFLAGS) $(LIBRARIES) -c
clean:
    rm -f *.o matmult matmult.check matmult.verify matmult.verify-rand

[rajopadhye]

This was very useful. One small fix (in the explanation above): case inconsistency in the "two new commands" listed above: GenerateMakefile --> generateMakefile

[lnarmour]

Yes, the java functions are named "GenerateMakefile" but the corresponding compiler script commands are "generateMakefile".