From 893dcc99c6c9b41246c6c2cad79d408718d0c455 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Wed, 18 May 2022 14:29:49 +0200
Subject: [PATCH] generate *_memory.h and *_spec.h headers
---
src/backends/C/c_backend.ml | 36 ++-
src/backends/C/c_backend_common.ml | 7 +-
src/backends/C/c_backend_common.mli | 1 +
src/backends/C/c_backend_header.ml | 103 ++++--
src/backends/C/c_backend_header.mli | 8 +-
src/backends/C/c_backend_spec.ml | 474 ++++++++++++++--------------
src/backends/C/c_backend_src.ml | 35 +-
src/backends/C/c_backend_src.mli | 3 +-
8 files changed, 369 insertions(+), 298 deletions(-)
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 5e524fee..62c7014f 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -38,12 +38,26 @@ let with_main_node machines node f =
f m
let gen_files
- ( print_alloc_header,
+ generate_spec_header
+ ( print_memory_header,
+ print_alloc_header,
+ print_spec_header,
print_lib_c,
print_main_c,
print_makefile (* , print_cmake *) ) basename prog machines dependencies =
let destname = !Options.dest_dir ^ "/" ^ basename in
+ (* Generating H spec file *)
+ if generate_spec_header then
+ let spec_header_file = destname ^ "_spec.h" in
+ with_out_file spec_header_file (fun header_fmt ->
+ print_spec_header header_fmt basename machines dependencies);
+
+ (* Generating H memory file *)
+ let memory_header_file = destname ^ "_memory.h" in
+ with_out_file memory_header_file (fun header_fmt ->
+ print_memory_header header_fmt basename machines dependencies);
+
(* Generating H alloc file *)
let alloc_header_file = destname ^ "_alloc.h" in
(* Could be changed *)
@@ -115,23 +129,25 @@ let print_c_header basename =
(* Generating H file *)
let lusic = Lusic.read_lusic destname ".lusic" in
let header_file = destname ^ ".h" in
- with_out_file header_file (fun header_fmt ->
- assert (not lusic.obsolete);
- Header.pp_header_from_header header_fmt basename lusic.contents)
+ with_out_file header_file @@ fun header_fmt ->
+ assert (not lusic.obsolete);
+ Header.pp_header_from_header header_fmt basename lusic.contents
let translate_to_c generate_c_header basename prog machines dependencies =
- let header_m, source_m, source_main_m, makefile_m, machines =
+ let generate_spec_header, header_m, source_m, source_main_m, makefile_m, machines =
let open Options in
match !spec with
| SpecNo ->
- ( C_backend_header.((module EmptyMod : MODIFIERS_HDR)),
+ ( false,
+ C_backend_header.((module EmptyMod : MODIFIERS_HDR)),
C_backend_src.((module EmptyMod : MODIFIERS_SRC)),
C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)),
machines )
| SpecACSL ->
let open C_backend_spec in
- ( C_backend_header.((module HdrMod : MODIFIERS_HDR)),
+ ( true,
+ C_backend_header.((module HdrMod : MODIFIERS_HDR)),
C_backend_src.((module SrcMod : MODIFIERS_SRC)),
C_backend_main.((module MainMod : MODIFIERS_MAINSRC)),
C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)),
@@ -146,14 +162,16 @@ let translate_to_c generate_c_header basename prog machines dependencies =
let module Makefile = C_backend_makefile.Main ((val makefile_m)) in
(* let module CMakefile = C_backend_cmake.Main (MakefileMod) in *)
let funs =
- ( Header.pp_alloc_header,
+ ( Header.pp_memory_header,
+ Header.pp_alloc_header,
+ Header.pp_spec_header,
Source.pp_lib_c,
SourceMain.pp_main_c,
Makefile.pp_makefile )
(* CMakefile.print_makefile *)
in
if generate_c_header then print_c_header basename;
- gen_files funs basename prog machines dependencies
+ gen_files generate_spec_header funs basename prog machines dependencies
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index b74c6d95..bc26d978 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -931,10 +931,13 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
outputs
end
-let pp_import_prototype fmt dep = fprintf fmt "#include \"%s.h\"" dep.name
+let pp_import_prototype fmt dep = fprintf fmt "#include \"%s.h\"@," dep.name
+
+let pp_import_memory_prototype fmt dep =
+ if dep.is_stateful then fprintf fmt "#include \"%s_memory.h\"@," dep.name
let pp_import_alloc_prototype fmt dep =
- if dep.is_stateful then fprintf fmt "#include \"%s_alloc.h\"" dep.name
+ if dep.is_stateful then fprintf fmt "#include \"%s_alloc.h\"@," dep.name
let pp_c_var m self pp_var fmt var =
pp_c_val m self pp_var fmt (Machine_code_common.mk_val (Var var) var.var_type)
diff --git a/src/backends/C/c_backend_common.mli b/src/backends/C/c_backend_common.mli
index a0a5c28a..ef7c56af 100644
--- a/src/backends/C/c_backend_common.mli
+++ b/src/backends/C/c_backend_common.mli
@@ -25,6 +25,7 @@ val pp_alloc_prototype : formatter -> ident * var_decl list -> unit
val pp_dealloc_prototype : formatter -> ident -> unit
val pp_import_prototype : formatter -> dep_t -> unit
val pp_import_alloc_prototype : formatter -> dep_t -> unit
+val pp_import_memory_prototype : formatter -> dep_t -> unit
val pp_c_var_read :
?test_output:bool -> machine_t -> formatter -> var_decl -> unit
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 3d8400ea..7e08852b 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -24,8 +24,8 @@ module Mpfr = Lustrec_mpfr
module type MODIFIERS_HDR = sig
module GhostProto : MODIFIERS_GHOST_PROTO
- val pp_machine_decl_prefix : formatter -> machine_t -> unit
val pp_predicates : formatter -> machine_t list -> unit
+ val pp_machine_decl_prefix : formatter -> machine_t -> unit
val pp_import_arrow : formatter -> unit -> unit
val pp_machine_alloc_decl : formatter -> machine_t -> unit
end
@@ -33,9 +33,10 @@ end
module EmptyMod = struct
module GhostProto = EmptyGhostProto
- let pp_machine_decl_prefix _ _ = ()
let pp_predicates _ _ = ()
+ let pp_machine_decl_prefix _ _ = ()
+
let pp_import_arrow fmt () =
fprintf
fmt
@@ -244,48 +245,47 @@ functor
(* Include once: start *)
let machines' = List.filter (fun m -> not m.mis_contract) machines in
let baseNAME = file_to_module_name basename in
+ let self_dep = {
+ local = true;
+ name = basename;
+ content = [];
+ is_stateful = true (* assuming it is stateful *);
+ }
+ in
fprintf
header_fmt
"@[<v>%a@,\
- #ifndef _%s_alloc@,\
- #define _%s_alloc@,\
+ #ifndef _%s_ALLOC@,\
+ #define _%s_ALLOC@,\
@,\
/* Import header from %s */@,\
- %a@,\
+ %a\
@,\
- %a%a%a%a%a#endif@]@."
+ /* Import memory header from %s */@,\
+ %a\
+ @,\
+ %a%a%a#endif@]@."
(* Print the svn version number and the supported C standard (C90 or
C99) *)
pp_print_version
()
baseNAME
baseNAME
- (* Import the header *) basename
+ (* Import the header *)
+ basename
pp_import_prototype
- {
- local = true;
- name = basename;
- content = [];
- is_stateful = true (* assuming it is staful *);
- }
- (* Print dependencies *)
+ self_dep
+ (* Import the memory header *)
+ basename
+ pp_import_memory_prototype
+ self_dep
+ (* Print dependencies *)
(pp_print_list
~pp_open_box:pp_open_vbox0
~pp_prologue:(pp_print_endcut "/* Import dependencies */")
pp_import_alloc_prototype
~pp_epilogue:pp_print_cutcut)
dependencies
- (* Print the struct definitions of all machines. *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
- ~pp_sep:pp_print_cutcut
- pp_machine_struct
- ~pp_epilogue:pp_print_cutcut)
- machines'
- (* Copy the spec (valid and memory packs predicates). *)
- Mod.pp_predicates
- machines
(* Print the prototypes of all machines *)
(pp_print_list
~pp_open_box:pp_open_vbox0
@@ -399,6 +399,59 @@ functor
pp_machine_decl_top_decl_from_header
~pp_epilogue:pp_print_cutcut)
nodes
+
+ let pp_memory_header header_fmt basename machines dependencies =
+ (* Include once: start *)
+ let machines' = List.filter (fun m -> not m.mis_contract) machines in
+ let baseNAME = file_to_module_name basename in
+ fprintf
+ header_fmt
+ "@[<v>%a@,\
+ #ifndef _%s_MEMORY@,\
+ #define _%s_MEMORY@,\
+ @,\
+ %a%a#endif@]@."
+ (* Print the svn version number and the supported C standard (C90 or
+ C99) *)
+ pp_print_version
+ ()
+ baseNAME
+ baseNAME
+ (* Print dependencies *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
+ pp_import_memory_prototype
+ ~pp_epilogue:pp_print_cutcut)
+ dependencies
+ (* Print the struct definitions of all machines. *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
+ ~pp_sep:pp_print_cutcut
+ pp_machine_struct
+ ~pp_epilogue:pp_print_cutcut)
+ machines'
+ (* Include once: end *)
+
+ let pp_spec_header header_fmt basename machines _dependencies =
+ let baseNAME = file_to_module_name basename in
+ fprintf
+ header_fmt
+ "@[<v>%a@,\
+ #ifndef _%s_SPEC@,\
+ #define _%s_SPEC@,\
+ @,\
+ %a#endif@]@."
+ (* Print the svn version number and the supported C standard (C90 or
+ C99) *)
+ pp_print_version
+ ()
+ baseNAME
+ baseNAME
+ Mod.pp_predicates
+ machines
+
end
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
diff --git a/src/backends/C/c_backend_header.mli b/src/backends/C/c_backend_header.mli
index 4f4aa965..cda9efcb 100644
--- a/src/backends/C/c_backend_header.mli
+++ b/src/backends/C/c_backend_header.mli
@@ -6,8 +6,8 @@ open C_backend_common
module type MODIFIERS_HDR = sig
module GhostProto : MODIFIERS_GHOST_PROTO
- val pp_machine_decl_prefix : formatter -> machine_t -> unit
val pp_predicates : formatter -> machine_t list -> unit
+ val pp_machine_decl_prefix : formatter -> machine_t -> unit
val pp_import_arrow : formatter -> unit -> unit
val pp_machine_alloc_decl : formatter -> machine_t -> unit
end
@@ -19,4 +19,10 @@ module Main (Mod : MODIFIERS_HDR) : sig
val pp_alloc_header :
formatter -> string -> machine_t list -> dep_t list -> unit
+
+ val pp_memory_header :
+ formatter -> string -> machine_t list -> dep_t list -> unit
+
+ val pp_spec_header :
+ formatter -> string -> machine_t list -> dep_t list -> unit
end
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index bcead9c2..fc8ae024 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -901,6 +901,209 @@ let pp_reset_flag_chain ?(indirect = true) ptr fmt mems =
let pp_arrow_reset_ghost mem fmt inst =
fprintf fmt "%s_reset_ghost(%a)" Arrow.arrow_id pp_indirect' (mem, inst)
+let contract_of machines m =
+ match m.mspec.mnode_spec with
+ | Some spec -> (
+ match spec with
+ | Contract c ->
+ Some c, None
+ | NodeSpec f -> (
+ let m_f = find_machine f machines in
+ match m_f.mspec.mnode_spec with
+ | Some (Contract c) ->
+ Some c, Some m_f
+ | _ ->
+ None, None))
+ | None ->
+ None, None
+
+let rename n x = sprintf "%s_%d" x n
+let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
+
+let pp_k_induction_case base m m_c pp_mem_out pp_vars fmt
+ (n, mem_out) =
+ let name = m.mname.node_id in
+ fprintf
+ fmt
+ "%s_%s_%d(@[<hov>%a,@;%a@])"
+ name
+ (if base then "base" else "inductive")
+ n
+ pp_mem_out
+ mem_out
+ pp_vars
+ (List.map (rename_var_decl n) m_c.mstep.step_outputs)
+
+let pp_k_induction_case_def base m (_, m_c, _) fmt n =
+ let name = m.mname.node_id in
+ let name_c = m_c.mname.node_id in
+ let mem = mk_mem m in
+ let mem_c = mk_mem_c m in
+ let inputs = m.mstep.step_inputs in
+ let outputs = m.mstep.step_outputs in
+ let stateless = fst (get_stateless_status m) in
+ let stateless_c = fst (get_stateless_status m_c) in
+ let l = List.init (n + 1) Fun.id in
+ let l_pp = List.concat_map (function
+ | 0 ->
+ let pp = pp_reset_set' in
+ [
+ fun fmt ->
+ (if stateless_c then fun fmt (x, _) -> pp fmt x
+ else pp_and pp pp)
+ fmt
+ ((name, rename 0 mem), (name_c, rename 0 mem_c))
+ ]
+ | n' ->
+ let pp_var_c fmt (out, vd) =
+ if out && n' < n then pp_true_c_bool fmt ()
+ else pp_var_decl fmt vd
+ in
+ let c_inputs =
+ List.map
+ (fun v -> false, rename_var_decl n' v)
+ m_c.mstep.step_inputs
+ in
+ let c_outputs =
+ List.map
+ (fun v -> true, rename_var_decl n' v)
+ m_c.mstep.step_outputs
+ in
+ let pp stateless pp_var =
+ pp_transition_aux
+ stateless
+ pp_print_string
+ pp_print_string
+ pp_var
+ in
+ [
+ (fun fmt ->
+ pp stateless pp_var_decl fmt
+ ( name,
+ List.map (rename_var_decl n') (inputs @ outputs),
+ rename (n' - 1) mem,
+ rename n' mem ));
+ (fun fmt ->
+ pp stateless_c pp_var_c fmt
+ ( name_c,
+ c_inputs @ c_outputs,
+ rename (n' - 1) mem_c,
+ rename n' mem_c ))
+ ]) l
+ in
+ let l_pp = if base then l_pp else List.tl l_pp in
+ let pp fmt () =
+ let pp fmt () = pp_and_l (fun fmt f -> f fmt) fmt l_pp in
+ if stateless_c then pp fmt ()
+ else
+ pp_exists
+ (pp_machine_decl
+ ~ghost:true
+ (pp_comma_list (fun fmt n ->
+ pp_print_string fmt (rename n mem_c))))
+ pp
+ fmt
+ ((name_c, l), ())
+ in
+ pp_predicate
+ (pp_k_induction_case
+ base
+ m
+ m_c
+ (pp_machine_decl' ~ghost:true)
+ (pp_locals m_c))
+ (pp_exists
+ (fun fmt l ->
+ fprintf
+ fmt
+ "%a@,%a"
+ (pp_machine_decl
+ ~ghost:true
+ (pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
+ pp_print_string fmt (rename (n - 1) mem))))
+ (name, l)
+ (pp_locals m)
+ (List.concat_map (fun n ->
+ List.map (rename_var_decl n) (inputs @ outputs))
+ l))
+ pp)
+ fmt
+ ( (n, (name, rename n mem)),
+ ( List.tl l, () ) )
+
+let pp_base_case_defs m fmt (_, _, k as c_m_k) =
+ let l = List.init (k - 1) succ in
+ pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:pp_print_cutcut
+ (pp_k_induction_case_def true m c_m_k)
+ fmt
+ l
+
+let pp_inductive_case_def m fmt (_, _, k as c_m_k) =
+ pp_k_induction_case_def false m c_m_k fmt k
+
+let pp_k_induction_lemmas m fmt (_, m_c, k) =
+ let name = m.mname.node_id in
+ let mem = mk_mem m in
+ let l = List.init k (fun n -> n + 1) in
+ pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:pp_print_cutcut
+ (fun fmt n ->
+ let outputs = List.map (rename_var_decl n) m_c.mstep.step_outputs in
+ pp_lemma
+ (fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
+ (pp_forall
+ (fun fmt () ->
+ fprintf
+ fmt
+ "%a,@;%a"
+ (pp_machine_decl' ~ghost:true)
+ (name, mem)
+ (pp_locals m_c)
+ outputs)
+ (pp_implies
+ (pp_k_induction_case
+ (n <> k)
+ m
+ m_c
+ pp_print_string
+ (pp_comma_list pp_var_decl))
+ (pp_and_l
+ (fun fmt x ->
+ pp_equal pp_var_decl pp_print_int fmt (x, 1)))))
+ fmt
+ (n, ((), ((n, mem), outputs))))
+ fmt
+ l
+
+let pp_k_induction m fmt c_m_k =
+ pp_acsl_cut
+ (fun fmt () ->
+ fprintf
+ fmt
+ "%a@,@,%a@,@,%a"
+ (pp_base_case_defs m)
+ c_m_k
+ (pp_inductive_case_def m)
+ c_m_k
+ (pp_k_induction_lemmas m)
+ c_m_k)
+ fmt
+ ()
+
+let pp_proof_annotation m m_c fmt c =
+ let pp m_c fmt = function
+ | Kinduction k ->
+ pp_k_induction m fmt (c, m_c, k)
+ in
+ match m_c with
+ | Some m_c ->
+ pp_print_option (pp m_c) fmt c.mc_proof
+ | None ->
+ ()
+
module GhostProto : MODIFIERS_GHOST_PROTO = struct
let pp_ghost_parameters ?(cut = true) fmt vs =
fprintf
@@ -916,15 +1119,6 @@ end
module HdrMod = struct
module GhostProto = GhostProto
- let pp_machine_decl_prefix _ _ = ()
-
- let pp_import_arrow fmt () =
- fprintf
- fmt
- "#include \"%s/arrow_spec.h%s\""
- (Arrow.arrow_top_decl ()).top_decl_owner
- (if !Options.cpp then "pp" else "")
-
let pp_predicates fmt machines =
let pp_preds comment pp =
pp_print_list
@@ -935,11 +1129,38 @@ module HdrMod = struct
in
fprintf
fmt
- "%a%a"
+ "%a%a%a%a%a%a%a%a"
(pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
machines
(pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
machines
+ (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
+ machines
+ (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
+ machines
+ (pp_preds "/* ACSL reset set annotations */" pp_reset_set_def)
+ machines
+ (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
+ machines
+ (pp_preds
+ "/* ACSL transition memory footprints lemmas */"
+ pp_transition_footprint_lemmas)
+ machines
+ (pp_preds
+ "/* k-induction predicates and lemmas */"
+ (fun fmt m ->
+ let c, m_c = contract_of machines m in
+ (pp_print_option (pp_proof_annotation m m_c) fmt c)))
+ machines
+
+ let pp_machine_decl_prefix _ _ = ()
+
+ let pp_import_arrow fmt () =
+ fprintf
+ fmt
+ "#include \"%s/arrow_spec.h%s\""
+ (Arrow.arrow_top_decl ()).top_decl_owner
+ (if !Options.cpp then "pp" else "")
let pp_machine_alloc_decl fmt m =
pp_machine_decl_prefix fmt m;
@@ -968,33 +1189,8 @@ end
module SrcMod = struct
module GhostProto = GhostProto
- let pp_predicates fmt machines =
- let pp_preds comment pp =
- pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:(pp_print_endcut comment)
- pp
- ~pp_epilogue:pp_print_cutcut
- in
- fprintf
- fmt
- "%a%a%a%a%a%a%a"
- (pp_preds "/* ACSL `valid` predicates */" pp_mem_valid_def)
- machines
- (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
- machines
- (pp_preds "/* ACSL initialization annotations */" pp_initialization_def)
- machines
- (pp_preds "/* ACSL reset cleared annotations */" pp_reset_cleared_def)
- machines
- (pp_preds "/* ACSL reset set annotations */" pp_reset_set_def)
- machines
- (pp_preds "/* ACSL transition annotations */" pp_transition_defs)
- machines
- (pp_preds
- "/* ACSL transition memory footprints lemmas */"
- pp_transition_footprint_lemmas)
- machines
+ let pp_import_spec_prototype fmt dep =
+ fprintf fmt "#include \"%s_spec.h\"@," dep.name
let pp_clear_reset_spec fmt self mem m =
let name = m.mname.node_id in
@@ -1060,25 +1256,6 @@ module SrcMod = struct
(* let pp_contract m fmt c = *)
(* PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c) *)
- let contract_of machines m =
- match m.mspec.mnode_spec with
- | Some spec -> (
- match spec with
- | Contract c ->
- Some c, None
- | NodeSpec f -> (
- let m_f = find_machine f machines in
- match m_f.mspec.mnode_spec with
- | Some (Contract c) ->
- Some c, Some m_f
- | _ ->
- None, None))
- | None ->
- None, None
-
- let rename n x = sprintf "%s_%d" x n
- let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
-
(** UNUSED *)
(* let rec rename_value n v = *)
(* { *)
@@ -1144,190 +1321,6 @@ module SrcMod = struct
(* mc_post = rename_formula n c.mc_post; *)
(* } *)
- let pp_k_induction_case base m m_c pp_mem_out pp_vars fmt
- (n, mem_out) =
- let name = m.mname.node_id in
- fprintf
- fmt
- "%s_%s_%d(@[<hov>%a,@;%a@])"
- name
- (if base then "base" else "inductive")
- n
- pp_mem_out
- mem_out
- pp_vars
- (List.map (rename_var_decl n) m_c.mstep.step_outputs)
-
- let pp_k_induction_case_def base m (_, m_c, _) fmt n =
- let name = m.mname.node_id in
- let name_c = m_c.mname.node_id in
- let mem = mk_mem m in
- let mem_c = mk_mem_c m in
- let inputs = m.mstep.step_inputs in
- let outputs = m.mstep.step_outputs in
- let stateless = fst (get_stateless_status m) in
- let stateless_c = fst (get_stateless_status m_c) in
- let l = List.init (n + 1) Fun.id in
- let l_pp = List.concat_map (function
- | 0 ->
- let pp = pp_reset_set' in
- [
- fun fmt ->
- (if stateless_c then fun fmt (x, _) -> pp fmt x
- else pp_and pp pp)
- fmt
- ((name, rename 0 mem), (name_c, rename 0 mem_c))
- ]
- | n' ->
- let pp_var_c fmt (out, vd) =
- if out && n' < n then pp_true_c_bool fmt ()
- else pp_var_decl fmt vd
- in
- let c_inputs =
- List.map
- (fun v -> false, rename_var_decl n' v)
- m_c.mstep.step_inputs
- in
- let c_outputs =
- List.map
- (fun v -> true, rename_var_decl n' v)
- m_c.mstep.step_outputs
- in
- let pp stateless pp_var =
- pp_transition_aux
- stateless
- pp_print_string
- pp_print_string
- pp_var
- in
- [
- (fun fmt ->
- pp stateless pp_var_decl fmt
- ( name,
- List.map (rename_var_decl n') (inputs @ outputs),
- rename (n' - 1) mem,
- rename n' mem ));
- (fun fmt ->
- pp stateless_c pp_var_c fmt
- ( name_c,
- c_inputs @ c_outputs,
- rename (n' - 1) mem_c,
- rename n' mem_c ))
- ]) l
- in
- let l_pp = if base then l_pp else List.tl l_pp in
- let pp fmt () =
- let pp fmt () = pp_and_l (fun fmt f -> f fmt) fmt l_pp in
- if stateless_c then pp fmt ()
- else
- pp_exists
- (pp_machine_decl
- ~ghost:true
- (pp_comma_list (fun fmt n ->
- pp_print_string fmt (rename n mem_c))))
- pp
- fmt
- ((name_c, l), ())
- in
- pp_predicate
- (pp_k_induction_case
- base
- m
- m_c
- (pp_machine_decl' ~ghost:true)
- (pp_locals m_c))
- (pp_exists
- (fun fmt l ->
- fprintf
- fmt
- "%a@,%a"
- (pp_machine_decl
- ~ghost:true
- (pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
- pp_print_string fmt (rename (n - 1) mem))))
- (name, l)
- (pp_locals m)
- (List.concat_map (fun n ->
- List.map (rename_var_decl n) (inputs @ outputs))
- l))
- pp)
- fmt
- ( (n, (name, rename n mem)),
- ( List.tl l, () ) )
-
- let pp_base_case_defs m fmt (_, _, k as c_m_k) =
- let l = List.init (k - 1) succ in
- pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_sep:pp_print_cutcut
- (pp_k_induction_case_def true m c_m_k)
- fmt
- l
-
- let pp_inductive_case_def m fmt (_, _, k as c_m_k) =
- pp_k_induction_case_def false m c_m_k fmt k
-
- let pp_k_induction_lemmas m fmt (_, m_c, k) =
- let name = m.mname.node_id in
- let mem = mk_mem m in
- let l = List.init k (fun n -> n + 1) in
- pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_sep:pp_print_cutcut
- (fun fmt n ->
- let outputs = List.map (rename_var_decl n) m_c.mstep.step_outputs in
- pp_lemma
- (fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
- (pp_forall
- (fun fmt () ->
- fprintf
- fmt
- "%a,@;%a"
- (pp_machine_decl' ~ghost:true)
- (name, mem)
- (pp_locals m_c)
- outputs)
- (pp_implies
- (pp_k_induction_case
- (n <> k)
- m
- m_c
- pp_print_string
- (pp_comma_list pp_var_decl))
- (pp_and_l
- (fun fmt x ->
- pp_equal pp_var_decl pp_print_int fmt (x, 1)))))
- fmt
- (n, ((), ((n, mem), outputs))))
- fmt
- l
-
- let pp_k_induction m fmt c_m_k =
- pp_acsl_cut
- (fun fmt () ->
- fprintf
- fmt
- "%a@,@,%a@,@,%a"
- (pp_base_case_defs m)
- c_m_k
- (pp_inductive_case_def m)
- c_m_k
- (pp_k_induction_lemmas m)
- c_m_k)
- fmt
- ()
-
- let pp_proof_annotation m m_c fmt c =
- let pp m_c fmt = function
- | Kinduction k ->
- pp_k_induction m fmt (c, m_c, k)
- in
- match m_c with
- | Some m_c ->
- pp_print_option (pp m_c) fmt c.mc_proof
- | None ->
- ()
-
let pp_step_spec fmt machines self mem m =
let name = m.mname.node_id in
let insts = instances machines m in
@@ -1420,7 +1413,6 @@ module SrcMod = struct
(* | _ -> *)
(* pp_print_nothing *)
(* in *)
- pp_print_option (pp_proof_annotation m m_c) fmt c;
(* pp_spec_vars fmt (); *)
pp_acsl_cut
(fun fmt () ->
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 4fa2b900..06da4eac 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -21,7 +21,8 @@ module Mpfr = Lustrec_mpfr
module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
- val pp_predicates : formatter -> machine_t list -> unit
+ val pp_import_spec_prototype : formatter -> dep_t -> unit
+
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
@@ -41,7 +42,7 @@ end
module EmptyMod = struct
module GhostProto = EmptyGhostProto
- let pp_predicates _ _ = ()
+ let pp_import_spec_prototype _ _ = ()
let pp_set_reset_spec _ _ _ _ = ()
let pp_clear_reset_spec _ _ _ _ = ()
let pp_step_spec _ _ _ _ _ = ()
@@ -1000,18 +1001,24 @@ module Main (Mod : MODIFIERS_SRC) = struct
ind.nodei_id
let pp_lib_c source_fmt basename prog machines dependencies =
+ let self_dep = {
+ local = true;
+ name = basename;
+ content = [];
+ is_stateful = true (* assuming it is stateful *);
+ }
+ in
fprintf
source_fmt
- "@[<v>%a%a@,@,%a@,%a%a%a%a%a%a%a@]@."
+ "@[<v>%a%a%a%a@,%a@,%a%a%a%a%a@]@."
pp_import_standard
()
pp_import_prototype
- {
- local = true;
- name = basename;
- content = [];
- is_stateful = true (* assuming it is stateful *);
- }
+ self_dep
+ pp_import_memory_prototype
+ self_dep
+ Mod.pp_import_spec_prototype
+ self_dep
(* Print the svn version number and the supported C standard (C90 or
C99) *)
pp_print_version
@@ -1086,16 +1093,6 @@ module Main (Mod : MODIFIERS_SRC) = struct
machines
else pp_print_nothing)
()
- (* Print the struct definitions of all machines. *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
- ~pp_sep:pp_print_cutcut
- pp_machine_struct
- ~pp_epilogue:pp_print_cutcut)
- (List.filter (fun m -> not m.mis_contract) machines)
- (* Print the spec predicates *) Mod.pp_predicates
- machines
(* Print nodes one by one (in the previous order) *)
(pp_print_list
~pp_open_box:pp_open_vbox0
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
index 1f0f9bcf..12d9fb78 100644
--- a/src/backends/C/c_backend_src.mli
+++ b/src/backends/C/c_backend_src.mli
@@ -7,7 +7,8 @@ open C_backend_common
module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
- val pp_predicates : formatter -> machine_t list -> unit
+ val pp_import_spec_prototype : formatter -> dep_t -> unit
+
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
--
GitLab