From cb8b7a6f846541963f903d7fb840013514d7343d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Tue, 17 Jan 2023 15:41:03 +0900
Subject: [PATCH] Monolithic reset in Spec
---
.ocamlformat | 2 +-
src/automata.ml | 6 +-
src/backends/Ada/misc_lustre_function.ml | 3 +-
src/backends/C/c_backend.ml | 12 +-
src/backends/C/c_backend_common.ml | 41 +-
src/backends/C/c_backend_common.mli | 13 +-
src/backends/C/c_backend_header.ml | 889 ++++++++++++-----------
src/backends/C/c_backend_header.mli | 2 +-
src/backends/C/c_backend_spec.ml | 332 ++++-----
src/backends/C/c_backend_src.ml | 147 +++-
src/backends/C/c_backend_src.mli | 15 +-
src/machine_code.ml | 22 +-
src/machine_code_common.ml | 22 +-
src/spec_common.ml | 11 +-
src/spec_types.ml | 9 +-
src/spec_types.mli | 9 +-
src/tools/tiny/tiny_verifier.ml | 1 -
strategy.ml | 3 -
18 files changed, 806 insertions(+), 733 deletions(-)
diff --git a/.ocamlformat b/.ocamlformat
index c4a2f22e..bf730f69 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.20.1
+version=0.24.1
parens-tuple=multi-line-only
wrap-comments=true
cases-exp-indent=2
diff --git a/src/automata.ml b/src/automata.ml
index 1e3f48c3..493d91fe 100644
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -217,8 +217,7 @@ let node_of_unless nused node aut_id aut_state handler =
(*Format.eprintf "node_of_unless %s@." node.node_id;*)
let inputs = unless_read ISet.empty handler in
let var_inputs =
- aut_state.incoming_r
- (*:: aut_state.incoming_s*)
+ aut_state.incoming_r (*:: aut_state.incoming_s*)
:: node_vars_of_idents node inputs
in
let var_outputs = [ aut_state.actual_r; aut_state.actual_s ] in
@@ -310,8 +309,7 @@ let node_of_assign_until nused used node aut_id aut_state handler =
in
let frename = mk_frename used writes in
let var_inputs =
- aut_state.actual_r
- (*:: aut_state.actual_s*)
+ aut_state.actual_r (*:: aut_state.actual_s*)
:: node_vars_of_idents node inputs
in
let new_var_locals = node_vars_of_idents node writes in
diff --git a/src/backends/Ada/misc_lustre_function.ml b/src/backends/Ada/misc_lustre_function.ml
index e585fbbe..c321b673 100644
--- a/src/backends/Ada/misc_lustre_function.ml
+++ b/src/backends/Ada/misc_lustre_function.ml
@@ -129,7 +129,8 @@ let unification (substituion : (int * Types.t) list)
(* We return the original substituion, it is already correct *)
substituion
(* If type_poly is not in the subsitution *))
- else (* We add it to the substituion *)
+ else
+ (* We add it to the substituion *)
(type_poly.tid, typ) :: substituion (* iftype_poly is not polymorphic *)
else (
(* We check that type_poly and typ are the same *)
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 3c46ad1a..3e25da04 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -113,17 +113,19 @@ let gen_files generate_spec_header
let print_c_header basename =
let open Options in
- let header_m =
+ let source_m, header_m =
match !spec with
| SpecNo ->
- C_backend_header.((module EmptyMod : MODIFIERS_HDR))
+ ( C_backend_src.((module EmptyMod : MODIFIERS_SRC)),
+ C_backend_header.((module EmptyMod : MODIFIERS_HDR)) )
| SpecACSL ->
- C_backend_header.((module C_backend_spec.HdrMod : MODIFIERS_HDR))
+ ( C_backend_src.((module C_backend_spec.SrcMod : MODIFIERS_SRC)),
+ C_backend_header.((module C_backend_spec.HdrMod : MODIFIERS_HDR)) )
| SpecC ->
assert false
(* not implemented yet *)
in
- let module Header = C_backend_header.Main ((val header_m)) in
+ let module Header = C_backend_header.Main ((val source_m)) ((val header_m)) in
let destname = !dest_dir ^ "/" ^ basename in
(* Generating H file *)
let lusic = Lusic.read_lusic destname ".lusic" in
@@ -160,7 +162,7 @@ let translate_to_c generate_c_header basename prog machines dependencies =
assert false
(* not implemented yet *)
in
- let module Header = C_backend_header.Main ((val header_m)) in
+ let module Header = C_backend_header.Main ((val source_m)) ((val header_m)) in
let module Source = C_backend_src.Main ((val source_m)) in
let module SourceMain = C_backend_main.Main ((val source_main_m)) in
let module Makefile = C_backend_makefile.Main ((val makefile_m)) in
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 4e955f73..d8081226 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -150,6 +150,7 @@ let pp_machine_static_alloc_name ?(ghost = false) fmt id =
let pp_machine_set_reset_name fmt id = fprintf fmt "%s_set_reset" id
let pp_machine_clear_reset_name fmt id = fprintf fmt "%s_clear_reset" id
+let pp_machine_ghost_reset_name fmt id = fprintf fmt "%s_reset_ghost" id
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
@@ -773,7 +774,8 @@ let pp_machine_struct ?(ghost = false) fmt m =
(* Define struct *)
fprintf
fmt
- "@[<v 2>%a {@,_Bool _reset;%a%a@]@,};"
+ (if ghost then "@[<v 2>%a {%a%a@]@,};"
+ else "@[<v 2>%a {@,_Bool _reset;%a%a@]@,};")
(pp_machine_memtype_name ~ghost)
m.mname.node_id
(if ghost && not m.mis_contract then
@@ -866,17 +868,28 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
(pp_print_only_if (not is_contract) (Mod.pp_ghost_parameters ~cut:true))
[ mem, pp_mem_ghost name ]
- let pp_set_reset_prototype is_contract self mem fmt (name, static) =
+ (* let pp_set_reset_prototype is_contract self mem fmt (name, static) = *)
+ (* fprintf *)
+ (* fmt *)
+ (* "@[<v>void %a(%a%t)%a@]" *)
+ (* pp_machine_set_reset_name *)
+ (* name *)
+ (* (pp_comma_list ~pp_eol:pp_print_comma pp_c_decl_input_var) *)
+ (* static *)
+ (* (pp_self is_contract self mem name) *)
+ (* (pp_print_only_if (not is_contract) (Mod.pp_ghost_parameters ~cut:true)) *)
+ (* [ mem, pp_mem_ghost name ] *)
+
+ let pp_ghost_reset_prototype mem fmt (name, static) =
fprintf
fmt
- "@[<v>void %a(%a%t)%a@]"
- pp_machine_set_reset_name
+ "@[<v>void %a(%a%a)@]"
+ pp_machine_ghost_reset_name
name
(pp_comma_list ~pp_eol:pp_print_comma pp_c_decl_input_var)
static
- (pp_self is_contract self mem name)
- (pp_print_only_if (not is_contract) (Mod.pp_ghost_parameters ~cut:true))
- [ mem, pp_mem_ghost name ]
+ (pp_mem_ghost name)
+ mem
let pp_ghost_proto fmt (mem_name, proto_c) =
let ghost_c =
@@ -896,13 +909,17 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
l)
in
match mem_name, proto_c with
- | None, None -> ()
+ | None, None ->
+ ()
| _ ->
- Mod.pp_ghost_parameters ~cut:true fmt
+ Mod.pp_ghost_parameters
+ ~cut:true
+ fmt
(match mem_name with
- | Some (mem, name) ->
- (mem, pp_mem_ghost name) :: ghost_c
- | None -> ghost_c)
+ | Some (mem, name) ->
+ (mem, pp_mem_ghost name) :: ghost_c
+ | None ->
+ ghost_c)
let pp_step_prototype is_contract self mem fmt (name, inputs, outputs, proto_c)
=
diff --git a/src/backends/C/c_backend_common.mli b/src/backends/C/c_backend_common.mli
index 8901985c..a8bdf18b 100644
--- a/src/backends/C/c_backend_common.mli
+++ b/src/backends/C/c_backend_common.mli
@@ -9,6 +9,7 @@ val pp_put_var : formatter -> string -> ident -> Types.t -> ident -> unit
val pp_ptr : formatter -> ident -> unit
val pp_machine_set_reset_name : formatter -> ident -> unit
val pp_machine_clear_reset_name : formatter -> ident -> unit
+val pp_machine_ghost_reset_name : formatter -> ident -> unit
val pp_machine_init_name : formatter -> ident -> unit
val pp_machine_clear_name : formatter -> ident -> unit
val pp_machine_step_name : formatter -> ident -> unit
@@ -220,15 +221,21 @@ module EmptyGhostProto : MODIFIERS_GHOST_PROTO
module Protos (Mod : MODIFIERS_GHOST_PROTO) : sig
val pp_stateless_prototype :
- formatter -> ident * var_decl list * var_decl list
+ formatter ->
+ ident
+ * var_decl list
+ * var_decl list
* (ident option * ident * var_decl list * var_decl list) option ->
unit
val pp_clear_reset_prototype :
bool -> ident -> ident -> formatter -> ident * var_decl list -> unit
- val pp_set_reset_prototype :
- bool -> ident -> ident -> formatter -> ident * var_decl list -> unit
+ (* val pp_set_reset_prototype : *)
+ (* bool -> ident -> ident -> formatter -> ident * var_decl list -> unit *)
+
+ val pp_ghost_reset_prototype :
+ ident -> formatter -> ident * var_decl list -> unit
val pp_step_prototype :
bool ->
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index bd88949a..002c58a2 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -48,466 +48,475 @@ module EmptyMod = struct
let pp_machine_alloc_decl _ _ = ()
end
-module Main =
-functor
- (Mod : MODIFIERS_HDR)
- ->
- struct
- module Protos = Protos (Mod.GhostProto)
+module Main (ModSrc : C_backend_src.MODIFIERS_SRC) (ModHdr : MODIFIERS_HDR) =
+struct
+ module Protos = Protos (ModHdr.GhostProto)
+ module Src = C_backend_src.Main (ModSrc)
- let pp_import_standard fmt () =
- (* if Machine_types.has_machine_type () then *)
- fprintf
- fmt
- "#include <stdint.h>@,%a%a"
- (if !Options.mpfr then pp_print_endcut "#include <mpfr.h>"
- else pp_print_nothing)
- ()
- Mod.pp_import_arrow
- ()
+ let pp_import_standard fmt () =
+ (* if Machine_types.has_machine_type () then *)
+ fprintf
+ fmt
+ "#include <stdint.h>@,%a%a"
+ (if !Options.mpfr then pp_print_endcut "#include <mpfr.h>"
+ else pp_print_nothing)
+ ()
+ ModHdr.pp_import_arrow
+ ()
- (* TODO: ACSL we do multiple things: - provide the semantics of the node as
- a predicate: function step and reset are associated to ACSL predicate -
- the node is associated to a refinement contract, wrt its ACSL sem - if
- the node is a regular node associated to a contract, print the contract
- as function contract. - do not print anything if this is a contract
- node *)
- let pp_machine_alloc_decl fmt m =
- Mod.pp_machine_decl_prefix fmt m;
- if not (fst (get_stateless_status m)) then
- if !Options.static_mem then
- (* Static allocation *)
- let macro = m, mk_attribute m, mk_instance m in
- fprintf
- fmt
- "%a@,%a@,%a"
- (fun x -> pp_static_declare_macro x)
- macro
- (fun x -> pp_static_link_macro x)
- macro
- (fun x -> pp_static_alloc_macro x)
- macro
- else
- (* Dynamic allocation *)
- fprintf
- fmt
- "extern %a;@,extern %a"
- pp_alloc_prototype
- (m.mname.node_id, m.mstatic)
- pp_dealloc_prototype
- m.mname.node_id
+ (* TODO: ACSL we do multiple things: - provide the semantics of the node as a
+ predicate: function step and reset are associated to ACSL predicate - the
+ node is associated to a refinement contract, wrt its ACSL sem - if the node
+ is a regular node associated to a contract, print the contract as function
+ contract. - do not print anything if this is a contract node *)
+ let pp_machine_alloc_decl fmt m =
+ ModHdr.pp_machine_decl_prefix fmt m;
+ if not (fst (get_stateless_status m)) then
+ if !Options.static_mem then
+ (* Static allocation *)
+ let macro = m, mk_attribute m, mk_instance m in
+ fprintf
+ fmt
+ "%a@,%a@,%a"
+ (fun x -> pp_static_declare_macro x)
+ macro
+ (fun x -> pp_static_link_macro x)
+ macro
+ (fun x -> pp_static_alloc_macro x)
+ macro
+ else
+ (* Dynamic allocation *)
+ fprintf
+ fmt
+ "extern %a;@,extern %a"
+ pp_alloc_prototype
+ (m.mname.node_id, m.mstatic)
+ pp_dealloc_prototype
+ m.mname.node_id
- let pp_machine_struct_top_decl_from_header fmt tdecl =
- let inode = imported_node_of_top tdecl in
- if not (inode.nodei_stateless || inode.nodei_iscontract) then
- (* Declare struct *)
- fprintf fmt "%a;" (pp_machine_memtype_name ~ghost:false) inode.nodei_id
+ let pp_machine_struct_top_decl_from_header fmt tdecl =
+ let inode = imported_node_of_top tdecl in
+ if not (inode.nodei_stateless || inode.nodei_iscontract) then
+ (* Declare struct *)
+ fprintf fmt "%a;" (pp_machine_memtype_name ~ghost:false) inode.nodei_id
- let pp_stateless_C_prototype fmt (name, inputs, outputs) =
- let output = match outputs with [ hd ] -> hd | _ -> assert false in
- fprintf
- fmt
- "%a %s %a"
- (fun x -> pp_basic_c_type ~pp_c_basic_type_desc x)
- output.var_type
- name
- (pp_print_parenthesized pp_c_decl_input_var)
- inputs
+ let pp_stateless_C_prototype fmt (name, inputs, outputs) =
+ let output = match outputs with [ hd ] -> hd | _ -> assert false in
+ fprintf
+ fmt
+ "%a %s %a"
+ (fun x -> pp_basic_c_type ~pp_c_basic_type_desc x)
+ output.var_type
+ name
+ (pp_print_parenthesized pp_c_decl_input_var)
+ inputs
- let pp_machine_decl_top_decl_from_header nodes fmt tdecl =
- let inode = imported_node_of_top tdecl in
- (*Mod.print_machine_decl_prefix fmt m;*)
- let used name =
- List.exists
- (fun v -> v.var_id = name)
- (inode.nodei_inputs @ inode.nodei_outputs)
- in
- let self = mk_new_name used "self" in
- let mem = mk_new_name used "mem" in
- let proto_c =
- match inode.nodei_spec with
- | Some spec -> (
- match spec with
- | Contract _ ->
- None
- | NodeSpec f -> (
- let td =
- List.find
- (fun td ->
- match td.top_decl_desc with
- | Node nd ->
- nd.node_id = f
- | ImportedNode ind ->
- ind.nodei_id = f
- | _ ->
- false)
- nodes
- in
- let stateless = fst (get_stateless_status_top_decl td) in
- let mem_c =
- if stateless then None else Some (mk_new_name used "mem_c")
- in
- match td.top_decl_desc with
- | Node nd -> (
- match nd.node_spec with
- | Some (Contract _) ->
- Some (mem_c, f, nd.node_inputs, nd.node_outputs)
- | _ ->
- None)
- | ImportedNode ind -> (
- match ind.nodei_spec with
- | Some (Contract _) ->
- Some (mem_c, f, ind.nodei_inputs, ind.nodei_outputs)
- | _ ->
- None)
- | _ ->
- None))
- | None ->
+ let pp_set_reset_macro self fmt name =
+ fprintf
+ fmt
+ "#define %a(%s) {%a = 1;}"
+ pp_machine_set_reset_name
+ name
+ self
+ (pp_reset_flag (fun fmt -> fprintf fmt "(%s)") ~indirect:true)
+ self
+
+ let pp_machine_decl_top_decl_from_header nodes fmt tdecl =
+ let inode = imported_node_of_top tdecl in
+ (*ModHdr.print_machine_decl_prefix fmt m;*)
+ let used name =
+ List.exists
+ (fun v -> v.var_id = name)
+ (inode.nodei_inputs @ inode.nodei_outputs)
+ in
+ let self = mk_new_name used "self" in
+ let mem = mk_new_name used "mem" in
+ let proto_c =
+ match inode.nodei_spec with
+ | Some spec -> (
+ match spec with
+ | Contract _ ->
None
- in
- let prototype = inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs in
- let prototype' =
- inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs, proto_c
- in
- if not inode.nodei_iscontract then
- if inode.nodei_prototype = Some "C" then
- if inode.nodei_stateless then
- fprintf fmt "extern %a;" pp_stateless_C_prototype prototype
- else (
- (* TODO: raise proper error *)
- Format.eprintf
- "internal error: pp_machine_decl_top_decl_from_header";
- assert false)
- else if inode.nodei_stateless then
- fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype'
- else
- let static_inputs =
- List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
+ | NodeSpec f -> (
+ let td =
+ List.find
+ (fun td ->
+ match td.top_decl_desc with
+ | Node nd ->
+ nd.node_id = f
+ | ImportedNode ind ->
+ ind.nodei_id = f
+ | _ ->
+ false)
+ nodes
+ in
+ let stateless = fst (get_stateless_status_top_decl td) in
+ let mem_c =
+ if stateless then None else Some (mk_new_name used "mem_c")
in
- let static_prototype = inode.nodei_id, static_inputs in
- fprintf
- fmt
- "extern %a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;"
- (Protos.pp_set_reset_prototype false self mem)
- static_prototype
- (Protos.pp_clear_reset_prototype false self mem)
- static_prototype
- (Protos.pp_init_prototype self)
- static_prototype
- (Protos.pp_clear_prototype self)
- static_prototype
- (Protos.pp_step_prototype false self mem)
- prototype'
+ match td.top_decl_desc with
+ | Node nd -> (
+ match nd.node_spec with
+ | Some (Contract _) ->
+ Some (mem_c, f, nd.node_inputs, nd.node_outputs)
+ | _ ->
+ None)
+ | ImportedNode ind -> (
+ match ind.nodei_spec with
+ | Some (Contract _) ->
+ Some (mem_c, f, ind.nodei_inputs, ind.nodei_outputs)
+ | _ ->
+ None)
+ | _ ->
+ None))
+ | None ->
+ None
+ in
+ let prototype = inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs in
+ let prototype' =
+ inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs, proto_c
+ in
+ if not inode.nodei_iscontract then
+ if inode.nodei_prototype = Some "C" then
+ if inode.nodei_stateless then
+ fprintf fmt "extern %a;" pp_stateless_C_prototype prototype
+ else (
+ (* TODO: raise proper error *)
+ Format.eprintf "internal error: pp_machine_decl_top_decl_from_header";
+ assert false)
+ else if inode.nodei_stateless then
+ fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype'
else
- Mod.pp_is_contract
- (fun fmt ->
- if inode.nodei_stateless then
- fprintf fmt "%a;" Protos.pp_stateless_prototype prototype'
- else
- let static_inputs =
- List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
- in
- let static_prototype = inode.nodei_id, static_inputs in
- fprintf
- fmt
- "%a;@,%a;@,%a;"
- (Protos.pp_set_reset_prototype true self mem)
- static_prototype
- (Protos.pp_clear_reset_prototype true self mem)
- static_prototype
- (Protos.pp_step_prototype true self mem)
- prototype')
+ let static_inputs =
+ List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
+ in
+ let static_prototype = inode.nodei_id, static_inputs in
+ fprintf
fmt
+ "%a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;"
+ (pp_set_reset_macro self)
+ inode.nodei_id
+ (Protos.pp_clear_reset_prototype false self mem)
+ static_prototype
+ (Protos.pp_init_prototype self)
+ static_prototype
+ (Protos.pp_clear_prototype self)
+ static_prototype
+ (Protos.pp_step_prototype false self mem)
+ prototype'
+ else
+ ModHdr.pp_is_contract
+ (fun fmt ->
+ if inode.nodei_stateless then
+ fprintf fmt "%a;" Protos.pp_stateless_prototype prototype'
+ else
+ let static_inputs =
+ List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
+ in
+ let static_prototype = inode.nodei_id, static_inputs in
+ fprintf
+ fmt
+ "%a;@,%a;@,%a;"
+ (pp_set_reset_macro self)
+ inode.nodei_id
+ (Protos.pp_clear_reset_prototype true self mem)
+ static_prototype
+ (Protos.pp_step_prototype true self mem)
+ prototype')
+ fmt
+
+ let pp_const_top_decl fmt tdecl =
+ let cdecl = const_of_top tdecl in
+ fprintf
+ fmt
+ "extern %a;"
+ (pp_c_type cdecl.const_id)
+ (if
+ !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
+ then Types.dynamic_type cdecl.const_type
+ else cdecl.const_type)
- let pp_const_top_decl fmt tdecl =
- let cdecl = const_of_top tdecl in
+ let rec pp_c_type_decl filename cpt var fmt tdecl =
+ match tdecl with
+ | Tydec_any ->
+ assert false
+ | Tydec_int ->
+ fprintf fmt "int %s" var
+ | Tydec_real when !Options.mpfr ->
+ fprintf fmt "%s %s" Mpfr.mpfr_t var
+ | Tydec_real ->
+ fprintf fmt "double %s" var
+ (* | Tydec_float -> fprintf fmt "float %s" var *)
+ | Tydec_bool ->
+ fprintf fmt "_Bool %s" var
+ | Tydec_clock ty ->
+ pp_c_type_decl filename cpt var fmt ty
+ | Tydec_const c ->
+ fprintf fmt "%s %s" c var
+ | Tydec_array (d, ty) ->
+ fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d
+ | Tydec_enum tl ->
+ incr cpt;
fprintf
fmt
- "extern %a;"
- (pp_c_type cdecl.const_id)
- (if
- !Options.mpfr
- && Types.(is_real_type (array_base_type cdecl.const_type))
- then Types.dynamic_type cdecl.const_type
- else cdecl.const_type)
+ "enum _enum_%s_%d %a %s"
+ (protect_filename filename)
+ !cpt
+ (pp_print_braced pp_print_string)
+ (List.sort compare tl)
+ var
+ | Tydec_struct fl ->
+ incr cpt;
+ fprintf
+ fmt
+ "struct _struct_%s_%d %a %s"
+ (protect_filename filename)
+ !cpt
+ (pp_print_braced ~pp_sep:pp_print_semicolon (fun fmt (label, tdesc) ->
+ pp_c_type_decl filename cpt label fmt tdesc))
+ fl
+ var
- let rec pp_c_type_decl filename cpt var fmt tdecl =
- match tdecl with
- | Tydec_any ->
- assert false
- | Tydec_int ->
- fprintf fmt "int %s" var
- | Tydec_real when !Options.mpfr ->
- fprintf fmt "%s %s" Mpfr.mpfr_t var
- | Tydec_real ->
- fprintf fmt "double %s" var
- (* | Tydec_float -> fprintf fmt "float %s" var *)
- | Tydec_bool ->
- fprintf fmt "_Bool %s" var
- | Tydec_clock ty ->
- pp_c_type_decl filename cpt var fmt ty
- | Tydec_const c ->
- fprintf fmt "%s %s" c var
- | Tydec_array (d, ty) ->
- fprintf
- fmt
- "%a[%a]"
- (pp_c_type_decl filename cpt var)
- ty
- pp_c_dimension
- d
- | Tydec_enum tl ->
- incr cpt;
- fprintf
- fmt
- "enum _enum_%s_%d %a %s"
- (protect_filename filename)
- !cpt
- (pp_print_braced pp_print_string)
- (List.sort compare tl)
- var
- | Tydec_struct fl ->
- incr cpt;
+ (* let print_type_definitions fmt filename =
+ * let cpt_type = ref 0 in
+ * Hashtbl.iter (fun typ decl ->
+ * match typ with
+ * | Tydec_const var ->
+ * begin match decl.top_decl_desc with
+ * | TypeDef tdef ->
+ * fprintf fmt "typedef %a;@.@."
+ * (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
+ * | _ -> assert false
+ * end
+ * | _ -> ()) type_table *)
+
+ let reset_type_definitions, pp_type_definition_top_decl_from_header =
+ let cpt_type = ref 0 in
+ ( (fun () -> cpt_type := 0),
+ fun filename fmt tdecl ->
+ let typ = typedef_of_top tdecl in
fprintf
fmt
- "struct _struct_%s_%d %a %s"
- (protect_filename filename)
- !cpt
- (pp_print_braced ~pp_sep:pp_print_semicolon (fun fmt (label, tdesc) ->
- pp_c_type_decl filename cpt label fmt tdesc))
- fl
- var
-
- (* let print_type_definitions fmt filename =
- * let cpt_type = ref 0 in
- * Hashtbl.iter (fun typ decl ->
- * match typ with
- * | Tydec_const var ->
- * begin match decl.top_decl_desc with
- * | TypeDef tdef ->
- * fprintf fmt "typedef %a;@.@."
- * (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
- * | _ -> assert false
- * end
- * | _ -> ()) type_table *)
-
- let reset_type_definitions, pp_type_definition_top_decl_from_header =
- let cpt_type = ref 0 in
- ( (fun () -> cpt_type := 0),
- fun filename fmt tdecl ->
- let typ = typedef_of_top tdecl in
- fprintf
- fmt
- "typedef %a;"
- (pp_c_type_decl filename cpt_type typ.tydef_id)
- typ.tydef_desc )
+ "typedef %a;"
+ (pp_c_type_decl filename cpt_type typ.tydef_id)
+ typ.tydef_desc )
- (********************************************************************************************)
- (* MAIN Header Printing functions *)
- (********************************************************************************************)
+ (********************************************************************************************)
+ (* MAIN Header Printing functions *)
+ (********************************************************************************************)
- let pp_alloc_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
- 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@,\
- @,\
- /* Import header from %s */@,\
- %a@,\
- /* 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
- pp_import_prototype
- 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 prototypes of all machines *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:
- (pp_print_endcut "/* Node allocation function/macro prototypes */")
- ~pp_sep:pp_print_cutcut
- pp_machine_alloc_decl
- ~pp_epilogue:pp_print_cutcut)
- machines'
- (* Print the spec prototypes of all machines *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:
- (pp_print_endcut
- "/* Node allocation function/macro ghost prototypes */")
- ~pp_sep:pp_print_cutcut
- Mod.pp_machine_alloc_decl
- ~pp_epilogue:pp_print_cutcut)
- machines'
- (* Include once: end *)
+ let pp_alloc_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
+ 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@,\
+ @,\
+ /* Import header from %s */@,\
+ %a@,\
+ /* 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
+ pp_import_prototype
+ 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 prototypes of all machines *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:
+ (pp_print_endcut "/* Node allocation function/macro prototypes */")
+ ~pp_sep:pp_print_cutcut
+ pp_machine_alloc_decl
+ ~pp_epilogue:pp_print_cutcut)
+ machines'
+ (* Print the spec prototypes of all machines *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:
+ (pp_print_endcut
+ "/* Node allocation function/macro ghost prototypes */")
+ ~pp_sep:pp_print_cutcut
+ ModHdr.pp_machine_alloc_decl
+ ~pp_epilogue:pp_print_cutcut)
+ machines'
+ (* Include once: end *)
- (* Function called when compiling a lusi file and generating the associated
- C header. *)
- let pp_header_from_header header_fmt basename header =
- (* Include once: start *)
- let baseNAME = file_to_module_name basename in
- let types = get_typedefs header in
- let consts = get_consts header in
- let nodes = get_imported_nodes header in
- let dependencies = get_dependencies header in
- reset_type_definitions ();
- fprintf
- header_fmt
- "@[<v>%a@,\
- #ifndef _%s@,\
- #define _%s@,\
- @,\
- /* Import standard library */@,\
- %a@,\
- @,\
- %a%a%a%a%a%a#endif@]@."
- (* Print the version number and the supported C standard (C90 or C99) *)
- pp_print_version
- ()
- baseNAME
- baseNAME
- (* imports standard library definitions (arrow) *)
- pp_import_standard
- ()
- (* imports dependencies *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
- (fun fmt dep ->
- let local, name = dependency_of_top dep in
- pp_import_prototype
- fmt
- {
- local;
- name;
- content = [];
- is_stateful = true (* assuming it is stateful *);
- })
- ~pp_epilogue:pp_print_cutcut)
- dependencies
- (* Print the type definitions from the type table *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:(pp_print_endcut "/* Types definitions */")
- (pp_type_definition_top_decl_from_header basename)
- ~pp_epilogue:pp_print_cutcut)
- types
- (* Print the global constant declarations. *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:
- (pp_print_endcut
- "/* Global constants (declarations, definitions are in C file) \
- */")
- pp_const_top_decl
- ~pp_epilogue:pp_print_cutcut)
- consts
- (* MPFR *)
- (if !Options.mpfr then fun fmt () ->
- fprintf
- fmt
- "/* Global initialization declaration */@,\
- extern %a;@,\
- @,\
- /* Global clear declaration */@,\
- extern %a;@,\
- @,"
- pp_global_init_prototype
- baseNAME
- pp_global_clear_prototype
- baseNAME
- else pp_print_nothing)
- ()
- (* Print the struct declarations of all machines. *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:(pp_print_endcut "/* Struct declarations */")
- pp_machine_struct_top_decl_from_header
- ~pp_epilogue:pp_print_cutcut)
- nodes
- (* Print the prototypes of all machines *)
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_prologue:(pp_print_endcut "/* Nodes declarations */")
- ~pp_sep:pp_print_cutcut
- (pp_machine_decl_top_decl_from_header nodes)
- ~pp_epilogue:pp_print_cutcut)
- nodes
+ (* Function called when compiling a lusi file and generating the associated C
+ header. *)
+ let pp_header_from_header header_fmt basename header =
+ (* Include once: start *)
+ let baseNAME = file_to_module_name basename in
+ let types = get_typedefs header in
+ let consts = get_consts header in
+ let nodes = List.rev (get_imported_nodes header) in
+ let dependencies = get_dependencies header in
+ reset_type_definitions ();
+ fprintf
+ header_fmt
+ "@[<v>%a@,\
+ #ifndef _%s@,\
+ #define _%s@,\
+ @,\
+ /* Import standard library */@,\
+ %a@,\
+ @,\
+ %a%a%a%a%a%a#endif@]@."
+ (* Print the version number and the supported C standard (C90 or C99) *)
+ pp_print_version
+ ()
+ baseNAME
+ baseNAME
+ (* imports standard library definitions (arrow) *)
+ pp_import_standard
+ ()
+ (* imports dependencies *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
+ (fun fmt dep ->
+ let local, name = dependency_of_top dep in
+ pp_import_prototype
+ fmt
+ {
+ local;
+ name;
+ content = [];
+ is_stateful = true (* assuming it is stateful *);
+ })
+ ~pp_epilogue:pp_print_cutcut)
+ dependencies
+ (* Print the type definitions from the type table *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:(pp_print_endcut "/* Types definitions */")
+ (pp_type_definition_top_decl_from_header basename)
+ ~pp_epilogue:pp_print_cutcut)
+ types
+ (* Print the global constant declarations. *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:
+ (pp_print_endcut
+ "/* Global constants (declarations, definitions are in C file) */")
+ pp_const_top_decl
+ ~pp_epilogue:pp_print_cutcut)
+ consts
+ (* MPFR *)
+ (if !Options.mpfr then fun fmt () ->
+ fprintf
+ fmt
+ "/* Global initialization declaration */@,\
+ extern %a;@,\
+ @,\
+ /* Global clear declaration */@,\
+ extern %a;@,\
+ @,"
+ pp_global_init_prototype
+ baseNAME
+ pp_global_clear_prototype
+ baseNAME
+ else pp_print_nothing)
+ ()
+ (* Print the struct declarations of all machines. *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:(pp_print_endcut "/* Struct declarations */")
+ pp_machine_struct_top_decl_from_header
+ ~pp_epilogue:pp_print_cutcut)
+ nodes
+ (* Print the prototypes of all machines *)
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_prologue:(pp_print_endcut "/* Nodes declarations */")
+ ~pp_sep:pp_print_cutcut
+ (pp_machine_decl_top_decl_from_header nodes)
+ ~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_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
+ let pp_spec_header header_fmt basename machines _dependencies =
+ let baseNAME = file_to_module_name basename in
+ 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
+ header_fmt
+ "@[<v>%a@,#ifndef _%s_SPEC@,#define _%s_SPEC@,@,%a@,%a#endif@]@."
+ (* Print the svn version number and the supported C standard (C90 or
+ C99) *)
+ pp_print_version
+ ()
+ baseNAME
+ baseNAME
+ ModHdr.pp_predicates
+ machines
+ (pp_preds "/* Monolithic ghost `reset` functions */" (fun fmt m ->
+ let mem = mk_mem m in
+ Src.pp_ghost_reset_spec_code machines mem fmt m))
+ machines
+end
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
(* End: *)
diff --git a/src/backends/C/c_backend_header.mli b/src/backends/C/c_backend_header.mli
index e167ee2a..013eb746 100644
--- a/src/backends/C/c_backend_header.mli
+++ b/src/backends/C/c_backend_header.mli
@@ -15,7 +15,7 @@ end
module EmptyMod : MODIFIERS_HDR
-module Main (Mod : MODIFIERS_HDR) : sig
+module Main (ModSrc : C_backend_src.MODIFIERS_SRC) (ModHdr : MODIFIERS_HDR) : sig
val pp_header_from_header : formatter -> string -> top_decl list -> unit
val pp_alloc_header :
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 4668a9f6..534426bc 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -42,8 +42,7 @@ let pp_acsl ?(ghost = false) pp fmt x =
let pp_acsl_cut ?ghost pp fmt = fprintf fmt "%a@," (pp_acsl ?ghost pp)
let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp
-let pp_acsl_line_cut pp fmt =
- fprintf fmt "%a@," (pp_acsl_line pp)
+let pp_acsl_line_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line pp)
let pp_acsl_line' ?(ghost = false) pp fmt x =
let op = if ghost then "" else "*" in
@@ -194,6 +193,8 @@ let pp_not pp fmt = fprintf fmt "!%a" pp
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x)
let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp
+let pre_label = "Pre"
+let pp_at pp l fmt x = fprintf fmt "\\at(%a, %s)" pp x l
let pp_ite pp_c pp_t pp_f fmt (c, t, f) =
fprintf fmt "(%a @[<hov>? %a@ : %a)@]" pp_c c pp_t t pp_f f
@@ -333,18 +334,6 @@ let pp_reset_set pp_mem fmt (name, mem) =
let pp_reset_set' = pp_reset_set pp_print_string
-let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
- fprintf
- fmt
- "%s_reset_cleared(@[<hov>%a,@ %a@])"
- name
- pp_mem_in
- mem_in
- pp_mem_out
- mem_out
-
-let pp_reset_cleared' = pp_reset_cleared pp_print_string pp_print_string
-
let pp_functional_update mems insts fmt mem =
let rec aux fmt = function
| [] ->
@@ -373,12 +362,6 @@ module PrintSpec = struct
| ResetOut
| InstrMode of ident
- let pp_reg mem fmt = function
- | ResetFlag ->
- fprintf fmt "%s.%s" mem reset_flag_name
- | StateVar x ->
- fprintf fmt "%s.%a" mem pp_var_decl x
-
let not_var v = match v.value_desc with Var _ -> false | _ -> true
let is_const v = match v.value_desc with Cst _ -> true | _ -> false
@@ -398,7 +381,7 @@ module PrintSpec = struct
| Var v ->
pp_var_decl fmt v
| Memory r ->
- pp_reg mem fmt r
+ fprintf fmt "%s.%a" mem pp_var_decl r
let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =
let test_output, mem_update =
@@ -433,13 +416,14 @@ module PrintSpec = struct
(pp_expr test_output)
fmt
(f, vars, mem_in', mem_out')
- | Reset (_f, inst, r) ->
+ | Reset (f, inst, r) ->
pp_ite
(pp_c_val m mem_in (pp_c_var_read m))
- (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
+ pp_initialization'
+ (* (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int) *)
(pp_equal pp_print_string pp_access')
fmt
- (r, (mem_out, 1), (mem_out, (mem_in, inst)))
+ (r, (f, mem_out), (mem_out, (mem_in, inst)))
| MemoryPackBase f ->
pp_memory_pack_base_aux
pp_print_string
@@ -462,11 +446,6 @@ module PrintSpec = struct
pp_print_string
fmt
(f, mem_in', mem_out, mem_in))
- | ResetCleared f ->
- pp_reset_cleared' fmt (f, mem_in, mem_out)
- (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
- | Initialization ->
- ()
| GhostAssign (v1, v2) ->
pp_ghost (pp_assign m mem_in (pp_c_var_read m)) fmt (v1, vdecl_to_val v2)
@@ -479,10 +458,8 @@ module PrintSpec = struct
id_to_tag t
| Var v ->
vdecl_to_val v
- | Memory (StateVar v) ->
+ | Memory v ->
vdecl_to_val v
- | Memory ResetFlag ->
- vdecl_to_val reset_flag
let find_arrow_val =
let bad_inits = Hashtbl.create 32 in
@@ -536,7 +513,10 @@ module PrintSpec = struct
| ResetOut ->
mem_in, mem_in, false, mem_reset, mem_reset, false
| InstrMode self ->
- let mem = "(*" ^ mem ^ ")" in
+ pp_at pp_ptr pre_label str_formatter mem;
+ let mem_reset = flush_str_formatter () in
+ fprintf str_formatter "(%a)" pp_ptr mem;
+ let mem = flush_str_formatter () in
self, mem_reset, false, mem, mem, false
in
let pp_expr fmt e = pp_expr m mem_in' fmt e in
@@ -607,19 +587,7 @@ module PrintSpec = struct
inst
| Predicate p ->
pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p
- | StateVarPack (ResetFlag, _) ->
- let r = vdecl_to_val reset_flag in
- pp_assign_spec
- m
- mem_out
- (pp_c_var_read ~test_output:false m)
- indirect_l
- mem_in
- (pp_c_var_read ~test_output:false m)
- indirect_r
- fmt
- (Type_predef.type_bool, r, r)
- | StateVarPack (StateVar v, tainted) ->
+ | StateVarPack (v, tainted) ->
let v' = vdecl_to_val v in
let pp_eq fmt () =
pp_assign_spec
@@ -654,6 +622,17 @@ module PrintSpec = struct
((f, mk_mem_reset m), (rc, tr))
| Value v ->
pp_c_val m mem_in (pp_c_var_read ~test_output:true m) fmt v
+ | MemoryPackToplevel (f, i) ->
+ pp_ite
+ (pp_reset_flag' ~indirect:true)
+ pp_initialization'
+ (pp_memory_pack_aux_taint
+ ~i
+ pp_print_string
+ pp_print_string
+ pp_print_string)
+ fmt
+ (mem_in, (f, mem_out), (f, mem_out, mem_out, mem_in))
in
pp_spec mode fmt (Spec_common.red f)
@@ -691,9 +670,11 @@ let pp_memory_pack_base_def m fmt f =
(pp_memory_pack_base_aux
(pp_machine_decl' ~ghost:true)
(pp_machine_decl pp_ptr))
- (PrintSpec.pp_spec MemoryPackMode m))
+ (pp_and
+ (pp_equal (pp_reset_flag' ~indirect:true) pp_print_int)
+ (PrintSpec.pp_spec MemoryPackMode m)))
fmt
- ((name, (name, mem), (name, self)), f)
+ ((name, (name, mem), (name, self)), ((self, 0), f))
let pp_memory_pack_def m fmt mp =
if not (fst (get_stateless_status m) || m.mis_contract) then
@@ -728,9 +709,7 @@ let pp_memory_pack_defs fmt m =
if not (fst (get_stateless_status m)) then
fprintf
fmt
- "%a@,%a%a"
- pp_machine_ghost_struct
- m
+ "%a%a"
(pp_memory_pack_base_def m)
m.mspec.mmemory_pack_base
(pp_print_list
@@ -845,48 +824,10 @@ let pp_initialization_def fmt m =
(pp_predicate
(pp_initialization (pp_machine_decl' ~ghost:true))
(pp_and_l (fun fmt (i, (td, _)) ->
- if Arrow.td_is_arrow td then
- pp_initialization pp_access' fmt (node_name td, (mem_in, i))
- else
- pp_equal
- (pp_reset_flag ~indirect:false pp_access')
- pp_print_int
- fmt
- ((mem_in, i), 1))))
+ pp_initialization pp_access' fmt (node_name td, (mem_in, i)))))
fmt
((name, (name, mem_in)), m.minstances)
-let pp_reset_set_def fmt m =
- if not (fst (get_stateless_status m)) then
- let name = m.mname.node_id in
- let mem = mk_mem m in
- pp_acsl
- (pp_predicate
- (pp_reset_set (pp_machine_decl' ~ghost:true))
- (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int))
- fmt
- ((name, (name, mem)), (mem, 1))
-
-let pp_reset_cleared_def fmt m =
- if not (fst (get_stateless_status m)) then
- let name = m.mname.node_id in
- let mem_in = mk_mem_in m in
- let mem_out = mk_mem_out m in
- pp_acsl
- (pp_predicate
- (pp_reset_cleared
- (pp_machine_decl' ~ghost:true)
- (pp_machine_decl' ~ghost:true))
- (pp_ite
- (pp_reset_flag' ~indirect:false)
- (pp_and
- (pp_equal (pp_reset_flag' ~indirect:false) pp_print_int)
- pp_initialization')
- (pp_equal pp_print_string pp_print_string)))
- fmt
- ( (name, (name, mem_in), (name, mem_out)),
- (mem_in, ((mem_out, 0), (name, mem_out)), (mem_out, mem_in)) )
-
let pp_register_chain ?(indirect = true) ptr =
pp_print_list
~pp_prologue:(fun fmt () -> fprintf fmt "%s->" ptr)
@@ -1136,16 +1077,14 @@ module HdrMod = struct
in
fprintf
fmt
- "%a%a%a%a%a%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)
+ (pp_preds "/* ACSL ghost structures */" pp_machine_ghost_struct)
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)
+ (pp_preds "/* ACSL `memory pack` simulations */" pp_memory_pack_defs)
machines
(pp_preds "/* ACSL transition annotations */" pp_transition_defs)
machines
@@ -1236,7 +1175,7 @@ module SrcMod = struct
(fun fmt () ->
fprintf
fmt
- "%a%a%a%a%a%a%a%a%a%a%a"
+ "%a%a%a%a%a%a%a"
(pp_if_not_contract (pp_requires pp_mem_valid'))
(name, self)
(pp_if_not_contract (pp_requires (pp_separated' self mem)))
@@ -1252,39 +1191,67 @@ module SrcMod = struct
pp_ptr
pp_print_string)))
(name, mem, mem, self)
- (pp_ensures (pp_reset_cleared (pp_old pp_ptr) pp_ptr))
- (name, mem, mem)
(pp_if_not_contract (pp_assigns pp_reset_flag'))
[ self ]
(pp_if_not_contract (pp_assigns (pp_register_chain self)))
(mk_insts arws)
(pp_if_not_contract (pp_assigns (pp_reset_flag_chain self)))
- (mk_insts narws)
- (pp_assigns pp_reset_flag')
- [ mem ]
- (pp_assigns (pp_register_chain ~indirect:false mem))
- (mk_insts arws)
- (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
(mk_insts narws))
fmt
()
- let pp_set_reset_spec fmt self mem m =
+ (* let pp_set_reset_spec fmt machines self mem m = *)
+ (* let name = m.mname.node_id in *)
+ (* let insts = instances machines m in *)
+ (* let stateful_insts = *)
+ (* List.( *)
+ (* filter *)
+ (* (fun path -> *)
+ (* let _, (_, mems) = hd (rev path) in *)
+ (* mems <> []) *)
+ (* insts) *)
+ (* in *)
+ (* let pp_if_not_contract pp = pp_print_only_if (not m.mis_contract) pp in *)
+ (* pp_acsl_cut *)
+ (* ~ghost:m.mis_contract *)
+ (* (fun fmt () -> *)
+ (* fprintf *)
+ (* fmt *)
+ (* "%a%a%a%a" *)
+ (* (pp_if_not_contract *)
+ (* (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))) *)
+ (* (name, mem, self) *)
+ (* (pp_if_not_contract *)
+ (* (pp_ensures (pp_initialization pp_ptr))) *)
+ (* (name, mem) *)
+ (* (pp_assigns pp_reset_flag') *)
+ (* (if m.mis_contract then [ ] else [ self ]) *)
+ (* (pp_assigns (pp_reg ~indirect:false mem)) *)
+ (* stateful_insts) *)
+ (* fmt *)
+ (* () *)
+
+ let pp_ghost_reset_spec fmt machines mem m =
let name = m.mname.node_id in
- let pp_if_not_contract pp = pp_print_only_if (not m.mis_contract) pp in
+ let insts = instances machines m in
+ let stateful_insts =
+ List.(
+ filter
+ (fun path ->
+ let _, (_, mems) = hd (rev path) in
+ mems <> [])
+ insts)
+ in
pp_acsl_cut
- ~ghost:m.mis_contract
+ ~ghost:true
(fun fmt () ->
fprintf
fmt
- "%a%a%a"
- (pp_if_not_contract
- (pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string)))
- (name, mem, self)
- (pp_ensures (pp_reset_set pp_ptr))
+ "%a%a"
+ (pp_ensures (pp_initialization pp_ptr))
(name, mem)
- (pp_assigns pp_reset_flag')
- (if m.mis_contract then [ mem ] else [ self; mem ]))
+ (pp_assigns (pp_reg ~indirect:false mem))
+ stateful_insts)
fmt
()
@@ -1466,7 +1433,7 @@ module SrcMod = struct
else
fprintf
fmt
- "%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a"
+ "%a%a%a%a%a%a%a%a%a%a%a%a%a%a"
(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
outputs
(pp_if_not_contract (pp_requires pp_mem_valid'))
@@ -1508,33 +1475,45 @@ module SrcMod = struct
insts_no_arrow
(pp_print_only_if (m.mmemory <> []) (pp_assigns (pp_reg mem)))
[ [] ]
- (pp_assigns pp_reset_flag')
- [ mem ]
(pp_assigns (pp_reg ~indirect:false mem))
- stateful_insts
- (pp_assigns (pp_reset_flag_chain ~indirect:false mem))
- insts_no_arrow)
+ stateful_insts)
fmt
()
- let pp_ghost_instr_code m self fmt instr =
+ let pp_ghost_reset pp_mem name fmt mem =
+ fprintf fmt "%a(%a);" pp_machine_ghost_reset_name name pp_mem mem
+
+ let pp_ghost_instr_code m mem fmt instr =
match instr.instr_desc with
| MStateAssign (x, v) ->
fprintf
fmt
"@,%a"
- (pp_acsl_line (pp_ghost (pp_assign m self (pp_c_var_read m))))
+ (pp_acsl_line' (pp_ghost (pp_assign m mem (pp_c_var_read m))))
(x, v)
- | MResetAssign b ->
- fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b
+ (* | MResetAssign b -> *)
+ (* fprintf fmt "@,%a" (pp_acsl_line (pp_ghost (pp_reset_assign self))) b *)
| MSetReset inst ->
- let td, _ = List.assoc inst m.minstances in
- if Arrow.td_is_arrow td then
- fprintf
- fmt
- "@,%a;"
- (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self)))
- inst
+ let name =
+ let node, _ =
+ try List.assoc inst m.minstances with Not_found -> assert false
+ in
+ node_name node
+ in
+ fprintf
+ fmt
+ "@,%a"
+ (pp_acsl_line'
+ (pp_ghost
+ (pp_ghost_reset (pp_indirect pp_ref' pp_print_string) name)))
+ (mem, inst)
+ (* let td, _ = List.assoc inst m.minstances in *)
+ (* if Arrow.td_is_arrow td then *)
+ (* fprintf *)
+ (* fmt *)
+ (* "@,%a;" *)
+ (* (pp_acsl_line (pp_ghost (pp_arrow_reset_ghost self))) *)
+ (* inst *)
| _ ->
()
@@ -1590,19 +1569,19 @@ module SrcMod = struct
in
List.fold_left gather VSet.empty m.mstep.step_instrs |> VSet.elements
- let pp_ghost_reset_memory m fmt mem =
- let name = m.mname.node_id in
- let mem_r = mk_mem_reset m in
- let pp fmt () =
- fprintf
- fmt
- "%a = %a;"
- (pp_machine_decl' ~ghost:true)
- (name, mem_r)
- pp_ptr
- mem
- in
- (if m.mis_contract then pp else pp_acsl_line' (pp_ghost pp)) fmt ()
+ (* let pp_ghost_reset_memory m fmt mem = *)
+ (* let name = m.mname.node_id in *)
+ (* let mem_r = mk_mem_reset m in *)
+ (* let pp fmt () = *)
+ (* fprintf *)
+ (* fmt *)
+ (* "%a = %a;" *)
+ (* (pp_machine_decl' ~ghost:true) *)
+ (* (name, mem_r) *)
+ (* pp_ptr *)
+ (* mem *)
+ (* in *)
+ (* (if m.mis_contract then pp else pp_acsl_line' (pp_ghost pp)) fmt () *)
end
module MainMod = struct
@@ -1647,7 +1626,9 @@ module MainMod = struct
(pp_print_option (fun fmt m_c ->
let stateless_c = fst (get_stateless_status m_c) in
let name_c = m_c.mname.node_id in
- pp_print_only_if (not stateless_c) (fun fmt ->
+ pp_print_only_if
+ (not stateless_c)
+ (fun fmt ->
fprintf
fmt
"@;%a"
@@ -1677,17 +1658,17 @@ module MainMod = struct
GhostProto.pp_ghost_parameters
~cut:false
fmt
- (if stateless then proto_c else
- (mk_main_mem_ghost m, pp_ref pp_print_string)
- :: proto_c)
+ (if stateless then proto_c
+ else (mk_main_mem_ghost m, pp_ref pp_print_string) :: proto_c)
let pp_main_loop_invariants main_mem machines fmt m =
let name = m.mname.node_id in
let insts = instances machines m in
let c, m_c = contract_of machines m in
- let m_c_k = match c, m_c with
+ let m_c_k =
+ match c, m_c with
| Some c, Some m_c -> (
- match c.mc_proof with Some (Kinduction k) -> Some (m_c, k) | _ -> None)
+ match c.mc_proof with Some (Kinduction k) -> Some (m_c, k) | _ -> None)
| _ ->
None
in
@@ -1697,7 +1678,8 @@ module MainMod = struct
fmt
"%a%a%a"
(pp_print_option (fun fmt _ ->
- pp_print_option (fun fmt m_c ->
+ pp_print_option
+ (fun fmt m_c ->
pp_acsl_cut
(pp_ghost
(pp_print_list
@@ -1707,7 +1689,8 @@ module MainMod = struct
(pp_local m_c)))
fmt
m_c.mstep.step_outputs)
- fmt m_c))
+ fmt
+ m_c))
c
(pp_print_option (fun fmt _ ->
fprintf
@@ -1720,22 +1703,27 @@ module MainMod = struct
fprintf
fmt
"%a%a%a%a%a"
- (pp_print_only_if (not stateless) (pp_loop_invariant pp_mem_valid'))
+ (pp_print_only_if
+ (not stateless)
+ (pp_loop_invariant pp_mem_valid'))
(name, main_mem)
- (pp_print_only_if (not stateless)
+ (pp_print_only_if
+ (not stateless)
(pp_loop_invariant
(pp_memory_pack_aux pp_print_string pp_print_string)))
(name, mk_main_mem_ghost m, main_mem)
- (fun fmt (_, _, _, outputs as x) ->
- if stateless then
- (if List.length outputs > 1 then
- pp_loop_invariant pp_separated'' fmt outputs)
- else
- pp_loop_invariant
+ (fun fmt ((_, _, _, outputs) as x) ->
+ if stateless then (
+ if List.length outputs > 1 then
+ pp_loop_invariant pp_separated'' fmt outputs)
+ else
+ pp_loop_invariant
(pp_separated
(pp_paren pp_print_string)
pp_ref'
- (pp_ref pp_var_decl)) fmt x)
+ (pp_ref pp_var_decl))
+ fmt
+ x)
(main_mem, mk_main_mem_ghost m, insts, m.mstep.step_outputs)
(pp_loop_invariant
(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
@@ -1791,23 +1779,25 @@ module MainMod = struct
fmt
"@,%a"
(pp_print_option (fun fmt c ->
- pp_print_option (fun fmt _ ->
+ pp_print_option
+ (fun fmt _ ->
fprintf
fmt
"%a%a"
(match c.mc_proof with
- | Some (Kinduction _) ->
- pp_acsl_line_cut (pp_ghost (fun fmt -> fprintf fmt "%s++;"))
- | None -> pp_print_nothing)
+ | Some (Kinduction _) ->
+ pp_acsl_line_cut (pp_ghost (fun fmt -> fprintf fmt "%s++;"))
+ | None ->
+ pp_print_nothing)
(mk_k m)
(pp_acsl_line'
- (pp_assert
- (PrintSpec.pp_spec TransitionMode m)))
+ (pp_assert (PrintSpec.pp_spec TransitionMode m)))
(spec_from_contract c))
- (* (pp_and_l (fun fmt v -> *)
- (* pp_equal pp_var_decl pp_print_int fmt (v, 1))))) *)
- (* m_c.mstep.step_outputs) *)
- fmt m_c))
+ (* (pp_and_l (fun fmt v -> *)
+ (* pp_equal pp_var_decl pp_print_int fmt (v, 1))))) *)
+ (* m_c.mstep.step_outputs) *)
+ fmt
+ m_c))
c
let pp_main_spec fmt =
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 2cb2ce25..e47d1374 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -22,9 +22,14 @@ module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
val pp_import_spec_prototype : formatter -> dep_t -> unit
- val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
+
+ (* val pp_set_reset_spec : formatter -> machine_t list -> ident -> ident ->
+ machine_t -> unit *)
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
+ val pp_ghost_reset_spec :
+ formatter -> machine_t list -> ident -> machine_t -> unit
+
val pp_step_spec :
formatter -> machine_t list -> ident -> ident -> machine_t -> unit
@@ -34,7 +39,8 @@ module type MODIFIERS_SRC = sig
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
val pp_c_decl_local_spec_var : machine_t -> formatter -> var_decl -> unit
val get_spec_locals : machine_t -> var_decl list
- val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit
+
+ (* val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit *)
val pp_is_contract : (formatter -> unit) -> formatter -> unit
val pp_contract_arrow_reset_name : formatter -> unit
val pp_contract_arrow_step_name : formatter -> unit
@@ -45,24 +51,29 @@ module type MODIFIERS_SRC = sig
formatter ->
unit ->
unit
+
+ (* val pp_ghost_reset: machine_t -> ident -> formatter -> unit -> unit *)
end
module EmptyMod = struct
module GhostProto = EmptyGhostProto
let pp_import_spec_prototype _ _ = ()
- let pp_set_reset_spec _ _ _ _ = ()
+ let pp_set_reset_spec _ _ _ _ _ = ()
let pp_clear_reset_spec _ _ _ _ = ()
+ let pp_ghost_reset_spec _ _ _ _ = ()
let pp_step_spec _ _ _ _ _ = ()
let pp_step_instr_spec _ _ _ _ _ = ()
let pp_ghost_parameter _ _ _ = ()
let pp_c_decl_local_spec_var _ _ _ = ()
let get_spec_locals _ = []
- let pp_ghost_reset_memory _ _ _ = ()
+
+ (* let pp_ghost_reset_memory _ _ _ = () *)
let pp_is_contract _ _ = ()
let pp_contract_arrow_reset_name _ = ()
let pp_contract_arrow_step_name _ = ()
let pp_contract_step_call _ _ _ _ = ()
+ (* let pp_ghost_reset _ _ _ _ = () *)
end
module Main (Mod : MODIFIERS_SRC) = struct
@@ -141,22 +152,23 @@ module Main (Mod : MODIFIERS_SRC) = struct
| None ->
m.mname.node_id, false, []
in
- let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
+ let is_set_reset = fn_name = "pp_machine_set_reset" in
+ let is_ghost_reset = fn_name = "pp_machine_ghost_reset" in
fprintf
fmt
"%a(%a%s%a)%a;"
(fun fmt name ->
- if is_arrow_reset then
+ if is_set_reset && is_arrow then
if m.mis_contract then Mod.pp_contract_arrow_reset_name fmt
else fprintf fmt "%s_reset" Arrow.arrow_id
else pp_machine_name fmt name)
name
(pp_comma_list ~pp_eol:pp_print_comma Dimension.pp)
static
- self
+ (if is_ghost_reset && not is_arrow then "&" ^ self else self)
(pp_print_option (fun fmt -> fprintf fmt "->%s"))
inst
- (if is_arrow_reset || m.mis_contract then pp_print_nothing
+ (if is_set_reset || m.mis_contract then pp_print_nothing
else Mod.pp_ghost_parameter mem)
inst
@@ -179,6 +191,16 @@ module Main (Mod : MODIFIERS_SRC) = struct
self
mem
+ let pp_machine_ghost_reset m mem fmt inst =
+ pp_machine_
+ pp_machine_ghost_reset_name
+ "pp_machine_ghost_reset"
+ { m with mis_contract = true }
+ fmt
+ ~inst
+ mem
+ mem
+
let pp_machine_init m self mem fmt inst =
pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
@@ -272,12 +294,13 @@ module Main (Mod : MODIFIERS_SRC) = struct
reset_loop_counter ();
aux [] fmt (List.hd inputs).Machine_code_types.value_type
- let rec pp_conditional dependencies m self mem fmt c tl el =
+ let rec pp_conditional ?(with_spec = true) dependencies m self mem fmt c tl el
+ =
let pp_machine_instrs =
pp_print_list
~pp_open_box:pp_open_vbox0
~pp_prologue:pp_print_cut
- (pp_machine_instr dependencies m self mem)
+ (pp_machine_instr ~with_spec dependencies m self mem)
in
let pp_cond = pp_c_val m self (pp_c_var_read m) in
match tl, el with
@@ -296,7 +319,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
pp_machine_instrs
el
- and pp_machine_instr dependencies m self mem fmt instr =
+ and pp_machine_instr ?(with_spec = true) dependencies m self mem fmt instr =
let self = if m.mis_contract then mem else self in
let pp_instr fmt instr =
match get_instr_desc instr with
@@ -306,12 +329,12 @@ module Main (Mod : MODIFIERS_SRC) = struct
pp_machine_set_reset m self mem fmt inst
| MClearReset ->
if not (fst (get_stateless_status m)) then
- fprintf
- fmt
- "%t@,%a"
- (pp_machine_clear_reset m self mem)
- (Mod.pp_ghost_reset_memory m)
- mem
+ (* fprintf *)
+ (* fmt *)
+ (* "%t@,%a" *)
+ (pp_machine_clear_reset m self mem) fmt
+ (* (Mod.pp_ghost_reset_memory m) *)
+ (* mem *)
| MResetAssign b ->
pp_reset_assign self fmt b
| MLocalAssign (i, v) ->
@@ -322,6 +345,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
when Basic_library.is_value_internal_fun
(mk_val (Fun (i, vl)) i0.var_type) ->
pp_machine_instr
+ ~with_spec
dependencies
m
self
@@ -369,6 +393,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
match i.instr_desc with MNoReset _ -> false | _ -> true)
in
pp_conditional
+ ~with_spec
dependencies
m
self
@@ -388,16 +413,30 @@ module Main (Mod : MODIFIERS_SRC) = struct
g
(pp_print_list_i
~pp_open_box:pp_open_vbox0
- (pp_machine_branch dependencies m self mem (List.length hl)))
+ (pp_machine_branch
+ ~with_spec
+ dependencies
+ m
+ self
+ mem
+ (List.length hl)))
hl
| MSpec s ->
fprintf fmt "@[/*@@ %s */@]@ " s
| MComment s ->
fprintf fmt "/* %s */" s
in
- fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
+ fprintf
+ fmt
+ "%a%a"
+ pp_instr
+ instr
+ (if with_spec then Mod.pp_step_instr_spec m self mem
+ else pp_print_nothing)
+ instr
- and pp_machine_branch dependencies m self mem n fmt i (t, h) =
+ and pp_machine_branch ?(with_spec = true) dependencies m self mem n fmt i
+ (t, h) =
fprintf
fmt
(if n > 1 && i = n - 1 then "@[<v 2>default: // %a@,%a@]"
@@ -406,7 +445,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
t
(pp_print_list
~pp_open_box:pp_open_vbox0
- (pp_machine_instr dependencies m self mem))
+ (pp_machine_instr ~with_spec dependencies m self mem))
h
(* let pp_machine_nospec_instr dependencies m self fmt instr =
@@ -636,11 +675,11 @@ module Main (Mod : MODIFIERS_SRC) = struct
Option.bind c (fun _ ->
Option.map
(fun m_c ->
- let stateless_c = fst (get_stateless_status m_c) in
- ( (if stateless_c then None else Some (mk_mem_c m)),
- m_c.mname.node_id,
- m_c.mstep.step_inputs,
- m_c.mstep.step_outputs ))
+ let stateless_c = fst (get_stateless_status m_c) in
+ ( (if stateless_c then None else Some (mk_mem_c m)),
+ m_c.mname.node_id,
+ m_c.mstep.step_inputs,
+ m_c.mstep.step_outputs ))
m_c)
let pp_stateless_code machines dependencies fmt m =
@@ -653,7 +692,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
~is_contract
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
~pp_prototype:Protos.pp_stateless_prototype
- ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, proto_c)
+ ~prototype:
+ (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, proto_c)
~pp_local:(pp_c_decl_local_var m)
~base_locals:m.mstep.step_locals
~pp_spec_local:(Mod.pp_c_decl_local_spec_var m)
@@ -688,7 +728,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
( m.mname.node_id,
m.mstep.step_inputs @ gen_locals @ gen_calls,
m.mstep.step_outputs,
- proto_c)
+ proto_c )
~pp_local:(pp_c_decl_local_var m)
~base_locals
~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
@@ -710,7 +750,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~prototype:(m.mname.node_id, m.mstatic)
~pp_local:(pp_c_decl_local_var m)
~base_locals:(const_locals m)
- ~pp_instr:(pp_machine_instr dependencies m self mem)
+ ~pp_instr:(pp_machine_instr ~with_spec:false dependencies m self mem)
~instrs:
[
mk_branch
@@ -719,17 +759,46 @@ module Main (Mod : MODIFIERS_SRC) = struct
]
fmt
- let pp_set_reset_code dependencies self mem fmt m =
- let is_contract = m.mis_contract in
+ let pp_ghost_reset_spec_code machines mem fmt m =
+ let pp_instr fmt i =
+ match get_instr_desc i with
+ | MSetReset inst ->
+ pp_machine_ghost_reset m mem fmt inst
+ | _ ->
+ assert false
+ in
pp_print_function
- ~is_contract
- ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
- ~pp_prototype:(Protos.pp_set_reset_prototype is_contract self mem)
+ ~is_contract:true
+ ~pp_spec:(fun fmt () -> Mod.pp_ghost_reset_spec fmt machines mem m)
+ ~pp_prototype:(Protos.pp_ghost_reset_prototype mem)
~prototype:(m.mname.node_id, m.mstatic)
- ~pp_instr:(pp_machine_instr dependencies m self mem)
- ~instrs:[ mkinstr (MResetAssign true) ]
+ ~pp_instr
+ ~instrs:m.minit
fmt
+ (* let pp_set_reset_code machines dependencies self mem fmt m = *)
+ (* let prototype = m.mname.node_id, m.mstatic in *)
+ (* let pp_instr fmt i = *)
+ (* match get_instr_desc i with *)
+ (* | MSetReset inst -> *)
+ (* pp_machine_ghost_reset m mem fmt inst *)
+ (* | _ -> assert false *)
+ (* in *)
+ (* in *)
+ (* let is_contract = m.mis_contract in *)
+ (* pp_print_function *)
+ (* ~is_contract *)
+ (* ~pp_spec:(fun fmt () -> *)
+ (* fprintf fmt "%t@;%a" *)
+ (* pp_ghost_reset *)
+ (* (fun fmt () -> Mod.pp_set_reset_spec fmt machines self mem m) ()) *)
+ (* ~pp_prototype:(Protos.pp_set_reset_prototype is_contract self mem) *)
+ (* ~prototype *)
+ (* ~pp_instr:(pp_machine_instr dependencies m self mem) *)
+ (* ~instrs:[ mkinstr (MResetAssign true) ] *)
+ (* ~pp_extra:(Mod.pp_ghost_reset m mem) *)
+ (* fmt *)
+
let pp_init_code self fmt m =
let minit =
List.map
@@ -1006,14 +1075,12 @@ module Main (Mod : MODIFIERS_SRC) = struct
let mem = mk_mem m in
fprintf
fmt
- "@[<v>%a%a@,@,%a@,@,%a%a@]"
+ "@[<v>%a%a@,@,%a%a@]"
pp_alloc_function
m
- (* Reset functions *)
+ (* Reset function *)
(pp_clear_reset_code dependencies self mem)
m
- (pp_set_reset_code dependencies self mem)
- m
(* Step function *)
(pp_step_code machines dependencies self mem)
m
diff --git a/src/backends/C/c_backend_src.mli b/src/backends/C/c_backend_src.mli
index d894abda..98168f33 100644
--- a/src/backends/C/c_backend_src.mli
+++ b/src/backends/C/c_backend_src.mli
@@ -8,9 +8,14 @@ module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
val pp_import_spec_prototype : formatter -> dep_t -> unit
- val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
+
+ (* val pp_set_reset_spec : formatter -> machine_t list -> ident -> ident ->
+ machine_t -> unit *)
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
+ val pp_ghost_reset_spec :
+ formatter -> machine_t list -> ident -> machine_t -> unit
+
val pp_step_spec :
formatter -> machine_t list -> ident -> ident -> machine_t -> unit
@@ -20,7 +25,8 @@ module type MODIFIERS_SRC = sig
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
val pp_c_decl_local_spec_var : machine_t -> formatter -> var_decl -> unit
val get_spec_locals : machine_t -> var_decl list
- val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit
+
+ (* val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit *)
val pp_is_contract : (formatter -> unit) -> formatter -> unit
val pp_contract_arrow_reset_name : formatter -> unit
val pp_contract_arrow_step_name : formatter -> unit
@@ -31,6 +37,8 @@ module type MODIFIERS_SRC = sig
formatter ->
unit ->
unit
+
+ (* val pp_ghost_reset: machine_t -> ident -> formatter -> unit -> unit *)
end
module EmptyMod : MODIFIERS_SRC
@@ -38,4 +46,7 @@ module EmptyMod : MODIFIERS_SRC
module Main (Mod : MODIFIERS_SRC) : sig
val pp_lib_c :
formatter -> string -> program_t -> machine_t list -> dep_t list -> unit
+
+ val pp_ghost_reset_spec_code :
+ machine_t list -> ident -> formatter -> machine_t -> unit
end
diff --git a/src/machine_code.ml b/src/machine_code.ml
index d90f135f..6338fbc4 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -212,9 +212,7 @@ let ctx_init =
si = [];
j = IMap.empty;
s = [];
- mp_base =
- And
- [ StateVarPack (ResetFlag, false); Equal (Memory ResetFlag, Val zero) ];
+ mp_base = True;
tainted = ISet.empty;
mp = [];
t = [];
@@ -547,20 +545,14 @@ let memory_pack_0 nd mems =
VSet.fold
(fun v a -> And [ a; mk_state_variable_pack v ])
mems
- (mk_memory_pack_base nd.node_id)
- (* And [ StateVarPack (ResetFlag, false); Equal (Memory ResetFlag, Val
- zero) ]; *);
+ (mk_memory_pack_base nd.node_id);
}
let memory_pack_toplevel nd i =
{
mpname = nd;
mpindex = None;
- mpformula =
- Ternary
- ( Memory ResetFlag,
- StateVarPack (ResetFlag, false),
- mk_memory_pack ~i nd.node_id );
+ mpformula = MemoryPackToplevel (nd.node_id, i);
}
let transition_0 nd =
@@ -568,9 +560,7 @@ let transition_0 nd =
tname = nd;
tindex = Some 0;
tvars = nd.node_inputs;
- tformula =
- (if fst (get_stateless_status_node nd) then True
- else StateVarPack (ResetFlag, false));
+ tformula = True;
tmem_footprint = ISet.empty;
tinst_footprint = IMap.empty;
}
@@ -588,9 +578,7 @@ let transition_toplevel nd i =
tname = nd;
tindex = None;
tvars = nd.node_inputs @ nd.node_outputs;
- tformula =
- (if fst (get_stateless_status_node nd) then tr
- else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
+ tformula = tr;
tmem_footprint = ISet.empty;
tinst_footprint = IMap.empty;
}
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index c0110d9e..b6cc3e8c 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -37,12 +37,6 @@ let rec pp_val m fmt v =
fprintf fmt "RESET"
module PrintSpec = struct
- let pp_reg fmt = function
- | ResetFlag ->
- pp_print_string fmt "{RESET}"
- | StateVar v ->
- fprintf fmt "{OUT:%a}" pp_vdecl v
-
let pp_expr m fmt = function
| Val v ->
pp_val m fmt v
@@ -51,7 +45,7 @@ module PrintSpec = struct
| Var v ->
pp_vdecl fmt v
| Memory r ->
- pp_reg fmt r
+ fprintf fmt "{OUT:%a}" pp_vdecl r
let pp_predicate m fmt p =
let pp_expr fmt e = pp_expr m fmt e in
@@ -94,10 +88,6 @@ module PrintSpec = struct
inst
(pp_print_option pp_print_int)
i
- | ResetCleared f ->
- fprintf fmt "ResetCleared_%a" pp_print_string f
- | Initialization ->
- ()
| GhostAssign (v1, v2) ->
fprintf fmt "Ghost %s = %s" v1.var_id v2.var_id
@@ -161,12 +151,20 @@ module PrintSpec = struct
"StateVarPack%a<%a>"
(if tainted then pp_print_string else pp_print_nothing)
"_tainted"
- pp_reg
+ pp_vdecl
r
| ExistsMem (_f, a, b) ->
fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
| Value v ->
pp_val m fmt v
+ | MemoryPackToplevel (f, i) ->
+ fprintf
+ fmt
+ "If RESET Then FULLRESET(%a) Else (@[<hov>%a@])"
+ pp_print_string
+ f
+ (pp_predicate m)
+ (MemoryPack (f, None, Some i))
in
pp_spec
diff --git a/src/spec_common.ml b/src/spec_common.ml
index 342fca6b..853e9a41 100644
--- a/src/spec_common.ml
+++ b/src/spec_common.ml
@@ -12,9 +12,7 @@ let type_of_value = function
t
| Var v ->
v.var_type
- | Memory ResetFlag ->
- Type_predef.type_bool
- | Memory (StateVar v) ->
+ | Memory v ->
v.var_type
let expr_eq a b = a = b
@@ -110,11 +108,8 @@ let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst
let mk_memory_pack ?i ?inst id = mk_pred_call (MemoryPack (id, inst, i))
let mk_memory_pack_base id = mk_pred_call (MemoryPackBase id)
-
-let mk_state_variable_pack ?(tainted = false) x =
- StateVarPack (StateVar x, tainted)
-
-let mk_state_assign_tr x v = Equal (Memory (StateVar x), Val v)
+let mk_state_variable_pack ?(tainted = false) x = StateVarPack (x, tainted)
+let mk_state_assign_tr x v = Equal (Memory x, Val v)
let mk_conditional_tr v t f = Ternary (Val v, t, f)
let mk_branch_tr x =
diff --git a/src/spec_types.ml b/src/spec_types.ml
index 5f0230b6..bdfcb53b 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -1,13 +1,11 @@
open Utils
open Lustre_types
-type register_t = ResetFlag | StateVar of var_decl
-
type 'a expression_t =
| Val of 'a
| Tag of ident * Types.t
| Var of var_decl
- | Memory of register_t
+ | Memory of var_decl
type 'a predicate_t =
| Transition :
@@ -27,8 +25,6 @@ type 'a predicate_t =
| Reset of ident * ident * 'a
| MemoryPack of ident * ident option * int option
| MemoryPackBase of ident
- | Initialization
- | ResetCleared of ident
| GhostAssign of var_decl * var_decl
type 'a formula_t =
@@ -43,9 +39,10 @@ type 'a formula_t =
| Forall of var_decl list * 'a formula_t
| Ternary of 'a expression_t * 'a formula_t * 'a formula_t
| Predicate : 'a predicate_t -> 'a formula_t
- | StateVarPack of register_t * bool (* tainted or not *)
+ | StateVarPack of var_decl * bool (* tainted or not *)
| ExistsMem of ident * 'a formula_t * 'a formula_t
| Value of 'a
+ | MemoryPackToplevel of ident * int
(* type 'a simulation_t = {
* sname: node_desc;
diff --git a/src/spec_types.mli b/src/spec_types.mli
index faff8b07..41749288 100644
--- a/src/spec_types.mli
+++ b/src/spec_types.mli
@@ -1,13 +1,11 @@
open Utils
open Lustre_types
-type register_t = ResetFlag | StateVar of var_decl
-
type 'a expression_t =
| Val of 'a
| Tag of ident * Types.t
| Var of var_decl
- | Memory of register_t
+ | Memory of var_decl
type 'a predicate_t =
| Transition :
@@ -27,8 +25,6 @@ type 'a predicate_t =
| Reset of ident * ident * 'a
| MemoryPack of ident * ident option * int option
| MemoryPackBase of ident
- | Initialization
- | ResetCleared of ident
| GhostAssign of var_decl * var_decl
type 'a formula_t =
@@ -43,9 +39,10 @@ type 'a formula_t =
| Forall of var_decl list * 'a formula_t
| Ternary of 'a expression_t * 'a formula_t * 'a formula_t
| Predicate : 'a predicate_t -> 'a formula_t
- | StateVarPack of register_t * bool (* tainted or not *)
+ | StateVarPack of var_decl * bool (* tainted or not *)
| ExistsMem of ident * 'a formula_t * 'a formula_t
| Value of 'a
+ | MemoryPackToplevel of ident * int
type 'a transition_t = {
tname : node_desc;
diff --git a/src/tools/tiny/tiny_verifier.ml b/src/tools/tiny/tiny_verifier.ml
index b10405e5..c18e1ed7 100644
--- a/src/tools/tiny/tiny_verifier.ml
+++ b/src/tools/tiny/tiny_verifier.ml
@@ -5,7 +5,6 @@ let descending = ref 1
let unrolling = ref 0
let output = ref false
let reachtube = ref false (* used to produce a list of set iterates *)
-
let quiet () = Tiny.Report.verbosity := 0
let report = Tiny_utils.report
diff --git a/strategy.ml b/strategy.ml
index feec6326..c6a50d77 100644
--- a/strategy.ml
+++ b/strategy.ml
@@ -136,7 +136,6 @@ let rec unify (push : Strategy.strategy -> unit) (sequent : Conditions.sequent)
class lustrec_transitions : Strategy.heuristic =
object
method id = "LustreC:Transitions" (* required, must be unique *)
-
method title = "LustreC Transitions"
method descr = "Custom goal transformations for transition relations"
@@ -166,7 +165,6 @@ class lustrec_transitions : Strategy.heuristic =
class lustrec_reset_cleared : Strategy.heuristic =
object
method id = "LustreC:ResetCleared" (* required, must be unique *)
-
method title = "LustreC ResetCleared"
method descr = "Custom goal transformations for reset_cleared relations"
@@ -256,7 +254,6 @@ let unfold_rec_strategy = Strategy.make (new unfold_rec) ~arguments:[]
class lustrec_memory_packs : Strategy.heuristic =
object
method id = "LustreC:MemoryPacks" (* required, must be unique *)
-
method title = "LustreC MemoryPacks"
method descr = "Custom goal transformations for memory_pack relations"
--
GitLab