From 241ef2a4bbec0523e29151fbf657a66691070932 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Tue, 5 Jul 2022 09:38:05 +0200
Subject: [PATCH] corrections to handle stateless / statefull
---
src/backends/C/c_backend_common.ml | 51 ++++++----
src/backends/C/c_backend_common.mli | 4 +-
src/backends/C/c_backend_header.ml | 4 +-
src/backends/C/c_backend_main.ml | 4 +-
src/backends/C/c_backend_spec.ml | 139 ++++++++++++++++------------
src/backends/C/c_backend_src.ml | 33 ++++---
6 files changed, 140 insertions(+), 95 deletions(-)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index f26b7eb1..4e955f73 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -878,6 +878,32 @@ 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_ghost_proto fmt (mem_name, proto_c) =
+ let ghost_c =
+ match proto_c with
+ | None ->
+ []
+ | Some (mem_c, name_c, _, outputs_c) -> (
+ let l =
+ List.map
+ (fun v -> "", fun fmt _ -> pp_c_decl_output_var fmt v)
+ outputs_c
+ in
+ match mem_c with
+ | Some mem_c ->
+ (mem_c, pp_mem_ghost name_c) :: l
+ | None ->
+ l)
+ in
+ match mem_name, proto_c with
+ | None, None -> ()
+ | _ ->
+ Mod.pp_ghost_parameters ~cut:true fmt
+ (match mem_name with
+ | 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)
=
fprintf
@@ -894,23 +920,8 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
pp_c_decl_output_var)
outputs
(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)
- ::
- (match proto_c with
- | None ->
- []
- | Some (mem_c, name_c, _, outputs_c) -> (
- let l =
- List.map
- (fun v -> "", fun fmt _ -> pp_c_decl_output_var fmt v)
- outputs_c
- in
- match mem_c with
- | Some mem_c ->
- (mem_c, pp_mem_ghost name_c) :: l
- | None ->
- l)))
+ (pp_print_only_if (not is_contract) pp_ghost_proto)
+ (Some (mem, name), proto_c)
let pp_init_prototype self fmt (name, static) =
fprintf
@@ -936,16 +947,18 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
name
self
- let pp_stateless_prototype fmt (name, inputs, outputs) =
+ let pp_stateless_prototype fmt (name, inputs, outputs, proto_c) =
fprintf
fmt
- "void %a (@[<v>%a%a@])"
+ "@[<v>void %a (@[<v>%a%a@])%a@]"
pp_machine_step_name
name
(pp_comma_list pp_c_decl_input_var)
inputs
(pp_comma_list ~pp_prologue:pp_print_comma pp_c_decl_output_var)
outputs
+ pp_ghost_proto
+ (None, proto_c)
end
let pp_import_prototype fmt dep = fprintf fmt "#include \"%s.h\"@," dep.name
diff --git a/src/backends/C/c_backend_common.mli b/src/backends/C/c_backend_common.mli
index 7ebacfec..8901985c 100644
--- a/src/backends/C/c_backend_common.mli
+++ b/src/backends/C/c_backend_common.mli
@@ -220,7 +220,9 @@ module EmptyGhostProto : MODIFIERS_GHOST_PROTO
module Protos (Mod : MODIFIERS_GHOST_PROTO) : sig
val pp_stateless_prototype :
- formatter -> ident * var_decl list * var_decl list -> unit
+ 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
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 14ca01aa..bd88949a 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -179,7 +179,7 @@ functor
"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
+ fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype'
else
let static_inputs =
List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
@@ -202,7 +202,7 @@ functor
Mod.pp_is_contract
(fun fmt ->
if inode.nodei_stateless then
- fprintf fmt "%a;" Protos.pp_stateless_prototype prototype
+ fprintf fmt "%a;" Protos.pp_stateless_prototype prototype'
else
let static_inputs =
List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 5228ef94..14bb64af 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -289,13 +289,15 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
if fst (get_stateless_status m) then
fprintf
fmt
- "%a(%a%a);"
+ "%a(%a%a)%a;"
pp_machine_step_name
mname
pp_inputs
inputs
(pp_outputs ~pp_eol:pp_print_nothing)
outputs
+ (Mod.pp_ghost_state_parameter m)
+ m_c
else
fprintf
fmt
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 86ff0c3d..4668a9f6 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -42,6 +42,8 @@ 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' ?(ghost = false) pp fmt x =
let op = if ghost then "" else "*" in
@@ -1102,6 +1104,8 @@ let pp_proof_annotation m m_c fmt c =
| None ->
()
+let spec_from_contract c = Spec_common.red (Imply (c.mc_pre, c.mc_post))
+
module GhostProto : MODIFIERS_GHOST_PROTO = struct
let pp_ghost_parameters ?(cut = true) fmt vs =
fprintf
@@ -1284,9 +1288,6 @@ module SrcMod = struct
fmt
()
- (** UNUSED *)
- (* let spec_from_contract c = Spec_common.red (Imply (c.mc_pre, c.mc_post)) *)
-
(** UNUSED *)
(* let pp_contract m fmt c = *)
(* PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c) *)
@@ -1380,6 +1381,7 @@ module SrcMod = struct
let outputs = m.mstep.step_outputs in
let stateless = fst (get_stateless_status m) in
let pp_if_outputs pp = pp_print_only_if (outputs = []) pp in
+ let pp_if_outputs' pp = pp_print_only_if (List.length outputs > 1) pp in
let pp_if_not_contract pp = pp_print_only_if (not m.mis_contract) pp in
let c, m_c = contract_of machines m in
let pp_spec =
@@ -1453,7 +1455,7 @@ module SrcMod = struct
"%a%a%a%a%a"
(pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
outputs
- (pp_if_outputs (pp_requires pp_separated''))
+ (pp_if_outputs' (pp_requires pp_separated''))
outputs
(pp_assigns pp_ptr_decl)
outputs
@@ -1645,34 +1647,21 @@ 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
- fprintf
+ pp_print_only_if (not stateless_c) (fun fmt ->
+ fprintf
+ fmt
+ "@;%a"
+ (pp_acsl_line'
+ (pp_ghost (fun fmt ->
+ fprintf fmt "%a;" (pp_machine_decl' ~ghost:true)))))
fmt
- "%a%a"
- (pp_print_only_if (not stateless_c) (fun fmt ->
- fprintf
- fmt
- "@;%a"
- (pp_acsl_line'_cut
- (pp_ghost (fun fmt ->
- fprintf fmt "%a;" (pp_machine_decl' ~ghost:true))))))
- (name_c, mk_main_mem_ghost_c m)
- (pp_acsl
- (pp_ghost
- (pp_print_list
- ~pp_open_box:pp_open_vbox0
- ~pp_sep:pp_print_semicolon
- ~pp_epilogue:pp_print_semicolon'
- (pp_local m_c))))
- m_c.mstep.step_outputs))
+ (name_c, mk_main_mem_ghost_c m)))
m_c
let pp_ghost_state_parameter m fmt m_c =
- GhostProto.pp_ghost_parameters
- ~cut:false
- fmt
- ((mk_main_mem_ghost m, pp_ref pp_print_string)
- ::
- (match m_c with
+ let stateless = fst (get_stateless_status m) in
+ let proto_c =
+ match m_c with
| None ->
[]
| Some m_c ->
@@ -1683,23 +1672,43 @@ module MainMod = struct
m_c.mstep.step_outputs
in
if stateless_c then l
- else (mk_main_mem_ghost_c m, pp_ref pp_print_string) :: l))
-
- let k_induction_of machines m =
- match contract_of machines m with
- | Some c, Some m_c -> (
- match c.mc_proof with Some (Kinduction k) -> Some (m_c, k) | _ -> None)
- | _ ->
- None
+ else (mk_main_mem_ghost_c m, pp_ref pp_print_string) :: l
+ in
+ 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)
let pp_main_loop_invariants main_mem machines fmt m =
let name = m.mname.node_id in
let insts = instances machines m in
- let m_c_k = k_induction_of machines m in
+ let c, m_c = contract_of machines m in
+ 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)
+ | _ ->
+ None
+ in
let var_k = mk_k m in
+ let stateless = fst (get_stateless_status m) in
fprintf
fmt
- "%a%a"
+ "%a%a%a"
+ (pp_print_option (fun fmt _ ->
+ pp_print_option (fun fmt m_c ->
+ pp_acsl_cut
+ (pp_ghost
+ (pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ ~pp_sep:pp_print_semicolon
+ ~pp_epilogue:pp_print_semicolon'
+ (pp_local m_c)))
+ fmt
+ m_c.mstep.step_outputs)
+ fmt m_c))
+ c
(pp_print_option (fun fmt _ ->
fprintf
fmt
@@ -1711,16 +1720,22 @@ module MainMod = struct
fprintf
fmt
"%a%a%a%a%a"
- (pp_loop_invariant pp_mem_valid')
+ (pp_print_only_if (not stateless) (pp_loop_invariant pp_mem_valid'))
(name, main_mem)
- (pp_loop_invariant
- (pp_memory_pack_aux pp_print_string pp_print_string))
+ (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)
- (pp_loop_invariant
- (pp_separated
- (pp_paren pp_print_string)
- pp_ref'
- (pp_ref pp_var_decl)))
+ (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)
(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)))
@@ -1771,21 +1786,29 @@ module MainMod = struct
()
let pp_main_loop_end _main_mem machines fmt m =
+ let c, m_c = contract_of machines m in
fprintf
fmt
"@,%a"
- (pp_print_option (fun fmt (m_c, _) ->
- fprintf
- fmt
- "%a@,%a"
- (pp_acsl_line (pp_ghost (fun fmt -> fprintf fmt "%s++;")))
- (mk_k m)
- (pp_acsl_line
- (pp_assert
- (pp_and_l (fun fmt v ->
- pp_equal pp_var_decl pp_print_int fmt (v, 1)))))
- m_c.mstep.step_outputs))
- (k_induction_of machines m)
+ (pp_print_option (fun fmt c ->
+ 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)
+ (mk_k m)
+ (pp_acsl_line'
+ (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))
+ c
let pp_main_spec fmt =
pp_acsl_cut
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 3cfd4a09..2cb2ce25 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -631,16 +631,29 @@ module Main (Mod : MODIFIERS_SRC) = struct
top_decl_itf = false;
}
+ let get_proto_c machines m =
+ let c, m_c = contract_of machines m in
+ 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 ))
+ m_c)
+
let pp_stateless_code machines dependencies fmt m =
let self = "__ERROR__" in
let is_contract = m.mis_contract in
+ let proto_c = get_proto_c machines m in
if not (!Options.ansi && is_generic_node (node_of_machine m)) then
(* C99 code *)
pp_print_function
~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)
+ ~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)
@@ -652,6 +665,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
+ ~pp_extra:(Mod.pp_contract_step_call m proto_c)
fmt
else
(* C90 code *)
@@ -673,7 +687,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
~prototype:
( m.mname.node_id,
m.mstep.step_inputs @ gen_locals @ gen_calls,
- m.mstep.step_outputs )
+ m.mstep.step_outputs,
+ 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))
@@ -683,6 +698,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
~checks:m.mstep.step_checks
~pp_instr:(pp_machine_instr dependencies m self self)
~instrs:m.mstep.step_instrs
+ ~pp_extra:(Mod.pp_contract_step_call m proto_c)
fmt
let pp_clear_reset_code dependencies self mem fmt m =
@@ -762,18 +778,7 @@ module Main (Mod : MODIFIERS_SRC) = struct
let pp_step_code machines dependencies self mem fmt m =
let is_contract = m.mis_contract in
- let c, m_c = contract_of machines m in
- let proto_c =
- 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 ))
- m_c)
- in
+ let proto_c = get_proto_c machines m in
if not (!Options.ansi && is_generic_node (node_of_machine m)) then
(* C99 code *)
pp_print_function
--
GitLab