Commit d84c5e66 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Improve the handling of Coq path.

This includes:
- A more robust behaviour of [refinedc init], including suggestions.
- A new [Coq_path] module to convert between strings and module paths.
parent a8710147
Pipeline #53845 passed with stage
in 13 minutes and 28 seconds
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
......@@ -808,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
......@@ -830,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";
......@@ -1150,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
......@@ -1172,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\".@;@;";
......@@ -1417,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
......
......@@ -7,7 +7,7 @@ open Version
(* Standard file and directory names. *)
let rc_project_file = "rc-project.toml"
let dune_project_file = "dune-project"
let dune_proj_file = "dune-project"
let coq_project_file = "_CoqProject"
let rc_dir_name = "proofs"
......@@ -16,7 +16,15 @@ let spec_file_name = "generated_spec.v"
let proof_file_name = Printf.sprintf "generated_proof_%s.v"
let proofs_file_name = "proof_files"
let default_coqdir base = ["refinedc"; "project"; base]
let default_coq_root_prefix = ["refinedc"; "project"]
(* The default Coq root is the above prefix followed by the project name. *)
let default_coq_root : Coq_path.member -> Coq_path.t =
let default_coq_root_prefix =
try List.map Coq_path.member_of_string default_coq_root_prefix
with Invalid_argument(_) -> assert false (* Should never fail. *)
in
fun base -> Coq_path.path_of_members (default_coq_root_prefix @ [base])
(* RefinedC include directory (containing [refinedc.h]). *)
let refinedc_include : string option =
......@@ -33,7 +41,7 @@ let refinedc_include : string option =
A RefinedC project, when it is initialized, contains the following files in
its root directory:
- [rc_project_file] containing certain project metadata,
- [dune_project_file] containing the build system setup for Coq,
- [dune_proj_file] containing the build system setup for Coq,
- [coq_project_file] containing editor setup for Coq.
These files are generated, and should not be modified directly. These files
all have special, reserved names, that should not be used for other files.
......@@ -99,80 +107,112 @@ let refinedc_include : string option =
a function spec, a proof file may no longer correspond to anything. In that
case it is deleted by RefinedC automatically upon generation. *)
type config =
{ cpp_config : Cerb_wrapper.cpp_config
; no_locs : bool
; no_analysis : bool
; no_build : bool }
(* Main entry point. *)
let run : config -> string -> unit = fun cfg c_file ->
(* Set the printing flags. *)
if cfg.no_locs then
begin
Coq_pp.print_expr_locs := false;
Coq_pp.print_stmt_locs := false
end;
(* Split the file path into a file name and absolute directory path. *)
let c_file =
(** Metadata associated to a C file. *)
type c_file_data = {
orig_path : string; (** Path given by the user on the command line. *)
file_path : string; (** Absolute, normalised file path. *)
file_dir : string; (** Directory holding the file. *)
base_name : string; (** Base name of the file, without extension. *)
root_dir : string; (** Absolute path to the RefinedC project root. *)
rel_path : string list; (** Relative path to the parent directory. *)
proj_cfg : project_config; (** Associated project configuration. *)
}
(** [get_c_file_data path] computes various metadata for the C file pointed to
by the given [path]. It includes, for instance, the path to the associated
RefinedC project directory. In case of error a suitable message is printed
and the program is terminated. *)
let get_c_file_data : string -> c_file_data = fun c_file ->
(* Original file path. *)
let orig_path = c_file in
(* Absolute, normalised file path. *)
let file_path =
try Filename.realpath c_file with Invalid_argument(_) ->
panic "File [%s] disappeared..." c_file
in
let c_file_name = Filename.basename c_file in
let c_file_name_no_ext = Filename.remove_extension c_file_name in
let c_file_dir = Filename.dirname c_file in
(* Locate the RefinedC project root and the relitive logical directory. *)
let find_root_and_dir_path dir =
panic "File \"%s\" disappeared..." c_file
in
(* Directoru, base name and extension. *)
let file_dir = Filename.dirname file_path in
let base_name = Filename.basename file_path in
let base_name = Filename.remove_extension base_name in
(* Root directory and relative path. *)
let (root_dir, rel_path) =
let rec find acc dir =
let rc_project = Filename.concat dir rc_project_file in
if Sys.file_exists rc_project then
(dir, acc)
else
if Sys.file_exists rc_project then (dir, acc) else
let parent = Filename.dirname dir in
if parent = dir then raise Not_found;
find (Filename.basename dir :: acc) parent
in
find [] dir
try find [] file_dir with Not_found ->
panic "No RefinedC project can be located for file \"%s\"." orig_path
in
let (root_dir, c_file_dir_path) =
try find_root_and_dir_path c_file_dir with Not_found ->
panic "No RefinedC project can be located for file [%s]." c_file
in
(* Read the project configuration from the project file. *)
let project_config =
(* Reading the project configuration. *)
let proj_cfg =
let project_file = Filename.concat root_dir rc_project_file in
try
if Sys.is_directory project_file then
panic "Invalid project file [%s] (directory)." project_file;
panic "Invalid project file \"%s\" (directory)." project_file;
read_project_file project_file
with Sys_error(_) ->
panic "Error while reading the project file [%s]." project_file
panic "Error while reading the project file \"%s\"." project_file
in
{orig_path; file_path; file_dir; base_name; root_dir; rel_path; proj_cfg}
(** Command line configuration for the ["check"] command. *)
type config =
{ cpp_config : Cerb_wrapper.cpp_config
; no_locs : bool
; no_analysis : bool
; no_build : bool }
(** Entry point for the ["check"] command. *)
let run : config -> string -> unit = fun cfg c_file ->
(* Set the printing flags. *)
if cfg.no_locs then
begin
Coq_pp.print_expr_locs := false;
Coq_pp.print_stmt_locs := false
end;
(* Obtain the metadata for the input C file. *)
let c_file = get_c_file_data c_file in
(* Compute the base Coq logical path for the files. *)
let file_coq_dir = project_config.project_coq_root @ c_file_dir_path in
let path = String.concat "." file_coq_dir ^ "." ^ c_file_name_no_ext in
let path =
let suffix =
let suffix = c_file.rel_path @ [c_file.base_name] in
try List.map Coq_path.member_of_string suffix
with Invalid_argument(msg) ->
panic "File \"%s\" does not correspond to a valid Coq module path.\n\
The obtained module path segment is \"%s\".\n%s"
c_file.orig_path (String.concat "." suffix) msg
in
Coq_path.append c_file.proj_cfg.project_coq_root suffix
in
(* Prepare the output folder if need be. *)
let file_rc_dir = Filename.concat c_file_dir rc_dir_name in
let file_rc_dir = Filename.concat c_file.file_dir rc_dir_name in
if not (Sys.file_exists file_rc_dir) then Unix.mkdir file_rc_dir 0o755;
let output_dir = Filename.concat file_rc_dir c_file_name_no_ext in
let output_dir = Filename.concat file_rc_dir c_file.base_name in
if not (Sys.file_exists output_dir) then
begin
Unix.mkdir output_dir 0o755;
(* Add the mapping to the Coq project file for editors. *)
let dune_dir_path =
let relative_path = Filename.relative_path root_dir c_file_dir in
let relative_path =
Filename.relative_path c_file.root_dir c_file.file_dir
in
let path =
if relative_path = Filename.current_dir_name then "_build/default"
else Filename.concat "_build/default" relative_path
in
let path = Filename.concat path rc_dir_name in
Filename.concat path c_file_name_no_ext
Filename.concat path c_file.base_name
in
let coq_project_path = Filename.concat root_dir coq_project_file in
let new_line = Printf.sprintf "-Q %s %s" dune_dir_path path in
let lines = try read_file coq_project_path with Sys_error(_) -> [] in
let coq_proj_path = Filename.concat c_file.root_dir coq_project_file in
let new_line =
Printf.sprintf "-Q %s %s" dune_dir_path (Coq_path.to_string path)
in
let lines = try read_file coq_proj_path with Sys_error(_) -> [] in
if not (List.mem new_line lines) then
append_file (Filename.concat root_dir coq_project_file) [new_line]
append_file coq_proj_path [new_line]
end;
(* Paths to the output files. *)
let code_file = Filename.concat output_dir code_file_name in
......@@ -183,11 +223,12 @@ let run : config -> string -> unit = fun cfg c_file ->
(* Prepare the CPP configuration. *)
let cpp_config =
let cpp_I =
let project_include =
List.map (Filename.concat root_dir) project_config.project_cpp_include
let proj_include =
let incl = c_file.proj_cfg.project_cpp_include in
List.map (Filename.concat c_file.root_dir) incl
in
let cpp_include = cfg.cpp_config.cpp_I @ project_include in
match (refinedc_include, project_config.project_cpp_with_rc) with
let cpp_include = cfg.cpp_config.cpp_I @ proj_include in
match (refinedc_include, c_file.proj_cfg.project_cpp_with_rc) with
| (_ , false) -> cpp_include
| (Some(d), true ) -> d :: cpp_include
| (None , true ) ->
......@@ -197,17 +238,20 @@ let run : config -> string -> unit = fun cfg c_file ->
in
(* Parse the comment annotations. *)
let open Comment_annot in
let ca = parse_annots (Cerb_wrapper.cpp_lines cpp_config c_file) in
let ca =
let lines = Cerb_wrapper.cpp_lines cpp_config c_file.file_path in
parse_annots lines
in
let ctxt = List.map (fun s -> "Context " ^ s) ca.ca_context in
(* Do the translation to Ail, analyse, and generate our AST. *)
Sys.chdir root_dir; (* Move to the root to get relative paths. *)
let c_file = Filename.relative_path root_dir c_file in
let ail_ast = Cerb_wrapper.c_file_to_ail cpp_config c_file in
Sys.chdir c_file.root_dir; (* Move to the root to get relative paths. *)
let c_file_rel = Filename.relative_path c_file.root_dir c_file.file_path in
let ail_ast = Cerb_wrapper.c_file_to_ail cpp_config c_file_rel in
if not cfg.no_analysis then Warn.warn_file ail_ast;
let coq_ast = Ail_to_coq.translate c_file ail_ast in
let coq_ast = Ail_to_coq.translate c_file_rel ail_ast in
(* Generate the code file. *)
let open Coq_pp in
let mode = Code(root_dir, ca.ca_code_imports) in
let mode = Code(c_file.root_dir, ca.ca_code_imports) in
write mode code_file coq_ast;
(* Generate the spec file. *)
let mode = Spec(path, ca.ca_imports, ca.ca_inlined, ca.ca_typedefs, ctxt) in
......@@ -250,26 +294,30 @@ let run : config -> string -> unit = fun cfg c_file ->
List.iter write_proof coq_ast.functions;
(* Generate the dune file. *)
let theories =
let glob = List.map coq_path_to_string project_config.project_theories in
let glob = List.map Coq_path.to_string c_file.proj_cfg.project_theories in
let imports = ca.ca_imports @ ca.ca_proof_imports @ ca.ca_code_imports in
let imports = List.sort_uniq Stdlib.compare imports in
ignore imports; (* TODO some dependency analysis based on [imports]. *)
List.sort_uniq String.compare (List.filter (fun s -> s <> path) (ca.ca_requires @ glob))
let theories =
let path = Coq_path.to_string path in
List.filter (fun s -> s <> path) (ca.ca_requires @ glob)
in
List.sort_uniq String.compare theories
in
write_file dune_file [
"; Generated by [refinedc], do not edit.";
"(coq.theory";
" (flags -w -notation-overridden -w -redundant-canonical-projection)";
Printf.sprintf " (name %s)" path;
Printf.sprintf " (name %s)" (Coq_path.to_string path);
Printf.sprintf " (theories %s))" (String.concat " " theories);
];
(* Run Coq type-checking. *)
if not (cfg.no_build || project_config.project_no_build) then
if not (cfg.no_build || c_file.proj_cfg.project_no_build) then
begin
Sys.chdir output_dir;
match Sys.command "dune build --display=short" with
| 0 ->
Format.printf "File [%s] successfully checked.\n%!" c_file
info "File \"%s\" successfully checked.\n%!" c_file.orig_path
| i ->
panic "The call to [dune] returned with error code %i." i
| exception _ ->
......@@ -381,47 +429,12 @@ let ail_cmd =
(* Cleaning command. *)
let run_clean soft c_file =
(* Split the file path into a file name and absolute directory path. *)
let c_file_name = Filename.basename c_file in
let c_file_name_no_ext = Filename.remove_extension c_file_name in
let c_file_dir =
let c_file_dir = Filename.dirname c_file in
try Filename.realpath c_file_dir with Invalid_argument(_) ->
panic "Directory [%s] disappeared..." c_file_dir
in
(* Check that the C source file is indeed in a RefinedC project. *)
let find_root_and_dir_path dir =
let rec find acc dir =
let rc_project = Filename.concat dir rc_project_file in
if Sys.file_exists rc_project then
(dir, acc)
else
let parent = Filename.dirname dir in
if parent = dir then raise Not_found;
find (Filename.basename dir :: acc) parent
in
find [] dir
in
let (root_dir, c_file_dir_path) =
try find_root_and_dir_path c_file_dir with Not_found ->
panic "No RefinedC project can be located for file [%s]." c_file
in
(* Read the project configuration from the project file. *)
let project_config =
let project_file = Filename.concat root_dir rc_project_file in
try
if Sys.is_directory project_file then
panic "Invalid project file [%s] (directory)." project_file;
read_project_file project_file
with Sys_error(_) ->
panic "Error while reading the project file [%s]." project_file
in
(* Compute the base Coq logical path for the files. *)
let file_coq_dir = project_config.project_coq_root @ c_file_dir_path in
let run_clean : bool -> string -> unit = fun soft c_file ->
(* Obtain the metadata for the input C file. *)
let c_file = get_c_file_data c_file in
(* Compute the relevant directory and file paths. *)
let rc_dir = Filename.concat c_file_dir rc_dir_name in
let gen_dir = Filename.concat rc_dir c_file_name_no_ext in
let rc_dir = Filename.concat c_file.file_dir rc_dir_name in
let gen_dir = Filename.concat rc_dir c_file.base_name in
let dune_file = Filename.concat gen_dir "dune" in
let proofs_file = Filename.concat gen_dir proofs_file_name in
let code_file = Filename.concat gen_dir code_file_name in
......@@ -443,15 +456,29 @@ let run_clean soft c_file =
List.iter rmdir all_dirs;
(* Delete the Coq project mapping for the file. *)
if not soft then
let path = String.concat "." file_coq_dir ^ "." ^ c_file_name_no_ext in
(* Compute the base Coq logical path for the files. *)
let path =
let suffix =
let suffix = c_file.rel_path @ [c_file.base_name] in
try List.map Coq_path.member_of_string suffix
with Invalid_argument(msg) ->
panic "File \"%s\" does not correspond to a valid Coq module path.\n\
The obtained module path segment is \"%s\".\n%s"
c_file.orig_path (String.concat "." suffix) msg
in
Coq_path.append c_file.proj_cfg.project_coq_root suffix
in
let dune_dir_path =
let relative_path = Filename.relative_path root_dir c_file_dir in
let path = Filename.concat "_build/default" relative_path in
let rel_path = Filename.relative_path c_file.root_dir c_file.file_dir in
let path = Filename.concat "_build/default" rel_path in
let path = Filename.concat path rc_dir_name in
Filename.concat path c_file_name_no_ext
Filename.concat path c_file.base_name
in
let coq_project_path = Filename.concat c_file.root_dir coq_project_file in