Commit c8e540dd authored by Lennard Gäher's avatar Lennard Gäher
Browse files

Merge remote-tracking branch 'origin/master' into rr

parents 9fc45564 13f33068
......@@ -30,11 +30,10 @@ variables:
- api
## Build jobs
# TODO: remove z3 version 4.8.9-1 once https://github.com/Z3Prover/z3/issues/5405 and https://github.com/rems-project/cerberus/issues/180 are fixed
build-coq.8.13.2-timing:
<<: *template
variables:
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
DENY_WARNINGS: "1"
OPAM_PKG: "1"
only:
......@@ -47,7 +46,7 @@ build-coq.8.13.2-timing:
build-coq.8.13.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
OPAM_PINS: "coq version 8.13.2 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
DENY_WARNINGS: "1"
only:
- /^ci/@iris/refinedc
......@@ -55,7 +54,7 @@ build-coq.8.13.2:
trigger-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.13.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/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
OPAM_PINS: "coq version 8.13.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/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5"
except:
only:
- triggers
......
......@@ -9,7 +9,7 @@ RefinedC to get at working setup suitable for development of RefinedC
and building the examples in this repository:
```
opam switch create . ocaml-base-compiler.4.11.1
opam switch create . ocaml-base-compiler.4.11.1 --no-install
sudo apt-get install libmpfr-dev # Implicit Cerberus dependency.
opam repo add coq-released "https://coq.inria.fr/opam/released"
opam repo add iris-dev "https://gitlab.mpi-sws.org/iris/opam.git"
......
......@@ -20,7 +20,7 @@
#-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/t02_evars refinedc.tutorial.t02_evars
#-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
......@@ -53,3 +53,6 @@
#-Q _build/default/examples/proofs/tagged_ptr refinedc.examples.tagged_ptr
#-Q _build/default/examples/proofs/ocaml_runtime refinedc.examples.ocaml_runtime
#-Q _build/default/linux/casestudies/proofs/page_alloc_find_buddy refinedc.linux.casestudies.page_alloc_find_buddy
#-Q _build/default/examples/proofs/pointers refinedc.examples.pointers
#-Q _build/default/linux/casestudies/proofs/pgtable refinedc.linux.casestudies.pgtable
#-Q _build/default/tutorial/proofs/lithium refinedc.tutorial.lithium
......@@ -9,10 +9,10 @@ typedef bool (*comp_fn)(void *, void *);
[[rc::parameters("R : {Z → Z → Prop}", "ls : {list Z}", "x : Z", "p : loc", "ty : {Z → type}", "px : loc")]]
[[rc::args("function_ptr<{fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝}>",
"p @ &own<array<void*, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<i32>", "px @ &own<{ty x}>")]]
"p @ &own<array<void*, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<size_t>", "px @ &own<{ty x}>")]]
[[rc::requires("{StronglySorted R ls}", "{Transitive R}")]]
[[rc::exists("n : nat")]]
[[rc::returns("n @ int<i32>")]]
[[rc::returns("n @ int<size_t>")]]
[[rc::ensures("{∀ i y, (i < n)%nat → ls !! i = Some y → R y x}",
"{∀ i y, (n ≤ i)%nat → ls !! i = Some y → ¬ R y x}")]]
[[rc::ensures("own p : array<void*, {(fun x => &own (ty x) : type) <$> ls}>")]]
......@@ -20,15 +20,15 @@ typedef bool (*comp_fn)(void *, void *);
[[rc::tactics("all: try by [revert select (∀ i j, _ → _ → ¬ R _ _); apply; [| done];solve_goal].")]]
[[rc::tactics("all: try by apply: binary_search_cond_1; [solve_goal|..]; solve_goal.")]]
[[rc::tactics("all: try by apply: binary_search_cond_2; [solve_goal|..]; solve_goal.")]]
int binary_search(comp_fn comp, void **xs, int n, void *x) {
int l = 0, r = n;
size_t binary_search(comp_fn comp, void **xs, size_t n, void *x) {
size_t l = 0, r = n;
[[rc::exists("vl : nat", "vr : nat")]]
[[rc::inv_vars("l : vl @ int<i32>", "r : vr @ int<i32>")]]
[[rc::inv_vars("l : vl @ int<size_t>", "r : vr @ int<size_t>")]]
[[rc::constraints("{vl <= vr}", "{vr <= length ls}")]]
[[rc::constraints("{∀ i y, (i < vl)%nat → ls !! i = Some y → R y x}",
"{∀ i y, (vr ≤ i)%nat → ls !! i = Some y → ¬ R y x}")]]
while(l < r) {
int k = l + (r - l) / 2;
size_t k = l + (r - l) / 2;
if (comp(xs[k], x)) {
l = k + 1;
} else {
......
......@@ -55,6 +55,7 @@ void mpool_put(struct mpool *p, void *ptr) {
void* e1, *e2;
[[rc::requires("global e1 : uninit<ENTRY_LAYOUT>")]]
[[rc::requires("global e2 : uninit<ENTRY_LAYOUT>")]]
[[rc::returns("int<i32>")]]
int main(void) {
struct mpool p;
void * p1, *p2;
......
......@@ -2,10 +2,6 @@
#include <stdbool.h>
#include <refinedc.h>
/**
THIS FILE IS WORK IN PROGRESS! PLEASE CONTINUE TO THE NEXT FILE!
*/
[[rc::parameters("p : loc", "n : Z")]]
[[rc::args("p @ &own<n @ int<i32>>")]]
[[rc::returns("n @ int<i32>")]]
......
......@@ -12,9 +12,15 @@ Section type.
l `has_layout_loc` struct_latch
l LATCH_INIT ={E}= l ◁ₗ{Shr} P @ latch.
Proof.
iIntros (? ?) "Hl".
iApply ty_share => //. unshelve iApply (@ty_ref with "[] Hl").
{ apply _. } { apply: (UntypedOp struct_latch). } { apply: MCNone. } { solve_goal. } { done. }
rewrite /ty_own_val/=. repeat iSplit => //. rewrite /ty_own_val/=/ty_own_val/=. iSplit => //. by iExists false.
iIntros (? ?) "Hl". iApply ty_share => //.
unshelve iApply (@ty_ref with "[] Hl").
{ apply _. }
{ apply: (UntypedOp struct_latch). }
{ apply: MCNone. }
{ solve_goal. }
{ done. }
rewrite /ty_own_val/=. repeat iSplit => //.
rewrite /ty_own_val /= /ty_own_val /=. iSplit => //.
iExists false. iSplit; last done. by iExists _.
Qed.
End type.
......@@ -21,7 +21,7 @@ Section type.
repeat liRStep; liShow.
liInst Hevar γ.
repeat liRStep; liShow.
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
Qed.
End type.
......@@ -92,3 +92,59 @@ void test_logical(){
if(INT_MAX) { assert(1); } else { assert(0); }
assert(UINT_MAX);
}
[[rc::returns("void")]]
void test_not_ptr(){
int i;
int *pi = &i;
if(!pi){
assert(0);
}
if(pi){
assert(1);
} else {
assert(0);
}
assert(pi);
void *p = NULL;
if(p){
assert(0);
}
if(!p){
assert(1);
} else {
assert(0);
}
assert(!p);
}
[[rc::returns("{0} @ int<i32>")]]
int main(){
// Check that [return 0] is inserted corectly.
}
struct test { int a; };
[[rc::exists("n : Z")]]
[[rc::returns("struct<struct_test, n @ int<i32>>")]]
[[rc::ensures("{n = 1}")]]
struct test test_struct_return() {
struct test test;
test.a = 1;
return test;
}
typedef void (*test_fn)(void);
[[rc::parameters("spec : {unit → fn_params}")]]
[[rc::args("function_ptr<spec>")]]
[[rc::returns("function_ptr<spec>")]]
test_fn test_fn_params(test_fn f) {
return f;
}
......@@ -177,7 +177,6 @@ let is_const_0 (AilSyntax.AnnotatedExpression(_, _, _, e)) =
end
| _ -> false
type 'a macro_annot_arg =
| MacroString of string
| MacroExpr of ail_expr
......@@ -911,6 +910,15 @@ let k_break = k_gen (fun k -> k.k_break )
let k_continue = k_gen (fun k -> k.k_continue)
let k_final = k_gen (fun k -> k.k_final )
let k_init : op_type option -> bool -> k_data list = fun ret_ty is_main ->
let ret_v =
match ret_ty with
(* Insert [return 0] in case of main with int type. *)
| Some(OpInt(ItI32(true))) when is_main -> Int("0", ItI32(true))
| _ -> Void
in
k_push_final (noloc (Return(noloc (Val(ret_v))))) []
let rec k_pop_cases : k_data list -> k_data list = fun l ->
match l with
| [] -> []
......@@ -941,8 +949,7 @@ let k_stack_print : out_channel -> k_data list -> unit = fun oc l ->
List.iter print_data l;
Printf.fprintf oc "\n%!"
let translate_block stmts blocks ret_ty =
let translate_block stmts blocks ret_ty is_main =
let translate_bool_expr then_goto else_goto e =
let ot = op_type_of_tc (loc_of e) (tc_of e) in
let e = translate_expr false None e in
......@@ -1278,8 +1285,7 @@ let translate_block stmts blocks ret_ty =
if not !attrs_used then warn_ignored_attrs (Some(s)) attrs;
res
in
let initial_ks = k_push_final (noloc (Return(noloc (Val(Void))))) [] in
trans [] [] initial_ks stmts blocks
trans [] [] (k_init ret_ty is_main) stmts blocks
(** [translate fname ail] translates typed Ail AST to Coq AST. *)
let translate : string -> typed_ail -> Coq_ast.t = fun source_file ail ->
......@@ -1402,21 +1408,20 @@ let translate : string -> typed_ail -> Coq_ast.t = fun source_file ail ->
in
List.mapi fn args_decl
in
let _ =
(* Collection top level local variables. *)
let (bindings, stmts) =
match stmt with
| AilSblock(bindings, _) -> insert_bindings bindings
| _ -> not_impl loc "Body not a block."
| AilSblock(bindings, stmts) -> (bindings, stmts)
| _ -> not_impl loc "Body not a block."
in
(* Collection top level local variables. *)
insert_bindings bindings;
let func_init = fresh_block_id () in
let func_blocks =
let stmts =
match stmt with
| AilSblock(_, stmts) -> stmts
| _ -> not_impl loc "Body not a block."
in
let ret_ty = op_type_opt Location_ocaml.unknown ret_ty in
let (stmt, blocks) = translate_block stmts SMap.empty ret_ty in
let (stmt, blocks) =
let is_main = func_name = "main" in
translate_block stmts SMap.empty ret_ty is_main
in
add_block func_init stmt blocks
in
let func_vars = collect_bindings () in
......
open Extra
type member = string
let member_of_string : string -> member = fun s ->
let invalid r =
let f = "Name \"%s\" is invalid as a Coq path member: it " ^^ r ^^ "." in
invalid_arg f s
in
(* Empty string is invalid. *)
if String.length s = 0 then invalid "is empty";
(* Only accept characters, digits and underscores. *)
let check_char c =
match c with
| 'a'..'z' | 'A'..'Z' | '0'..'9' | '_' -> ()
| _ when Char.printable_ascii c ->
invalid "contains '%c'" c;
| _ ->
invalid "uses non-printable ASCII characters" c;
in
String.iter check_char s;
(* Should not start with a letter. *)
match s.[0] with
| 'a'..'z' | 'A'..'Z' -> s
| c -> invalid "starts with '%c'" c
let fixup_string_member : string -> string option = fun s ->
(* Remove non-ASCII characters. *)
let s = Ubase.from_utf8 ~malformed:"" ~strip:"" s in
(* Use underscores for invalid characters. *)
let fn c =
match c with
| 'a'..'z' | 'A'..'Z' | '0'..'9' -> c
| _ -> '_'
in
let s = String.map fn s in
(* Remove leading underscores. *)
let s = String.trim_leading '_' s in
(* Check non-empty. *)
if String.length s = 0 then None else
(* Check starts with letter. *)
match s.[0] with
| 'a'..'z' | 'A'..'Z' -> Some(s)
| _ -> None
type path = Path of member * member list
type t = path
let path_of_members : member list -> path = fun ms ->
match ms with
| [] -> invalid_arg "Coq_path.path_of_members requires a non-empty list."
| m::ms -> Path(m, ms)
let path_of_string : string -> path = fun s ->
let members = String.split_on_char '.' s in
try
match List.map member_of_string members with
| m :: ms -> Path(m, ms)
| [] -> invalid_arg "The empty module path is forbidden."
with Invalid_argument(msg) ->
invalid_arg "String \"%s\" is not a valid Coq module path.\n%s" s msg
let fixup_string_path : string -> string option = fun s ->
let rec build ms acc =
match (ms, acc) with
| ([] , []) -> None
| ([] , _ ) -> Some(String.concat "." (List.rev acc))
| (m :: ms, _ ) ->
match fixup_string_member m with
| None -> None
| Some(m) -> build ms (m :: acc)
in
build (String.split_on_char '.' s) []
type suffix = member list
let append : t -> suffix -> t = fun (Path(m, ms)) suff -> Path(m, ms @ suff)
let to_string : path -> string = fun (Path(m, ms)) ->
String.concat "." (m :: ms)
let pp : path pp = fun ff path ->
Format.pp_print_string ff (to_string path)
(** Management of Coq module paths.
Coq modules path identifiers and file names are restricted to be valid Coq
identifiers, with further restrictions (only ASCII letters, digits and the
underscore symbol). This module provides types that encapsulate components
of Coq module paths into abstract types, to enforces that they are valid.
Useful links:
- https://coq.inria.fr/refman/practical-tools/coq-commands.html
- https://coq.inria.fr/refman/language/core/basic.html#lexical-conventions
*)
open Extra
(** Coq module path member. *)
type member
(** [member_of_string s] converts string [s] into a Coq module path member. If
the given string does not correspond to a valid path member, the exception
[Invalid_argument] is raised with an explanatory error message formed of a
full sentence, to be displayed directly (and ideally on its own line). *)
val member_of_string : string -> member
(** [fixup_string_member s] tries to build a resonable (valid) Coq module path
member name from the string [s]. This is done by replacing diacritic marks
by corresponding ASCII sequences if applicable, and by using ['_'] instead
of invalid characters like ['-']. If a result string is produced, applying
the [member_of_string] function to it is guaranteed to succeed. *)
val fixup_string_member : string -> string option
(** Coq module path. *)
type path
(** Short synonym for [path]. *)
type t = path
(** [path_of_members ms] turns the (non-empty) list of members [ms] into a Coq
module path. If [ms] is empty then [Invalid_argument] is raised. *)
val path_of_members : member list -> path
(** [path_of_string s] parses string [s] into a Coq module path. In case where
[s] does not denote a valid module path, then exception [Invalid_argument]
is raised with a full, explanatory error message. *)
val path_of_string : string -> path
(** [fixup_string_path s] is similar to [fixup_string_member] but for full Coq
module paths. If a result string is produced, applying [path_of_string] to
it it guaranteed to succeed (no exception is produced). *)
val fixup_string_path : string -> string option
(** Coq path suffix. *)
type suffix = member list
(** [append path suff] extends the Coq path [path] with suffix [suff]. *)
val append : t -> suffix -> t
(** [to_string path] converts the path [path] into a string directly usable as
the Coq representation of the path. *)
val to_string : path -> string
(** [pp ff path] prints the string representation of [path] (as obtained using
[to_string]) to the [ff] formatter. *)
val pp : path pp
......@@ -158,30 +158,43 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
| BinOp(op,ty1,ty2,e1,e2) ->
begin
match (ty1, ty2, op) with
(* Comma operator. *)
| (_ , _ , CommaOp) ->
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
(* Pointer offset operations. *)
| (OpPtr(l), OpInt(_), AddOp ) ->
pp "(%a) at_offset{%a, PtrOp, %a} (%a)" pp_expr e1
(pp_layout false) l pp_op_type ty2 pp_expr e2
| (OpPtr(l), OpInt(_), SubOp ) ->
pp "(%a) at_neg_offset{%a, PtrOp, %a} (%a)" pp_expr e1
(pp_layout false) l pp_op_type ty2 pp_expr e2
(* Pointer difference. *)
| (OpPtr(l1), OpPtr(l2), SubOp) ->
pp "(%a) sub_ptr{%a, PtrOp, PtrOp} (%a)" pp_expr e1
(pp_layout false) l1 pp_expr e2
| (OpPtr(_), OpInt(_), _ ) ->
panic_no_pos "Binop [%a] not supported on pointers."
pp_bin_op op
(* Pointer compared to 0 (Cerberus rejects non-0 integer values). *)
| (OpInt(_) , OpPtr(l) , (EqOp | NeOp)) ->
let e1 = {e1 with elt = UnOp(CastOp(ty2), ty1, e1)} in
pp "(%a) %a{PtrOp, PtrOp, i32} (%a)" pp_expr e1
pp_bin_op op pp_expr e2
| (OpPtr(l) , OpInt(_) , (EqOp | NeOp)) ->
let e2 = {e2 with elt = UnOp(CastOp(ty1), ty2, e2)} in
pp "(%a) %a{PtrOp, PtrOp, i32} (%a)" pp_expr e1
pp_bin_op op pp_expr e2
(* Invalid operations mixing an integer and a pointer. *)
| (OpPtr(_), OpInt(_), _ )
| (OpInt(_), OpPtr(_), _ ) ->
panic_no_pos "Wrong ordering of integer pointer binop [%a]."
pp_bin_op op
| _ when is_bool_result_op op ->
pp "(%a) %a{%a, %a, i32} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
let loc = Location.to_cerb_loc e.loc in
panic loc "Invalid use of binary operation [%a]." pp_bin_op op
(* All other operations are defined. *)
| _ ->
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
if is_bool_result_op op then
pp "(%a) %a{%a, %a, i32} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
else
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
end
| Deref(atomic,ty,e) ->
if atomic then
......@@ -795,9 +808,9 @@ let collect_invs : func_def -> (string * loop_annot) list = fun def ->
in
SMap.fold fn def.func_blocks []
let pp_spec : string -> import list -> inlined_code ->
let pp_spec : Coq_path.t -> import list -> inlined_code ->
typedef list -> string list -> Coq_ast.t pp =
fun import_path imports inlined typedefs ctxt ff ast ->
fun coq_path imports inlined typedefs ctxt ff ast ->
(* Formatting utilities. *)
let pp fmt = Format.fprintf ff fmt in
......@@ -817,7 +830,7 @@ let pp_spec : string -> import list -> inlined_code ->
(* Printing some header. *)
pp "@[<v 0>From refinedc.typing Require Import typing.@;";
pp "From %s Require Import generated_code.@;" import_path;
pp "From %a Require Import generated_code.@;" Coq_path.pp coq_path;
List.iter (pp_import ff) imports;
pp "Set Default Proof Using \"Type\".\n";
......@@ -1137,8 +1150,9 @@ let pp_spec : string -> import list -> inlined_code ->
pp_inlined false (Some "final") inlined.ic_final;
pp "@]"
let pp_proof : string -> func_def -> import list -> string list -> proof_kind
-> Coq_ast.t pp = fun import_path def imports ctxt proof_kind ff ast ->
let pp_proof : Coq_path.t -> func_def -> import list -> string list
-> proof_kind -> Coq_ast.t pp =
fun coq_path def imports ctxt proof_kind ff ast ->
(* Formatting utilities. *)
let pp fmt = Format.fprintf ff fmt in
......@@ -1159,8 +1173,8 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
(* Printing some header. *)
pp "@[<v 0>From refinedc.typing Require Import typing.@;";
pp "From %s Require Import generated_code.@;" import_path;
pp "From %s Require Import generated_spec.@;" import_path;
pp "From %a Require Import generated_code.@;" Coq_path.pp coq_path;
pp "From %a Require Import generated_spec.@;" Coq_path.pp coq_path;
List.iter (pp_import ff) imports;
pp "Set Default Proof Using \"Type\".@;@;";
......@@ -1374,7 +1388,7 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
pp "@; all: print_typesystem_goal \"%s\" \"%s\"." def.func_name id
in
List.iter pp_do_step (List.cons "#0" (List.map fst invs_fb));
pp "@;Unshelve. all: sidecond_hook; prepare_sideconditions; ";
pp "@;Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; ";
pp "normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.";
let tactics_items =
let is_all t =
......@@ -1396,6 +1410,7 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
in
List.iter (pp "@;+ %s") tactics_items;
pp "@;all: print_sidecondition_goal \"%s\"." def.func_name;
pp "@;Unshelve. all: try done; try apply: inhabitant; print_remaining_shelved_goal \"%s\"." def.func_name;
pp "@]@;Qed.";
(* Closing the section. *)
......@@ -1403,18 +1418,18 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
type mode =
| Code of string * import list
| Spec of string * import list * inlined_code * typedef list * string list
| Fprf of string * func_def * import list * string list * proof_kind
| Spec of Coq_path.t * import list * inlined_code * typedef list * string list
| Fprf of Coq_path.t * func_def * import list * string list * proof_kind
let write : mode -> string -> Coq_ast.t -> unit = fun mode fname ast ->
let pp =
match mode with
| Code(root_dir,imports) ->
pp_code root_dir imports
| Spec(path,imports,inlined,tydefs,ctxt) ->
pp_spec path imports inlined tydefs ctxt
| Fprf(path,def,imports,ctxt,kind) ->
pp_proof path def imports ctxt kind
| Spec(coq_path,imports,inlined,tydefs,ctxt) ->
pp_spec coq_path imports inlined tydefs ctxt
| Fprf(coq_path,def,imports,ctxt,kind) ->
pp_proof coq_path def imports ctxt kind
in
(* We write to a buffer. *)
let buffer = Buffer.create 4096 in
......
......@@ -5,7 +5,7 @@
(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 toml earley.core cerberus.frontend
(libraries cmdliner str unix toml ubase earley.core cerberus.frontend
cerberus.backend_common cerberus.mem.concrete cerberus.util))
(rule
......
......@@ -15,6 +15,14 @@ module Int =
let compare = (-)
end
module Char =
struct
include Char
let printable_ascii : char -> bool = fun c ->
' ' <= c && c <= '~'
end
module Option =
struct
type 'a t = 'a option
......@@ -183,6 +191,15 @@ module String =
let for_all : (char -> bool) -> string -> bool = fun p s ->
try iter (fun c -> if not (p c) then raise Exit) s; true
with Exit -> false
let sub_from : string -> int -> string = fun s i ->
sub s i (length s - i)
let trim_leading : char -> string -> string = fun c s ->
let len = length s in
let index = ref 0 in
while !index < len && s.[!index] = '_' do incr index done;
sub_from s !index
end
(** [outut_lines oc ls] prints the lines [ls] to the output channel [oc]. Note
......
......@@ -59,3 +59,13 @@ let pp_loc : t pp = fun ff (key, pool) ->