CP in porting to 8.11

.gitignore

@@ -17,7 +17,11 @@ Makefile.coq
 /theories/plugin/*.mli
 /theories/Extraction/*.ml
 /theories/Extraction/*.mli
+/theories/*.ml
+/theories/*.mli
+.coqdeps.d
 
+.DS_Store
 *.bak
 Makefile.conf
 Makefile.plugin.conf

README.md

@@ -162,18 +162,6 @@ However, it can be configured for x86_32 by:
    by
 	  compcert/x86_32/Archi.v	
 
-2) In theory/L7/L6_to_Clight.v, replace the lines
-         Notation val := ulongTy.
-	 Notation uval := ulongTy.
-	 Notation val_typ := (AST.Tlong:typ).
-	 Notation Init_int x := (Init_int64 (Int64.repr x)).
-
-   by
-         Notation val := uintTy.
-	 Notation uval := uintTy.
-         Notation val_typ := (Tany32:typ).
-         Notation Init_int x := (Init_int32 (Int.repr x)).
-
 
 
 
@@ -185,15 +173,15 @@ Building the compiler:
 
   This will build the compiler and its proofs.
 
-To build the OCaml version of the compiler and the
-`CertiCoq Compile` plugin, in `theories/`, run:
 
     # sh make_plugin.sh
 
 To install Certicoq, do the following. This steps the above build steps.
 
     # make install
 
+To test the installation, go to 'certicoq/benchmark' and run
+   # make all
 
 Troubleshooting:
 ----------------------

benchmarks/.gitignore

@@ -0,0 +1,37 @@
+demo.*.c
+demo.*.h
+glue.demo.*.c
+glue.demo.*.h
+CertiCoq.Benchmarks.tests.*
+glue.CertiCoq.Benchmarks.tests.*
+Top.*
+glue.Top.*
+
+
+gc.c
+gc.h
+gc_stack.c
+gc_stack.h
+values.h
+main.c
+config.h
+
+demo1
+demo2
+demo3
+list_sum
+binom
+color
+sha
+vs_easy
+vs_hard
+
+demo1_cps
+demo2_cps
+demo3_cps
+list_sum_cps
+binom_cps
+color_cps
+sha_cps
+vs_easy_cps
+vs_hard_cps

benchmarks/Makefile

@@ -1,27 +1,58 @@
-COQOPTS = -R ../plugin CertiCoq.Plugin -I ../plugin -R ../benchmarks CertiCoq.Benchmarks
+COQOPTS = -R ../plugin CertiCoq.Plugin -I ../plugin -R ./ CertiCoq.Benchmarks -R lib CertiCoq.Benchmarks.lib
+CCOMPILER=gcc
 
-all: copy demo demo1 demo2
+# Names of the benchmarks
+TESTS=$(shell cat TESTS)
+# Names of the generated cfiles
+CFILES=$(patsubst %, CertiCoq.Benchmarks.tests.%_cps.c, $(TESTS)) $(patsubst %, CertiCoq.Benchmarks.tests.%.c, $(TESTS))
+# Names of the generated executables
+EXEC=$(TESTS) $(patsubst %, %_cps, $(TESTS))
+
+default: copy exec run
+all: copy lib exec run
+
+.PHONY: all default clean lib cleanlib tests run
+
+$(CFILES): tests
+exec: $(TESTS)
 
 copy:
 	cp ../theories/Runtime/gc.c ./
 	cp ../theories/Runtime/gc.h ./
+	cp ../theories/Runtime/gc_stack.c ./
+	cp ../theories/Runtime/gc_stack.h ./
 	cp ../theories/Runtime/values.h ./
 	cp ../theories/Runtime/main.c ./
 	cp ../theories/Runtime/config.h ./
-demo: demo.v
-	coqc $(COQOPTS) demo.v
 
-demo0: maindemo0.c gc.c CertiCoq.Benchmarks.demo.demo0.c
-	gcc -o demo0 -Wno-everything -O2 $+
+clean:
+	rm -f ./gc.c
+	rm -f ./gc.h
+	rm -f ./values.h
+	rm -f ./main.c
+	rm -f ./config.h
+	rm -f ./*.*.c
+	rm -f ./*.*.h
+	rm -f ./glue.*.*.c
+	rm -f ./glue.*.*.h
+	rm -f ./*.vo
+	rm -f $(EXEC)
+
+lib/Makefile:
+	cd lib; coq_makefile -f _CoqProject -o Makefile
+
+lib: lib/Makefile
+	$(MAKE) -C lib
 
-demo1: maindemo1.c gc.c CertiCoq.Benchmarks.demo.demo1.c
-	gcc -o demo1 -Wno-everything -O2 $+
+cleanlib:
+	$(MAKE) clean -C lib
 
-demo2: maindemo2.c gc.c CertiCoq.Benchmarks.demo.demo2.c
-	gcc -o demo2 -Wno-everything -O2 $+
+tests: tests.v
+	coqc $(COQOPTS) tests.v
 
-vs: CertiCoq.Benchmarks.demo.is_valid.c
-	gcc -o vs -Wno-everything -O2 mainvs.c gc.c $<
+$(TESTS): $(CFILES)
+	$(CCOMPILER) -o $@_cps -Wno-everything -O2 $@_main.c gc.c CertiCoq.Benchmarks.tests.$@_cps.c glue.CertiCoq.Benchmarks.tests.$@_cps.c
+	$(CCOMPILER) -o $@ -Wno-everything -O2 $@_main.c gc_stack.c CertiCoq.Benchmarks.tests.$@.c glue.CertiCoq.Benchmarks.tests.$@.c
 
-%.vo: %.v
-	coqc ${COQOPTS} $<
+run: run.sh
+	sh run.sh

benchmarks/README.md

@@ -0,0 +1,37 @@
+CertiCoq Benchmarks
+-------------------
+To compile the Coq benchmarks to C, compile and run the C files simply run
+
+  # make all
+
+This will also compile the necessary libraries located in ./lib. To avoid
+recompiling the library in the future compile with
+
+  # make
+
+To clean and recompile the library run
+
+  # make cleanlib
+  # make lib
+
+Some of these benchmarks are featured in Olivier Savary Belanger's thesis [1],
+for an old version of the compiler.
+
+How to add new benchmarks
+-------------------------
+To add a new benchmark
+
+1) Go to tests.v and add your bencmark program at the end of the file. The
+   top-level definition that is complied should be defined in the file tests.v
+   (not just imported). Write command to compile both the CPS and ANF versions
+   (otherwise the bencmarking automation will not work.
+
+2) Create a file named <benchmark_name>_main.c to run the benchmark and print
+   the result
+
+3) Go to file TESTS, add the name of the new benchmark at the end of the file.
+
+
+References
+----------
+[1] Savary Belanger, Olivier. Verified Extraction for Coq. PhD Thesis, Princeton University, 2019.

benchmarks/TESTS

@@ -0,0 +1,8 @@
+demo1
+demo2
+demo3
+list_sum
+vs_easy
+vs_hard
+binom
+color

benchmarks/benchmark_certicoq.v

@@ -0,0 +1,46 @@
+(* Compile Binom, Color, Veristar, and SHA through Certicoq
+
+Time CertiCoq should only be used for T0 or T1 
+(Since T2 does *)
+From CertiCoq Require Import CertiCoq.
+(* Unset Template Cast Propositions. *)
+
+
+(* BINOM *)
+Require Import CertiCoq.Benchmarks.Binom.
+(* Time Extraction "bench_binom.ml" main.   *)
+Time CertiCoq Compile main.
+
+
+(* Color *)
+Require Import CertiCoq.Benchmarks.Color.
+(* Time Extraction "bench_color.ml" main.  *)
+Time CertiCoq Compile main.
+
+
+(* VS*)
+Require Import CertiCoq.Benchmarks.vs.
+(* Time Extraction "bench_vs.ml" main_h.  *)
+Time CertiCoq Compile main_h. 
+
+
+
+(* SHA256 *)
+Require Import CertiCoq.Benchmarks.sha256.
+Require Import String.
+Open Scope string_scope.
+
+Definition compute_sha (m:String.string) :=  (SHA_256 (sha256.str_to_bytes m)). 
+
+
+Definition test500 := "The Secure Hash Algorithm is a family of cryptographic hash functions published by the National Institute of Standards and Technology (NIST) as a U.S. Federal Information Processing Standard (FIPS)The Secure Hash Algorithm is a family of cryptographic hash functions published by the National Institute of Standards and Technology (NIST) as a U.S. Federal Information Processing Standard (FIPS)The Secure Hash Algorithm is a family of cryptographic hash functions published by the National Institute ".
+
+Definition test200 := "The Secure Hash Algorithm is a family of cryptographic hash functions published by the National Institute of Standards and Technology (NIST) as a U.S. Federal Information Processing Standard (FIPS)".
+
+
+
+Definition benchsha := compute_sha test200.
+
+(*  Time Extraction "bench_sha.ml" benchsha. *)  
+Time CertiCoq Compile benchsha.
+

benchmarks/benchmarks.expected

@@ -0,0 +1,87 @@
+cp ../theories/Runtime/gc.c ./
+cp ../theories/Runtime/gc.h ./
+cp ../theories/Runtime/values.h ./
+cp ../theories/Runtime/main.c ./
+cp ../theories/Runtime/config.h ./
+coqc benchmark_certicoq.v
+Debug: Average time elapsed in L2 to L2k:  0.000000
+Debug: Quoting
+Debug: Finished quoting in 0.000237 s.. compiling to L7.
+Debug: Average time elapsed in L1 to L2:  0.001594
+Debug: Average time elapsed in L2 to L3:  0.000025
+Debug: Average time elapsed in L3 to L4:  0.000038
+Debug: Average time elapsed in L4 to L4_2:  0.000072
+Debug: Average time elapsed in L4_2 to L_5:  0.000016
+Debug: Average time elapsed in L4_5 to L5:  0.000181
+Debug: Average time elapsed in L5 to L6:  0.002567
+Debug: Average time elapsed in L6 to L6cc:  0.018391
+Debug: Average time elapsed in L6 to L7:  0.001182
+Debug: Finished compiling, printing to file.
+Debug: Printed to file in 0.020764 s..
+Finished transaction in 0.262 secs (0.259u,0.002s) (successful)
+Debug: Quoting
+Debug: Finished quoting in 0.168379 s.. compiling to L7.
+Debug: Average time elapsed in L1 to L2:  3.452359
+Debug: Average time elapsed in L2 to L3:  0.000443
+Debug: Average time elapsed in L3 to L4:  0.003212
+Debug: Average time elapsed in L4 to L4_2:  0.002778
+Debug: Average time elapsed in L4_2 to L_5:  0.000867
+Debug: Average time elapsed in L4_5 to L5:  0.003808
+Debug: Average time elapsed in L5 to L6:  0.131621
+Debug: Average time elapsed in L6 to L6cc:  0.517183
+Debug: Average time elapsed in L6 to L7:  2.307410
+Debug: Finished compiling, printing to file.
+Debug: Printed to file in 1.083311 s..
+Finished transaction in 65.452 secs (65.348u,0.092s) (successful)
+Debug: Quoting
+Debug: Finished quoting in 0.084067 s.. compiling to L7.
+Debug: Average time elapsed in L1 to L2:  0.417027
+Debug: Average time elapsed in L2 to L3:  0.000390
+Debug: Average time elapsed in L3 to L4:  0.008844
+Debug: Average time elapsed in L4 to L4_2:  0.003507
+Debug: Average time elapsed in L4_2 to L_5:  0.000476
+Debug: Average time elapsed in L4_5 to L5:  0.004793
+Debug: Average time elapsed in L5 to L6:  0.063707
+Debug: Average time elapsed in L6 to L6cc:  0.789461
+Debug: Average time elapsed in L6 to L7:  0.122009
+Debug: Finished compiling, printing to file.
+Debug: Printed to file in 0.617249 s..
+Finished transaction in 14.804 secs (14.776u,0.024s) (successful)
+Debug: Quoting
+Debug: Finished quoting in 0.942419 s.. compiling to L7.
+Debug: Average time elapsed in L1 to L2:  2.838754
+Debug: Average time elapsed in L2 to L3:  0.003245
+Debug: Average time elapsed in L3 to L4:  0.016461
+Debug: Average time elapsed in L4 to L4_2:  0.004647
+Debug: Average time elapsed in L4_2 to L_5:  0.001029
+Debug: Average time elapsed in L4_5 to L5:  0.008008
+Debug: Average time elapsed in L5 to L6:  0.159621
+Debug: Average time elapsed in L6 to L6cc:  0.894042
+Debug: Average time elapsed in L6 to L7:  0.256138
+Debug: Finished compiling, printing to file.
+Debug: Printed to file in 1.018279 s..
+Finished transaction in 43.781 secs (43.62u,0.151s) (successful)
+ccomp -o binom -w -O2 main.c gc.c CertiCoq.Benchmarks.Binom.main.c
+ccomp -o color -w -O2 main.c gc.c CertiCoq.Benchmarks.Color.main.c
+ccomp -o vs -w -O2 main.c gc.c CertiCoq.Benchmarks.vs.main_h.c
+ccomp -o sha -w -O2 main.c gc.c benchmark_certicoq.benchsha.c
+echo "binom"
+binom
+./binom
+Time taken 0.000014 seconds 0.014000 milliseconds
+16324
+echo "color"
+color
+./color
+Time taken 0.040422 seconds 40.422000 milliseconds
+    7f86
+echo "vs"
+vs
+./vs
+Time taken 0.078509 seconds 78.509000 milliseconds
+       0
+echo "sha"
+sha
+./sha
+Time taken 6.668135 seconds 6668.135000 milliseconds
+       0

benchmarks/binom_main.c

@@ -0,0 +1,39 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "gc.h"
+#include <time.h>
+
+
+extern void body(struct thread_info *);
+
+extern void print_Coq_Init_Datatypes_nat(unsigned long long);
+
+extern value args[];
+
+_Bool is_ptr(value s) {
+  return (_Bool) Is_block(s);
+}
+
+int main(int argc, char *argv[]) {
+  value val;
+  struct thread_info* tinfo;
+  clock_t start, end;
+  double msec, sec;
+
+  tinfo = make_tinfo();
+  start = clock();
+  // Run Coq program
+  body(tinfo);
+  end = clock();
+
+  val = tinfo -> args[1];
+  // TODO : fold over nat to print the C int
+  print_Coq_Init_Datatypes_nat(val);
+  printf("\n");
+
+  sec = (double)(end - start)/CLOCKS_PER_SEC;
+  msec = 1000*sec;
+  printf("Time taken %f seconds %f milliseconds\n", sec, msec);
+
+  return 0;
+}