Commit 15fda11c authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Paul
Browse files

Have front-end generate bitfield stuff.

parent 8a4e9a6b
......@@ -633,3 +633,28 @@ Arguments can be given as well as follows.
//rc::typedef tree<x:A, y:B, z:C> ≔ ...
```
Types can be omitted for the parameters.
## Bitfields description
A bitfield type can be generated (as part of the spec file) given annotations
of the following form.
```c
//@rc::bitfields <ident as name> as <integer type>
//@ <field name 1> : <field type 1>
//@ <field name 2> : <field type 2>
//@ <field name 3> : <field type 3>
//@rc::end
```
The provided name is used as a base for the type name, and the integer type
(of the form `i32`, `u64`, ...) should give the intended signedness as well
as width for integers intended to store the bitfields.
Each field is specified using a name and a type, which includes a bit range.
The syntax of types is given bellow.
```
<field type> ::=
| "bool[" <index> "]"
| "integer[" <index> "]"
| "integer[" <index> ".." <index> "]"
```
The syntax `integer[42]` is equivalent to `integer[42..42]`.
......@@ -5,6 +5,38 @@ type inlined_code =
; ic_section : string list
; ic_final : string list }
type bff_type =
| BFF_bool of int
| BFF_integer of int * int
let bff_type_of_string : string -> bff_type option = fun s ->
let parse_rest ty s =
if s = "" || s.[String.length s - 1] <> ']' then None else
let s = String.sub s 0 (String.length s - 1) in
let s =
match String.split_on_char '.' s with
| [i] -> [String.trim i]
| [i; ""; j] -> [String.trim i; String.trim j]
| _ -> []
in
try
match (ty, List.map int_of_string s) with
| (`Bool, [i] ) -> Some(BFF_bool(i))
| (`Int , [i] ) -> Some(BFF_integer(i,i))
| (`Int , [i;j]) -> Some(BFF_integer(i,j))
| _ -> None
with Failure(_) -> None
in
match List.map String.trim (String.split_on_char '[' s) with
| [ "bool" ; s ] -> parse_rest `Bool s
| [ "integer" ; s ] -> parse_rest `Int s
| _ -> None
type bitfields_spec =
{ bf_name : string
; bf_type : bool * int (* signed, width *)
; bf_fields : (string * bff_type) list }
type comment_annots =
{ ca_inlined : inlined_code
; ca_requires : string list
......@@ -12,7 +44,8 @@ type comment_annots =
; ca_proof_imports : (string * string) list
; ca_code_imports : (string * string) list
; ca_context : string list
; ca_typedefs : Rc_annot.typedef list }
; ca_typedefs : Rc_annot.typedef list
; ca_bitfields : bitfields_spec list }
type annot_line =
| AL_annot of string * string option
......@@ -64,6 +97,7 @@ let parse_annots : string list -> comment_annots = fun ls ->
let inlined_top = ref [] in
let inlined_end = ref [] in
let typedefs = ref [] in
let bitfields = ref [] in
let context = ref [] in
let read_block start_tag ls =
let rec read_block acc ls =
......@@ -99,10 +133,52 @@ let parse_annots : string list -> comment_annots = fun ls ->
in
r := lines @ !r; ls
in
let add_bitfield ls =
let (lines, ls) = read_block n ls in
let p = get_payload () in
let bf =
let (bf_name, bf_type) =
let p = String.split_on_char ' ' p in
let parse_bf_type s =
let w =
try int_of_string (String.sub s 1 (String.length s - 1))
with Failure(_) ->
error "annotation [rc::%s] contains an invalid type" n
in
match s.[0] with
| 'i' -> (true , w)
| 'u' -> (false, w)
| _ -> error "annotation [rc::%s] contains an invalid type" n
in
match List.filter (fun s -> s <> "") p with
| [ bf_name ; "as" ; bf_type ] -> (bf_name, parse_bf_type bf_type)
| _ ->
error "annotation [rc::%s] expects payload \"<name> as <type>\"" n
in
let parse_field line =
let line = String.split_on_char ':' line in
let (field, field_type) =
match List.map String.trim line with
| [ field; field_type ] -> (field, field_type)
| _ ->
error "field description for type [%s] is invalid" bf_name
in
let field_type =
match bff_type_of_string field_type with Some(ty) -> ty | None ->
error "field description for type [%s] is invalid" bf_name
in
(field, field_type)
in
let bf_fields = List.rev_map parse_field lines in
{ bf_name ; bf_type ; bf_fields }
in
bitfields := bf :: !bitfields; ls
in
match n with
| "inlined" -> loop (add_inlined inlined p ls)
| "inlined_prelude" -> loop (add_inlined inlined_top p ls)
| "inlined_final" -> loop (add_inlined inlined_end p ls)
| "bitfields" -> loop (add_bitfield ls)
| "end" -> error "no block has been started"
| "import" ->
begin
......@@ -143,4 +219,5 @@ let parse_annots : string list -> comment_annots = fun ls ->
; ca_imports = List.map (fun (f,m,_) -> (f,m)) imports
; ca_requires = List.rev !requires
; ca_context = List.rev !context
; ca_typedefs = List.rev !typedefs }
; ca_typedefs = List.rev !typedefs
; ca_bitfields = List.rev !bitfields }
......@@ -809,13 +809,95 @@ let collect_invs : func_def -> (string * loop_annot) list = fun def ->
in
SMap.fold fn def.func_blocks []
let pp_spec : Coq_path.t -> import list -> inlined_code ->
typedef list -> string list -> Coq_ast.t pp =
fun coq_path imports inlined typedefs ctxt ff ast ->
let pp_spec : Coq_path.t -> import list -> bitfields_spec list ->
inlined_code -> typedef list -> string list -> Coq_ast.t pp =
fun coq_path imports bf_specs inlined typedefs ctxt ff ast ->
(* Formatting utilities. *)
let pp fmt = Format.fprintf ff fmt in
(* Print the definition of a bitfield specifications. *)
let pp_bitfield_spec _ {bf_name=n; bf_type=ty; bf_fields=fs} =
pp "Record %s := mk_%s {@;" n n;
let pp_field_def (f, ty) =
let ty = match ty with BFF_bool(_) -> "bool" | _ -> "Z" in
pp " %s : %s;@;" f ty
in
List.iter pp_field_def fs;
pp "}.\n@;";
pp "Global Instance %s_settable : Settable _ := settable! mk_%s@;" n n;
pp " <%a>.\n@;" (pp_sep "; " pp_print_string) (List.map fst fs);
pp "Definition zero_%s := {|@;" n;
let pp_field_def (f, ty) =
let zero = match ty with BFF_bool(_) -> "false" | _ -> "0" in
pp " %s := %s;@;" f zero
in
List.iter pp_field_def fs;
pp "|}.\n@;";
pp "Definition %s_repr (r : %s) : tm :=@;" n n;
let bff_type_to_range ty =
match ty with
| BFF_bool(i) -> (i, 1)
| BFF_integer(i,j) -> (i, j - i + 1)
in
let pp_field_def (f, ty) =
let (i, j) = bff_type_to_range ty in
let extra = match ty with BFF_bool(_) -> " Z_of_bool $ " | _ -> "" in
pp " bf_cons (range_of %i %i) (bf_val $ %s%s r) $@;" i j extra f
in
List.iter pp_field_def fs;
pp " bf_nil.@;";
pp "Arguments %s_repr _/.\n@;" n;
pp "Definition %s_wf (r : %s) : Prop :=@;" n n;
let pp_field_def (f, ty) =
let w = match ty with BFF_bool(_) -> 1 | BFF_integer(i,j) -> j-i+1 in
let extra = match ty with BFF_bool(_) -> "Z_of_bool $ " | _ -> "" in
pp " 0 ≤ %s%s r < 2^%i ∧@;" extra f w
in
List.iter pp_field_def fs;
pp " True.\n@;";
pp "Global Program Instance %s_bd : BitfieldDesc %s := {|@;" n n;
pp " bitfield_it := %c%i;@;" (if fst ty then 'i' else 'u') (snd ty);
pp " bitfield_repr := %s_repr;@;" n;
pp " bitfield_wf := %s_wf;@;" n;
pp " bitfield_sig := {|@;";
pp " sig_bits := %i;@;" (snd ty);
pp " sig_ranges := [#@;";
let pp_range _ (_, ty) =
let (i, j) = bff_type_to_range ty in
pp "(range_of %i %i)" i j
in
pp " %a@;" (pp_sep "; " pp_range) fs;
pp " ];@;";
pp " |}@;";
pp "|}.@;";
pp "Next Obligation. solve_ranges_monotone. Qed.@;";
pp "Next Obligation. sig_max_range_bounded. Qed.@;";
pp "Next Obligation. done. Qed.\n@;";
let pp_inst_body q =
pp " %s %a, P {|@;" q (pp_sep " " pp_print_string) (List.map fst fs);
let pp_field_def (f, _) = pp " %s := %s;@;" f f in
List.iter pp_field_def fs;
pp " |}@;"
in
pp "Global Instance simpl_exist_%s P : SimplExist %s P (@;" n n;
pp_inst_body "∃";
pp ").@;";
pp "Proof. unfold SimplExist. naive_solver. Qed.\n@;";
pp "Global Instance simpl_forall_%s P : SimplForall %s %i P (@;" n n
(List.length fs);
pp_inst_body "∀";
pp ").@;";
pp "Proof. unfold SimplForall => ? []. naive_solver. Qed."
in
(* Print inlined code (starts with an empty line) *)
let pp_inlined extra_line_after descr ls =
if ls <> [] then pp "\n";
......@@ -838,6 +920,10 @@ let pp_spec : Coq_path.t -> import list -> inlined_code ->
(* Printing generation data in a comment. *)
pp "@;(* Generated from [%s]. *)" ast.source_file;
(* Printing bitfield specifications. *)
if bf_specs <> [] then pp "\n";
List.iter (pp "@;%a\n" pp_bitfield_spec) bf_specs;
(* Printing inlined code (from comments). *)
pp_inlined true (Some "prelude") inlined.ic_prelude;
......@@ -1416,17 +1502,17 @@ let pp_proof : Coq_path.t -> func_def -> import list -> string list
type mode =
| Code of string * import list
| Spec of Coq_path.t * import list * inlined_code * typedef list * string list
| Spec of Coq_path.t * import list * bitfields_spec 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) ->
| Code(root_dir,imports) ->
pp_code root_dir imports
| Spec(coq_path,imports,inlined,tydefs,ctxt) ->
pp_spec coq_path imports inlined tydefs ctxt
| Fprf(coq_path,def,imports,ctxt,kind) ->
| Spec(coq_path,imports,bf_specs,inlined,tydefs,ctxt) ->
pp_spec coq_path imports bf_specs inlined tydefs ctxt
| Fprf(coq_path,def,imports,ctxt,kind) ->
pp_proof coq_path def imports ctxt kind
in
(* We write to a buffer. *)
......
......@@ -254,7 +254,10 @@ let run : config -> string -> unit = fun cfg c_file ->
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
let mode =
let bfs = ca.ca_bitfields in
Spec(path, ca.ca_imports, bfs, ca.ca_inlined, ca.ca_typedefs, ctxt)
in
write mode spec_file coq_ast;
(* Compute the list of proof files to generate. *)
let to_generate =
......
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