Commit 10cc836a authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Frontend uses dune for RefinedC projects.

parent 9e1211df
-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
......
......@@ -3,4 +3,7 @@
(dev (flags :standard))
(release (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)
......@@ -2,6 +2,10 @@ open Cerb_frontend
open Cerb_backend
open Pipeline
type cpp_config =
{ cpp_include : string list
; cpp_nostdinc : bool }
let (>>=) = Exception.except_bind
let return = Exception.except_return
......@@ -62,10 +66,12 @@ let source_file_check filename =
if not (Filename.check_suffix filename ".c") then
Panic.panic_no_pos "File [%s] does not have the [.c] extension." filename
let c_file_to_ail cpp_includes cpp_nostd filename =
let c_file_to_ail config fname =
let open Exception in
source_file_check filename;
match frontend (cpp_cmd cpp_includes cpp_nostd) filename with
let cpp_includes = config.cpp_include in
let cpp_nostd = config.cpp_nostdinc in
source_file_check fname;
match frontend (cpp_cmd cpp_includes cpp_nostd) fname with
| Result(_, Some(ast), _) -> ast
| Result(_, None , _) ->
Panic.panic_no_pos "Unexpected frontend error."
......@@ -80,11 +86,27 @@ let c_file_to_ail cpp_includes cpp_nostd filename =
in
Panic.panic loc "Frontend error.\n%s\n\027[0m%s%!" err pos
let cpp_lines cpp_includes cpp_nostd filename =
source_file_check filename;
let cpp_lines config fname =
let cpp_includes = config.cpp_include in
let cpp_nostd = config.cpp_nostdinc in
source_file_check fname;
let str =
match run_cpp (cpp_cmd cpp_includes cpp_nostd) filename with
match run_cpp (cpp_cmd cpp_includes cpp_nostd) fname with
| Result(str) -> str
| Exception(_) -> Panic.panic_no_pos "Failed due to preprocessor error."
in
String.split_on_char '\n' str
let print_ail : Ail_to_coq.typed_ail -> unit = fun ast ->
match io.run_pp None (Pp_ail_ast.pp_program true false ast) with
| Result(_) -> ()
| Exception((loc,err)) ->
match err with
| CPP(_) -> Panic.panic_no_pos "Failed due to preprocessor error."
| _ ->
let err = Pp_errors.short_message err in
let (_, pos) =
try Location_ocaml.head_pos_of_location loc with Invalid_argument(_) ->
("", "(Cerberus position bug)")
in
Panic.panic loc "Frontend error.\n%s\n\027[0m%s%!" err pos
(** [c_file_to_ail includes nostdinc fname] uses Cerberus to preprocess, parse
and also type-check the C source file [fname]. All the directory in of the
[includes] list are passed to the C preprocessor through the ["-I"] option
(they are hence searched for header files). If [nostdinc] then the default
system directories are not searched for header files. In case of error, an
a message is displayed and the program exits with error code [-1]. *)
val c_file_to_ail : string list -> bool -> string -> Ail_to_coq.typed_ail
(** Preprocessor configuration. *)
type cpp_config =
{ cpp_include : string list (** Directories in the search path. *)
; cpp_nostdinc : bool (** Do not search standard lib C dirs. *) }
(** [cpp_lines includes nostdinc fname] preprocesses the C source file [fname]
using Cerberus, and returns the list of the lines of the output. The flags
[includes] and [nostdinc] have the same effect as for [c_file_to_ail]. *)
val cpp_lines : string list -> bool -> string -> string list
(** [c_file_to_ail config fname] uses Cerberus to preprocess, parse, elaborate
and type-check the C source file [fname]. The given configuration [config]
is used to alter the behaviour of the preprocessor. In case of an error, a
message is displayed and the program exits with error code [-1]. *)
val c_file_to_ail : cpp_config -> string -> Ail_to_coq.typed_ail
(** [cpp_lines config fname] preprocesses the C file [fname] with Cerberus and
returns the obtained list of lines. The configuration [config] can be used
to alter the behaviour of the preprocessor. In case of an error, a message
is displayed and the program exits with error code [-1]. *)
val cpp_lines : cpp_config -> string -> string list
(** [print_ail ast] outputs the given Ail [ast] to standard output. *)
val print_ail : Ail_to_coq.typed_ail -> unit
......@@ -734,18 +734,13 @@ let collect_invs : func_def -> (string * loop_annot) list = fun def ->
let pp_spec : string -> import list -> string list -> typedef list ->
string list -> Coq_ast.t pp =
fun import_path imports inlined typedefs ctxt ff ast ->
(* Stuff for import of the code. *)
let basename =
let name = Filename.basename ast.source_file in
try Filename.chop_extension name with Invalid_argument(_) -> name
in
(* Formatting utilities. *)
let pp fmt = Format.fprintf ff fmt in
(* Printing some header. *)
pp "@[<v 0>From refinedc.typing Require Import typing.@;";
pp "From %s Require Import %s_code.@;" import_path basename;
pp "From %s Require Import code.@;" import_path;
List.iter (pp_import ff) imports;
pp "Set Default Proof Using \"Type\".@;@;";
......@@ -1072,16 +1067,10 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
| _ -> imports
in
(* Stuff for import of the code. *)
let basename =
let name = Filename.basename ast.source_file in
try Filename.chop_extension name with Invalid_argument(_) -> name
in
(* Printing some header. *)
pp "@[<v 0>From refinedc.typing Require Import typing.@;";
pp "From %s Require Import %s_code.@;" import_path basename;
pp "From %s Require Import %s_spec.@;" import_path basename;
pp "From %s Require Import code.@;" import_path;
pp "From %s Require Import spec.@;" import_path;
List.iter (pp_import ff) imports;
pp "Set Default Proof Using \"Type\".@;@;";
......
(executable
(name main)
(public_name rcgen)
(package refinedc-rcgen)
(public_name refinedc)
(package refinedc)
(preprocess (per_module ((action (run pa_ocaml %{input-file})) rc_annot)))
(flags (:standard -w -27 -I +../cerberus/frontend)) ; FIXME crazy hack.
(foreign_stubs (language c) (names stubs))
(libraries cmdliner str unix earley.core cerberus.frontend
cerberus.backend_common cerberus.mem.concrete cerberus.util))
(rule
(targets version.ml)
(action
(with-stdout-to version.ml
(run ocaml unix.cma %{dep:tools/gen_version.ml})))
(mode fallback))
......@@ -59,6 +59,35 @@ module Filename =
[path] is invalid (i.e., it does not describe an existing file), then
the exception [Invalid_argument] is raised. *)
external realpath : string -> string = "c_realpath"
(** [iter_files ?ignored_dirs dir f] recursively traverses directory [dir]
and calls function [f] on each file, using as first argument a boolean
indicating whether the file is a directory, and as second arugment the
full path to the file. The traversal ignores directories whose name is
contained in [ignored_dirs], as well as their contents. *)
let iter_files : ?ignored_dirs:string list -> string
-> (bool -> string -> unit) -> unit = fun ?(ignored_dirs=[]) dir f ->
let rec iter dirs =
match dirs with
| [] -> ()
| (dir, base) :: dirs ->
let file = Filename.concat dir base in
let is_dir = Sys.is_directory file in
(* Ignore if necessary. *)
match is_dir && List.mem base ignored_dirs with
| true -> iter dirs
| false ->
(* Run the action on the current file. *)
f is_dir file;
(* Compute remaining files. *)
if is_dir then
let files = Sys.readdir file in
let fn name dirs = (file, name) :: dirs in
iter (Array.fold_right fn files dirs)
else
iter dirs
in
iter [(Filename.dirname dir, Filename.basename dir)]
end
module SMap = Map.Make(String)
......@@ -122,9 +151,38 @@ module String =
with Exit -> false
end
(** [outut_lines oc ls] prints the lines [ls] to the output channel [oc] while
inserting newlines according to [String.split_on_char]. *)
(** [outut_lines oc ls] prints the lines [ls] to the output channel [oc]. Note
that a newline character is added at the end of each line. *)
let output_lines : out_channel -> string list -> unit = fun oc ls ->
match ls with
| [] -> ()
| l :: ls -> output_string oc l; List.iter (Printf.fprintf oc "\n%s") ls
List.iter (Printf.fprintf oc "%s\n") ls
(** [write_file fname ls] writes the lines [ls] to file [fname]. All lines are
terminated with a newline character. *)
let write_file : string -> string list -> unit = fun fname ls ->
let oc = open_out fname in
output_lines oc ls; close_out oc
(** [append_file fname ls] writes the lines [ls] at the end of file [fname]. A
newline terminates each inserted lines. The file must exist. *)
let append_file : string -> string list -> unit = fun fname ls ->
let oc = open_out_gen [Open_append] 0 fname in
output_lines oc ls; close_out oc
(** [read_file fname] returns the list of the lines of file [fname]. Note that
the trailing newlines are removed. *)
let read_file : string -> string list = fun fname ->
let ic = open_in fname in
let lines = ref [] in
try
while true do lines := input_line ic :: !lines done;
assert false (* Unreachable. *)
with End_of_file -> close_in ic; List.rev !lines
(** Short name for a standard formatter with continuation. *)
type ('a,'b) koutfmt = ('a, Format.formatter, unit, unit, unit, 'b) format6
(** [invalid_arg fmt ...] raises [Invalid_argument] with the given message. It
can be formed using the standard formatter syntax. *)
let invalid_arg : ('a, 'b) koutfmt -> 'a = fun fmt ->
let cont _ = invalid_arg (Format.flush_str_formatter ()) in
Format.kfprintf cont Format.str_formatter fmt
This diff is collapsed.
let version =
(* Trick to check whether the watermark has been substituted. *)
if "%%VERSION%%" <> "%%" ^ "VERSION%%" then "%%VERSION%%" else
(* If not, we fallback to git version. *)
let cmd = "git describe --dirty --always" in
let (oc, ic, ec) = Unix.open_process_full cmd (Unix.environment ()) in
let version =
try Printf.sprintf "dev-%s" (input_line oc)
with End_of_file -> "unknown"
in
match Unix.close_process_full (oc, ic, ec) with
| Unix.WEXITED(0) -> version
| _ -> "unknown"
let _ =
let line fmt = Printf.printf (fmt ^^ "\n%!") in
line "(** Version informations. *)";
line "";
line "(** [version] gives a version description. *)";
line "let version : string = \"%s\"" version
(install
(files (refinedc.h as include/refinedc.h))
(section lib)
(package refinedc))
#ifndef REFINEDC_H
#define REFINEDC_H
#define rc_unfold(e) \
_Pragma("GCC diagnostic push") \
_Pragma("GCC diagnostic ignored \"-Wunused-value\"") \
&(e); \
_Pragma("GCC diagnostic pop")
#define rc_unfold_int(e) \
_Pragma("GCC diagnostic push") \
_Pragma("GCC diagnostic ignored \"-Wunused-value\"") \
e + 0; \
_Pragma("GCC diagnostic pop")
#define rc_annot(e, ...) \
_Pragma("GCC diagnostic push") \
_Pragma("GCC diagnostic ignored \"-Wunused-value\"") \
[[rc::annot(__VA_ARGS__)]] &(e); \
_Pragma("GCC diagnostic pop")
#define rc_unlock(e) rc_annot(e, "UnlockA")
#define rc_to_uninit(e) rc_annot(e, "ToUninit")
#define rc_uninit_strengthen_align(e) rc_annot(e, "UninitStrengthenAlign")
#define rc_stop(e) rc_annot(e, "StopAnnot")
#define rc_share(e) rc_annot(e, "ShareAnnot")
#define rc_unfold_once(e) rc_annot(e, "UnfoldOnceAnnot")
#define rc_learn(e) rc_annot(e, "LearnAnnot")
#ifdef RC_ENABLE_FOCUS
#define RC_FOCUS ,rc::trust_me
#define RC_FOCUS_X
#else
#define RC_FOCUS
#define RC_FOCUS_X
#endif
#endif
opam-version: "2.0"
synopsis: "The RefinedC frontend"
description: """
This tool translates annotated C code into a deep embedding of the Ceasium C
semantics in Coq. Function specifications are checked againinst the RefiendC
refinement type system, and Coq proofs are automatically generated.
"""
maintainer: ["Rodolphe Lepigre <lepigre@mpi-sws.org>"]
authors: ["Rodolphe Lepigre" "Michael Sammler" "Kayvan Memarian"]
license: "BSD"
homepage: "https://plv.mpi-sws.org/refinedc"
bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/-/issues"
depends: [
"dune" {>= "2.0.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
"earley" {= "2.0.0"}
]
build: [
["dune" "subst"] {pinned}
[make "prelude-src"]
["dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
dev-repo: "git+https://github.com/rems-project/cerberus-private.git"
opam-version: "2.0"
name: "coq-refinedc"
maintainer: "Michael Sammler <msammler@mpi-sws.org>"
authors: "Michael Sammler"
name: "refinedc"
synopsis: "RefinedC verification framework"
description: """
RefinedC is a framework for verifying idiomatic, low-level C code using a
combination of refinement types and ownership types.
"""
license: "BSD"
homepage: "https://gitlab.mpi-sws.org/iris/refinedc"
maintainer: ["Michael Sammler <msammler@mpi-sws.org>"
"Rodolphe Lepigre <lepigre@mpi-sws.org>"]
authors: ["Michael Sammler" "Rodolphe Lepigre" "Kayvan Memarian"]
homepage: "https://plv.mpi-sws.org/refinedc"
bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
synopsis: "RefinedC"
description: """
RefinedC: Framework for verifying low-level code using refinement types and ownership types.
"""
depends: [
"coq" { (>= "8.11.0" & < "8.12~") | (= "dev") }
"coq-iris" { (= "dev.2020-09-29.7.19ba2bc0") | (= "dev") }
"dune" {>= "2.0.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
"earley" {= "2.0.0"}
]
build: [make "-j%{jobs}%"]
install: [make "install"]
build: [
["dune" "subst"] {pinned}
["dune" "build" "-p" name "-j" jobs]
]
(coq.theory
(name refinedc.lang)
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Core language"))
(coq.theory
(name refinedc.lithium)
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Lithium")
(theories refinedc.lang))
(coq.theory
(name refinedc.typing.automation)
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Lithium")
(theories refinedc.lang refinedc.typing refinedc.lithium))
(coq.theory
(name refinedc.typing)
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Lithium")
(theories refinedc.lang refinedc.lithium))
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