Commit c806b383 authored by Michael Sammler's avatar Michael Sammler Committed by Rodolphe Lepigre
Browse files

Initial commit.


Co-authored-by: Rodolphe Lepigre's avatarRodolphe Lepigre <lepigre@mpi-sws.org>
parents
Pipeline #31754 passed with stage
in 14 minutes and 3 seconds
root = true
[*]
end_of_line = lf
insert_final_newline = true
[*.c]
indent_size = 2
*.v gitlab-language=coq
_build/
.merlin
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
\#*\#
.\#*
*~
*.bak
.coq-native/
build-dep/
Makefile.coq
.Makefile.coq.d
Makefile.coq.conf
_opam
/theories/examples/tutorial/tutorial
*.timing
image: ralfjung/opam-ci:opam2
stages:
- build
variables:
CPU_CORES: "10"
.template: &template
stage: build
tags:
- fp
script:
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
only:
- master@iris/refinedc
- /^ci/@iris/refinedc
except:
- triggers
- schedules
- api
## Build jobs
build-coq.8.11.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.11.2"
tags:
- fp-timing
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"
except:
only:
- triggers
- schedules
- api
This diff is collapsed.
The type system gets stuck on a sidecondition which contains an evar (i.e. protected (...)), what should I do?
--------------------------------------------------------------------------------------------------------------
Sometimes the automation gets stuck on a goal of the form `P ∧ ...`
where `P` is some pure proposition that contains evars (marked with
`protected`). When such a goal is reached, the system automatically
applies simplification rules in the hope of reducing `P` to an
equality `x = y` which can be solved by unifying `x` and `y`. If the
type system does not know how to further simplify `P`, but it is not
yet reduced to an unifiable equality, it gets stuck. In this case
there are two options:
1. Add additional simplification rules to further simplify `P` and
reduce it to an equality
2. Restructure the annotations such that it becomes easier for the
type system to figure out the instantiation
Currently RefinedC does not provide a way to give a manual
instantiation of existential quantifiers, but it can be added if
necessary.
See further points in this FAQ for explanation of these options.
How do I add additional simplification rules?
---------------------------------------------
The simplification rules can be extended by the user through special
typeclasses such as `SimplBoth`, `SimplAnd` and `SimplImpl`. See the
file `theories/typing/automation.v` for the definition and many
instances. Keep in mind the simplification rules should in general be
bi-implications to avoid accidentally turning a provable goal into an
unprovable.
How should I structure my annotations such that the automatic instantiation mechanism for evars works well?
-----------------------------------------------------------------------------------------------------------
Automatic instantiation of evars is a tricky problem. Some tools like
Verifast put syntactic restrictions on where evars can be introduced
to guarantee that they can always be automatically instantiated.
RefinedC does not enforce such restrictions and allows evars to be
basically used everywhere, but in turn it cannot give guarantees that
it will always be able to automatically figure out the right way to
instantiate these evars. Thus it is important to keep this problem in
mind when writing complex RefinedC annotations which involve evars. In
particular, one should think of the following:
1. Have a sense where evars will arise during type checking. The most
common causes for evars are the `∃ x. ty` type and `exists` clauses
of loop invariants. Sometimes (but not so often) the implicit
existential quantifier in a refinement type without a refinement
can also cause problems. Note that the first occurence of an evar
will usually instantiate it so later occurences don't have to be
considered.
2. Have a strategy how these evars should be instantiated. The best
(and most common) way to force the instantiation of an evar is to
directly use it as a refinement (we call such evars **good**
evars). For example, `∃ x. x @ int<size_t>` is a good evar and it
will be very easily instantiated since `subsume (n @ int<size_t>)
(?x @ int<size_t>)` gets reduced to `n = ?x` which instantiates
`?x` to `n`. `∃ x. (x + 1) @ int<size_t>` is not a good evar
because the unification problem will become the more tricky `n =
?x + 1` where one needs to use a simplification rule. In general,
**you should try to ensure that all your evars are good evars**.
This might require restructuring annotations and adding new evars or constraints.
For example, this is not a good evar:
```
∃ l. (length l) @ int<size_t>, {something which uses l}
```
and should be rewritten to
```
∃ x l. x @ int<size_t>, {something which uses l} & {length l = x}
```
If is is not possible to restructure the annotations to turn all
evars into good evars (this can happen e.g. arrays), it is still
important to *avoid partial instantion of evars* as this will
require simplification rules. For example, instead of
```
∃ l, array<size_t, l.*1 `at_type` int<size_t>>, {something which uses l}
```
one should write
```
∃ l1 l2, array<size_t, l1 `at_type` int<size_t>>, {something which uses zip l1 l2**
```
to avoid needing to partially instantiate `?l` to something like `zip l ?l2`.
The main take-away is the following: **Prefer many small evars with a
clear path to instantiation and linked with additional constraints to
few large evars which require complicated reasoning to figure out how
they should be instantiated.**
How do I debug the simplification mechanism?
--------------------------------------------
When adding such simplification rules, the system may still get stuck and it
may be useful to understand why. To this aim, you can step through the proof
manually until it gets stuck
```
repeat do_step; do_finish.
```
and then enable typeclass debugging.
```
Set Typeclasses Debug.
(*Set Typeclasses Debug Verbosity 2.*)
try do_step.
```
Another option is to apply the instances manually. To start with, use the
following tactic, and then apply the tactics mentionned in the debugging log.
```
notypeclasses refine (apply_simpl_and _ _ _ _ _)
```
Why does `ContainsProtected` contain an evar?
----------------------------------------------
Simplification rules will sometimes have an argument of the following form:
```
`{!ContainsProtected (some coq term)}
```
Do not forget the `!` here. Otherwise weird things happen.
Why don't I get as an hypothesis that an integer parameter is in range?
-----------------------------------------------------------------------
The hypotheses that the integer parameters are in range are only added to the
context on the first time the parameter is accessed. If such an hypothesis is
required prior to a first access, you can use the following macro to make it
available.
```c
rc_unfold_int(i);
```
All files in this development are distributed under the terms of the BSD
license, included below.
Copyright: refinedC developers and contributors
------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the copyright holder nor the names of its contributors
may be used to endorse or promote products derived from this software
without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# 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
.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
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# 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
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.
@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 --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
# 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 $@
# RefinedC verification framework
This repository contains the source code of **RefinedC**, a foundational
verification framework targeted at idiomatic C code. Thanks to its frontend
`rcgen` (written in OCaml), RefinedC automatically translates annotated C
source code into a deep embedding of our **Caesium** C semantics in Coq,
together with corresponding function specs expressed using ownership and
refinement types. After this generation step, the RefinedC automation (built
using our **Lithium** logic programming framework) takes over to prove the
user-defined function specs (which can encode full functional correctness),
leaving possible (pure) side-conditions to the user. To resolve such
side-conditions, the user can either extend the RefinedC automation or
discharge them directly using an interactive Coq proof. The RefiendC type
system itself is also extensible to allow expert users to add support for
specific programming idioms through new typing rules. Such additions must be
proven sound against the RefinedC semantic model, which is encoded in the
[Iris](https://gitlab.mpi-sws.org/iris/iris) framework for higher-order
concurrent separation logic.
## Building RefinedC
RefinedC is known to compile with Coq 8.11.2, but the frontend currently only
builds using OCaml 4.07.1. To avoid issues with other OCaml tools we highly
recommend building RefinedC against a specific Opam switch by following the
following instructions.
**Note:** All commands should be run inside the RefinedC repository.
**Note:** This was only tested on a 64-bits Linux machine. (Although it may
possibly work on MacOS as well.)
### Setting up [opam](https://opam.ocaml.org/doc/Install.html)
First, make sure that the OCaml package manager `opam` is installed. To do
so you can run the following command.
```bash
opam --version
```
If you already have `opam` version 2.0.0 or higher then you can skip to the
next section.
Otherwise, install `opam` using your usual package manager (checking that a
recent enough version is available), or run the following command (taken from
the [official installation guide](https://opam.ocaml.org/doc/Install.html)).
```bash
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
```
You can use the `BINDIR` environment variable to choose where the binary is
installed. There is a reasonable default but it needs root privileges.
### Setting up an [opam](https://opam.ocaml.org) switch
After having made sure that `opam` version 2.0.0 or higher is available, you
can create a "switch" (i.e., a virtual environment for a specific version of
the OCaml compiler and a specific set of installed libraries).
```bash
opam switch create --no-install . ocaml-base-compiler.4.07.1
```
**Note:** It may be necessary to run `eval $(opam env)` inside the RefinedC
directory to setup the switch in another terminal. This is not necessary in
the terminal used for creating the switch.
**Note:** The frontend requires a C compile (accessible through `cc`).
### Installing dependencies
The first thing to do is to set up repositories:
```bash
opam pin add -n -y cerberus git+https://github.com/rems-project/cerberus.git#5462d5bd84262f4248a6b9486151978c6dd9b362
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam pin add -n -y refinedc .
opam pin add -n -y refinedc-rcgen .
```
You can then install the dependencies:
```bash
opam install --deps-only refinedc refinedc-rcgen
```
**Note:** You can use `make update_deps` to install the right version of the
dependencies if the requirements have changed. This should typically done if
the version of Iris on which RefinedC relies has been updated.
### Building
To compile the Coq source files of RefinedC run:
```bash
# Replace 8 by the number of CPUs you can spare.
make -j8 all_without_examples
```
(Using `make` will compile all the examples as well and this takes a while.)
Although this is not necessary, you can compile the frontend using:
```bash
dune build
```
(The frontend is compiled if necessary when it is called.)
### Sourcing the commands
To finish setting up RefinedC, run the following command to extend your
current shell with two new commands `rcgen` and `refinedc`:
```bash
export PATH=$(pwd)/scripts:$PATH
```
The `rcgen` command is a simple wrapper around the frontend (use the `--help` option
to see how it is used). It can be used to generate the Coq files corresponding
to an annotated C source file.
The `refinedc` command is a higher-level wrapper around the frontend. When
called on a C source file of the repository, it generates the corresponding
Coq files (that need to be updated), and also compiles them.
**NOTE:** Although these commands will be available everywhere, they only
work under the RefinedC source tree.
## Verifying Programs using RefinedC
After having installed the dependencies and compiled the Coq development a
first time (with `make -j8 all_without_examples`), the typical way to interact
with the system is to simply edit some C file and to run the `refinedc`
command on it.
A good starting point to get a hang of the system is to explore the examples
of the `examples/tutorial` directory. Feel free to edit them, break them, and
also try to extend them with new functions. After having modified, say, file
`examples/tutorial/t1_basic.c`, run `refinedc examples/tutorial/t1_basic.c`
to check the full example.
If you want to start a new example from scratch, create a new directory under
`examples`, create the C file, and just call `refinedc` on it. Note that if
you need to define things in Coq you can do so in the directory, `refinedc`
will take care of the dependencies.
The RefinedC annotation syntax is documented in file `ANNOTATIONS.md`. Note
that you will need to add the following preprocessor directive to get access
to the RefinedC macros.
```c
#include "../inc/refinedc.h"
```
## Structure of the development
The structure of the development under `theories` is as follows:
- `lang`: Caesium formalization of C and Iris instantiation
- `lithium`: Lithium definition and interpreter
- `typing`: RefinedC type system
- `examples`: examples which use RefinedC
## Common Problems
- The build fails after removing a C function: manually delete the `*_proof.*`
files corresponding to that function in the directory where the source file
is placed.
- How do I generate all the Coq files at once? The easyest solution is to run
the command `for f in $(find examples -name "*.c"); rcgen "$f"`. Files that
do not need updating are left untouched (and as is their timestamp).
-Q theories refinedc
# We sometimes want to locally override notation (e.g. in proofmode/base.v,
# bi/embedding.v), and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Non-canonical projections (https://github.com/coq/coq/pull/10076) do not
# exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
#!/usr/bin/env python3
import sys
import re
import json
import subprocess
## TODO: distinguish between specification annotations and proof
## annotations (by checking if there is whitespace at the beginning of
## the line?)
## TODO: also count Coq code
annotation_re = re.compile(r"( ?)\[\[rc::([A-Za-z_]+)\s*\((.*?)\)\s*\]\]", re.DOTALL)
inline_re = re.compile("rc_([A-Za-z_]*)")
def print_stats(annots, loc):
annots_sum_with_spec = 0
for k,v in annots.items():
annots_sum_with_spec += v[0]
annots_sum_without_spec = 0
for k,v in annots.items():
annots_sum_without_spec += v[1]
loc -= annots_sum_with_spec + annots_sum_without_spec
print("with spec: {}/{} = {:.2f}".format(annots_sum_with_spec, loc, annots_sum_with_spec / loc))
print("without spec: {}/{} = {:.2f}".format(annots_sum_without_spec, loc, annots_sum_without_spec / loc))
total = {}
def parse_file(f):
per_file = {}
for match in annotation_re.finditer(f):
num_lines = len(match.group(3).strip().split('\n'))
idx = 0 if match.group(1) == "" else 1
# if "::" in match.group(2):
# if match.group(1) == "parameters":
# print(match.group(1), match.group(2))
per_file[match.group(2)] = per_file.get(match.group(2), [0,0])
per_file[match.group(2)][idx] += num_lines
for match in inline_re.finditer(f):
num_lines = 1
# if "::" in match.group(2):
# if match.group(1) == "parameters":
# print(match.group(1))
per_file[match.group(1)] = per_file.get(match.group(1), [0,0])
per_file[match.group(1)][1] += num_lines
return per_file
if len(sys.argv) < 2:
print("Usage: {} <files.c> ...".format(sys.argv[0]))
exit(1)
FILES=sys.argv[1:]
o = subprocess.check_output(["tokei", "--output=json", "--files"] + FILES)
inner = json.loads(o)["inner"]
if "CHeader" not in inner:
inner["CHeader"] = { "code": 0, "stats": []}
lines_total = inner["C"]["code"] + inner["CHeader"]["code"]
lines_per_file = {}
for s in inner["C"]["stats"] + inner["CHeader"]["stats"]:
lines_per_file[s["name"]] = s["code"]
for f in FILES:
print(f)
with open(f, 'r') as content_file:
per_file = parse_file(content_file.read())
print_stats(per_file, lines_per_file[f])
for k,v in per_file.items():
total[k] = total.get(k, [0,0])
total[k][0] += v[0]
total[k][1] += v[1]
print("total:")
print_stats(total, lines_total)
# print(json.dumps(total, indent=2))
; Add project-wide flags here.
(env
(dev (flags :standard))
(release (flags :standard)))
(dirs frontend)
(lang dune 2.6)
(name refinedc)
This diff is collapsed.
(** Entry point of the Cerberus typed Ail AST. *)
type typed_ail =
Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.ail_program
(** [translate fname ail] translates the Cerberus typed Ail AST [ast] into our
Coq AST. The file name [fname] should correspond to the C source file that
lead to generating [ail]. In case of error an error message is displayed,
and the program fails with error code [-1]. Note that any invalid RefinedC
annotation is ignored (although a warning is displayed on [stderr]) but an
error will be triggered if one attempts to generate a spec file. *)
val translate : string -> typed_ail -> Coq_ast.t
open Cerb_frontend
open Cerb_backend
open Pipeline
let (>>=) = Exception.except_bind
let return = Exception.except_return
let io : Pipeline.io_helpers =
let pass_message = let ref = ref 0 in fun str ->
Debug_ocaml.print_success (Printf.sprintf "%i. %s" !ref str);
incr ref; return ()
in
let set_progress _ = return () in
let run_pp opts doc = run_pp opts doc; return () in
let print_endline str = print_endline str; return () in
let print_debug n mk_str = Debug_ocaml.print_debug n [] mk_str; return () in
let warn mk_str = Debug_ocaml.warn [] mk_str; return () in
{pass_message ; set_progress ; run_pp ; print_endline ; print_debug ; warn}