Commit 491227fb authored by Michael Sammler's avatar Michael Sammler
Browse files

Merge branch 'dune_build' into 'master'

Dune build

Closes #17

See merge request !2
parents 9e1211df 39d6203a
Pipeline #35013 passed with stage
in 28 minutes and 38 seconds
......@@ -21,3 +21,4 @@ Makefile.coq.conf
_opam
/theories/examples/tutorial/tutorial
*.timing
*.gen
......@@ -5,6 +5,8 @@ stages:
variables:
CPU_CORES: "10"
MAKE_TARGET: "all_with_examples"
OCAML: "ocaml-base-compiler.4.07.1"
.template: &template
stage: build
......@@ -30,7 +32,7 @@ variables:
build-coq.8.11.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.11.2"
OPAM_PINS: "coq version 8.11.2 cerberus git git+https://github.com/rlepigre/cerberus.git#da87de09974dd4063c0b50fea7f23420374dd169"
DENY_WARNINGS: "1"
tags:
- fp-timing
......@@ -38,7 +40,7 @@ build-coq.8.11.2:
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.11.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
OPAM_PINS: "coq version 8.11.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV cerberus git git+https://github.com/rlepigre/cerberus.git#da87de09974dd4063c0b50fea7f23420374dd169"
except:
only:
- triggers
......
......@@ -573,6 +573,13 @@ code file.
//@rc::import <modpath> from <library> (for code only)
```
Note that it is not directly possible to import Coq modules from theories
defined in the same RefinedC project. To do so, one must first use a directive
like the following.
```c
//@rc::require <modpath>
```
## Context directive
The Coq context (in spec and proof sections) using the following annotation:
......
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+@make -f Makefile.coq all
all:
@dune build _build/default/refinedc.install --display short
.PHONY: all
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache
dune clean
all_with_examples:
@dune build --display short
.PHONY: all_with_examples
clean:
@dune clean
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
install:
@dune install
.PHONY: install
# Install build-dependencies
build-dep/opam: refinedc.opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <refinedc.opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
uninstall:
@dune uninstall
.PHONY: uninstall
C_SRC = $(wildcard examples/*.c) $(wildcard tutorial/*.c)
build-dep-opamfiles: build-dep/opam phony
%.c.gen: %.c
@dune exec -- refinedc check --no-build $<
@touch $@
generate_all: $(addsuffix .gen, $(C_SRC))
.PHONY: generate_all
build-dep-opamfiles: build-dep/opam
@true
.PHONY: build-dep-opamfiles
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
# Create a virtual Opam package with the same dependencies as RefinedC.
build-dep/opam: refinedc.opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@head -n -5 $< > $@
@sed -i -E 's/^name: *"(.*)" */name: "\1-builddep"/' $@
# Install the virtual Opam package to ensure that:
# 1) dependencies of RefinedC are installed,
# 2) they will remain satisfied even if other packages are updated/installed,
# 3) we do not have to pin the RefinedC package itself (which takes time).
build-dep: build-dep/opam
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
update-deps: refinedc.opam refinedc-rcgen.opam
opam pin add -n -y refinedc .
opam pin add -n -y refinedc-rcgen .
opam install --working-dir --deps-only refinedc refinedc-rcgen
.PHONY: update-deps
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
%.opam: ;
Makefile.local: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
.PHONY: build-dep
# FIXME
#TUTORIAL_SRC = \
# theories/examples/tutorial/t3_list.c \
# theories/examples/tutorial/t4_alloc.c \
# theories/examples/tutorial/t5_main.c \
# theories/examples/spinlock/spinlock.c
#
#theories/examples/tutorial/tutorial: $(TUTORIAL_SRC)
# clang -fdouble-square-bracket-attributes -Wno-unknown-attributes -g -O0 $^ -o $@
# The .SILENT is necessary because EXTRA_COQFILES contains many files
# and we don't want to print them. Also .PHONY is necessary since the
# files are not dependencies of Makefile.coq.
.SILENT: Makefile.coq
.PHONY: Makefile.coq
EXTRA_COQFILES := $(shell find theories -name "*.v" -and -not -name ".*")
# Default target
all:
.PHONY: all_without_examples
all_without_examples: theories/typing/typing.vo
# Generation of examples using [ail_to_coq].
%.generate: % phony
./scripts/rcgen $<
@touch $@
ALL_EXAMPLES_GENERATE = $(wildcard theories/examples/*/*.generate)
ALL_TUTORIAL_GENERATE = $(wildcard theories/examples/tutorial/*.generate)
.PHONY: all_examples all_tutorial
all_examples: $(ALL_EXAMPLES_GENERATE)
all_tutorial: $(ALL_TUTORIAL_GENERATE)
TUTORIAL_SRC = \
theories/examples/tutorial/t3_list.c \
theories/examples/tutorial/t4_alloc.c \
theories/examples/tutorial/t5_main.c \
theories/examples/spinlock/spinlock.c
theories/examples/tutorial/tutorial: $(TUTORIAL_SRC)
clang -fdouble-square-bracket-attributes -Wno-unknown-attributes -g -O0 $^ -o $@
-Q theories refinedc
-Q _build/default/theories refinedc
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-Q _build/default/examples/proofs/spinlock refinedc.examples.spinlock
-Q _build/default/examples/proofs/mpool_simpl refinedc.examples.mpool_simpl
-Q _build/default/examples/proofs/mpool refinedc.examples.mpool
-Q _build/default/examples/proofs/malloc1 refinedc.examples.malloc1
-Q _build/default/examples/proofs/mutable_map refinedc.examples.mutable_map
-Q _build/default/examples/proofs/latch refinedc.examples.latch
-Q _build/default/examples/proofs/simple_union refinedc.examples.simple_union
-Q _build/default/examples/proofs/queue refinedc.examples.queue
-Q _build/default/examples/proofs/reverse refinedc.examples.reverse
-Q _build/default/examples/proofs/btree refinedc.examples.btree
-Q _build/default/examples/proofs/lock refinedc.examples.lock
-Q _build/default/examples/proofs/flags refinedc.examples.flags
-Q _build/default/examples/proofs/shift refinedc.examples.shift
-Q _build/default/examples/proofs/paper_examples refinedc.examples.paper_examples
-Q _build/default/tutorial/proofs/binary_search_defs refinedc.tutorial.binary_search_defs
-Q _build/default/tutorial/proofs/t00_intro refinedc.tutorial.t00_intro
-Q _build/default/tutorial/proofs/t01_basic refinedc.tutorial.t01_basic
-Q _build/default/tutorial/proofs/t02_pointers refinedc.tutorial.t02_pointers
-Q _build/default/tutorial/proofs/t03_list refinedc.tutorial.t03_list
-Q _build/default/tutorial/proofs/t04_alloc refinedc.tutorial.t04_alloc
-Q _build/default/tutorial/proofs/t05_main refinedc.tutorial.t05_main
-Q _build/default/tutorial/proofs/t06_struct refinedc.tutorial.t06_struct
-Q _build/default/tutorial/proofs/t07_arrays refinedc.tutorial.t07_arrays
-Q _build/default/tutorial/proofs/t08_tree refinedc.tutorial.t08_tree
-Q _build/default/tutorial/proofs/t09_switch refinedc.tutorial.t09_switch
-Q _build/default/tutorial/proofs/t10_loops refinedc.tutorial.t10_loops
-Q _build/default/tutorial/proofs/t11_tree_set refinedc.tutorial.t11_tree_set
-Q _build/default/tutorial/adequacy refinedc.tutorial.adequacy
-Q _build/default/tutorial/proofs/quicksort_solution refinedc.tutorial.quicksort_solution
-Q _build/default/tutorial/proofs/quicksort_exercise refinedc.tutorial.quicksort_exercise
; Add project-wide flags here.
(env
(dev (flags :standard))
(release (flags :standard)))
(dev
(binaries (tools/coqc_timing.sh as coqc))
(flags :standard))
(release
(binaries (tools/coqc_timing.sh as coqc))
(flags :standard)))
(dirs frontend)
(install
(files FAQ.md ANNOTATIONS.md)
(section doc)
(package refinedc))
(lang dune 2.6)
(lang dune 2.7)
(name refinedc)
(using coq 0.2)
#include <refinedc.h>
#include <alloc.h>
#include "btree.h"
#include "alloc.h"
#include "../inc/refinedc.h"
//@rc::import btree_learn from refinedc.examples.btree (for proofs only)
......
......@@ -25,3 +25,6 @@ void *alloc_array(size_t size, size_t n);
[[rc::requires("{size * n < it_max size_t}", "{(8 | size)}")]]
[[rc::args("size @ int<size_t>", "n @ int<size_t>", "&own<array<{mk_layout size 3}, {replicate n (uninit (mk_layout size 3))}>>")]]
void free_array(size_t size, size_t n, void *ptr);
#define ALLOC(sz) alloc(sz)
#define FREE(sz,ptr) free(sz,ptr)
......@@ -6,6 +6,7 @@
#include <stdatomic.h>
//@rc::import latch_def from refinedc.examples.latch
//@rc::require refinedc.examples.latch
struct latch {
atomic_bool released;
......
......@@ -4,6 +4,7 @@
#include <stddef.h>
#include <stdatomic.h>
//@rc::require refinedc.examples.spinlock
//@rc::import spinlock_annot from refinedc.examples.spinlock (for code only)
//@rc::import spinlock_def from refinedc.examples.spinlock
//@rc::context `{!lockG Σ}
......
#include <stdbool.h>
#include "latch.h"
#include <latch.h>
void latch_wait(struct latch* latch) {
while(atomic_load(&latch->released) == (_Bool)false) {}
......
#include <stddef.h>
#include "../inc/refinedc.h"
#include "../inc/spinlock.h"
#include <refinedc.h>
#include <spinlock.h>
struct [[rc::refined_by("n1 : Z", "n2 : Z", "n3 : Z")]]
[[rc::exists("l: lock_id")]] lock_test {
......
// based on https://github.com/alastairreid/verifast-play/blob/master/src/malloc1.h
// and https://github.com/alastairreid/verifast-play/blob/master/src/malloc1.c
#include "stddef.h"
#include "stdint.h"
#include "../inc/refinedc.h"
#include <stddef.h>
#include <stdint.h>
#include <refinedc.h>
typedef struct [[rc::ptr_type("freelist_t:{(0 < len)%nat} @ optional<&own<...>>")]]
[[rc::parameters("entry_size: nat")]]
......
......@@ -17,8 +17,8 @@
#include <stddef.h>
#include <stdint.h>
#include <stdbool.h>
#include "../inc/refinedc.h"
#include "../inc/spinlock.h"
#include <refinedc.h>
#include <spinlock.h>
[[rc::parameters("p : loc", "size : loc", "align : nat")]]
[[rc::args("p @ ptr", "align @ int<size_t>", "size @ &own<uninit<size_t>>")]]
......
#define NULL (void*)0
#include "../inc/refinedc.h"
#include <refinedc.h>
//@rc::inlined Definition ENTRY_LAYOUT := {| ly_size := 16%nat; ly_align_log := 3%nat |}.
......
#include <stddef.h>
#include <stdint.h>
#include <stdbool.h>
#include "../inc/refinedc.h"
#include "../tutorial/alloc.h"
#include <refinedc.h>
#include <alloc.h>
// see https://github.com/splatlab/veribetrfs/blob/master/lib/DataStructures/MutableMapImpl.i.dfy
// and https://github.com/splatlab/veribetrfs/blob/master/lib/DataStructures/MutableMapModel.i.dfy
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment