From 85a7d54a8a06126ccc362240e12db5d114b80624 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 16:27:17 +0200
Subject: [PATCH] ACSL ok for main loop of stateless nodes
---
src/backends/C/c_backend_main.ml | 29 +++++---
src/backends/C/c_backend_main.mli | 3 +
src/backends/C/c_backend_spec.ml | 115 ++++++++++++++++++++++++------
3 files changed, 116 insertions(+), 31 deletions(-)
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 876ab82f..3f78e6aa 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -18,19 +18,25 @@ open C_backend_common
module Mpfr = Lustrec_mpfr
module type MODIFIERS_MAINSRC = sig
+
+ val pp_import_spec_prototype : formatter -> dep_t -> unit
val pp_declare_ghost_state : formatter -> ident -> unit
val pp_ghost_state_parameter : formatter -> unit -> unit
val pp_main_spec : formatter -> unit
val pp_main_loop_invariants :
ident -> machine_t list -> formatter -> machine_t -> unit
+ val pp_main_loop_end :
+ ident -> machine_t list -> formatter -> machine_t -> unit
end
module EmptyMod = struct
+ let pp_import_spec_prototype _ _ = ()
let pp_declare_ghost_state _ _ = ()
let pp_ghost_state_parameter _ _ = ()
let pp_main_spec _ = ()
let pp_main_loop_invariants _ _ _ _ = ()
+ let pp_main_loop_end _ _ _ _ = ()
end
module Main (Mod : MODIFIERS_MAINSRC) = struct
@@ -306,7 +312,7 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
/* Infinite loop */@,\
%a@[<v 2>while(1){@,\
fflush(stdout);@,\
- %a%a%a%a@]@,\
+ %a%a%a%a%a@]@,\
}"
(Mod.pp_main_loop_invariants main_mem machines)
m
@@ -337,6 +343,8 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
~pp_prologue:pp_print_cut
pp_put_output)
(m.mname.node_outputs, m.mstep.step_outputs)
+ (Mod.pp_main_loop_end main_mem machines)
+ m
let pp_usage fmt () =
fprintf
@@ -457,12 +465,20 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
()
let pp_main_c main_fmt main_machine basename _prog machines _dependencies =
+ let self_dep = {
+ local = true;
+ name = basename;
+ content = [];
+ is_stateful = true (* assuming it is stateful*);
+ }
+ in
fprintf
main_fmt
"@[<v>%a@,\
#include <stdlib.h>@,\
#include <assert.h>@,\
- %a@,\
+ %a\
+ %a\
@,\
%a@,\
%a\n\
@@ -470,12 +486,9 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
pp_main_header
()
pp_import_alloc_prototype
- {
- local = true;
- name = basename;
- content = [];
- is_stateful = true (* assuming it is stateful*);
- }
+ 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
diff --git a/src/backends/C/c_backend_main.mli b/src/backends/C/c_backend_main.mli
index e8135e8d..3dc18e6b 100644
--- a/src/backends/C/c_backend_main.mli
+++ b/src/backends/C/c_backend_main.mli
@@ -4,12 +4,15 @@ open Lustre_types
open Machine_code_types
module type MODIFIERS_MAINSRC = sig
+ val pp_import_spec_prototype : formatter -> dep_t -> unit
val pp_declare_ghost_state : formatter -> ident -> unit
val pp_ghost_state_parameter : formatter -> unit -> unit
val pp_main_spec : formatter -> unit
val pp_main_loop_invariants :
ident -> machine_t list -> formatter -> machine_t -> unit
+ val pp_main_loop_end :
+ ident -> machine_t list -> formatter -> machine_t -> unit
end
module EmptyMod : MODIFIERS_MAINSRC
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index fc8ae024..3c02b2bd 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -86,7 +86,6 @@ let pp_false fmt () = pp_print_string fmt "\\false"
let pp_nothing fmt () = pp_print_string fmt "\\nothing"
let pp_null fmt () = pp_print_string fmt "\\null"
let pp_stdout fmt () = pp_print_string fmt "stdout"
-let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l
let find_machine f = List.find (fun m -> m.mname.node_id = f)
let instances machines m =
@@ -134,7 +133,7 @@ let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =
pp_mem
mem
(pp_comma_list ~pp_prologue:pp_print_comma (fun fmt path ->
- pp_indirect pp_print_string pp_instance fmt (self, path)))
+ pp_indirect pp_self pp_instance fmt (self, path)))
paths
(pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)
ptrs
@@ -1150,7 +1149,7 @@ module HdrMod = struct
"/* 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)))
+ pp_print_option (pp_proof_annotation m m_c) fmt c))
machines
let pp_machine_decl_prefix _ _ = ()
@@ -1563,6 +1562,9 @@ module SrcMod = struct
end
module MainMod = struct
+
+ let pp_import_spec_prototype = SrcMod.pp_import_spec_prototype
+
let main_mem_ghost = "main_mem_ghost"
let pp_declare_ghost_state fmt name =
@@ -1583,31 +1585,98 @@ module MainMod = struct
fmt
[ main_mem_ghost, pp_ref pp_print_string ]
+ let k_induction_of machines m =
+ match contract_of machines m with
+ | Some c, Some m_c ->
+ begin match c.mc_proof with
+ | Some (Kinduction k) ->
+ Some (m_c, k)
+ | _ -> None
+ end
+ | _ -> None
+
let pp_main_loop_invariants main_mem machines fmt m =
let name = m.mname.node_id in
let insts = instances machines m in
- pp_acsl_cut
- (fun fmt () ->
- fprintf
- fmt
- "%a@,%a@,%a@,%a"
- (pp_loop_invariant pp_mem_valid')
- (name, main_mem)
- (pp_loop_invariant
- (pp_memory_pack_aux pp_print_string pp_print_string))
- (name, main_mem_ghost, main_mem)
- (pp_loop_invariant
- (pp_separated
- (pp_paren pp_print_string)
- pp_ref'
- (pp_ref pp_var_decl)))
- (main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
- (pp_loop_invariant
- (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
- ((), ((), ())))
- fmt
+ let m_c_k = k_induction_of machines m in
+ fprintf fmt "%a%a"
+ (pp_print_option
+ (fun fmt _ ->
+ fprintf fmt "%a@,"
+ (pp_acsl_line (pp_ghost pp_print_string)) "int __k = 0;"))
+ m_c_k
+ (pp_acsl_cut
+ (fun fmt () ->
+ fprintf
+ fmt
+ "%a@,%a@,%a@,%a%a"
+ (pp_loop_invariant pp_mem_valid')
+ (name, main_mem)
+ (pp_loop_invariant
+ (pp_memory_pack_aux pp_print_string pp_print_string))
+ (name, main_mem_ghost, main_mem)
+ (pp_loop_invariant
+ (pp_separated
+ (pp_paren pp_print_string)
+ pp_ref'
+ (pp_ref pp_var_decl)))
+ (main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
+ (pp_loop_invariant
+ (pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
+ ((), ((), ()))
+ (pp_print_option
+ (fun fmt (m_c, k) ->
+ fprintf fmt "@,%a@,%a"
+ (pp_loop_invariant (pp_gequal pp_print_string pp_print_int))
+ ("__k", 0)
+ (pp_loop_invariant
+ (pp_and_l (fun fmt k' ->
+ pp_paren
+ (pp_implies
+ ((if k' = k then pp_gequal else pp_equal) pp_print_string pp_print_int)
+ (fun fmt mem ->
+ if k' = 0 then pp_reset_set' fmt (name, mem)
+ else pp_k_induction_case
+ (k' < k)
+ m
+ m_c
+ pp_print_string
+ (pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (fun fmt _ -> pp_true_c_bool fmt ()))
+ fmt (k', mem)))
+ fmt
+ (("__k", k'),
+ main_mem_ghost))))
+ (List.init (k + 1) Fun.id)))
+ m_c_k))
()
+ let pp_main_loop_end _main_mem machines fmt m =
+ fprintf fmt "@,%a"
+ (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
+ let mem_in_c = mk_mem_in_c m in
+ let mem_out_c = mk_mem_out_c m in
+ let pp_var_c fmt (out, vd) =
+ if out then pp_true_c_bool fmt ()
+ else pp_var_decl fmt vd
+ in
+ let c_inputs = List.map (fun v -> false, v) m_c.mstep.step_inputs in
+ let c_outputs = List.map (fun v -> true, v) m_c.mstep.step_outputs in
+ fprintf fmt "%a@,%a"
+ (pp_acsl_line (pp_ghost pp_print_string))
+ "__k++;"
+ (pp_acsl_line'
+ (pp_assert
+ (pp_transition_aux
+ stateless_c
+ pp_print_string
+ pp_print_string
+ pp_var_c)))
+ (name_c, c_inputs @ c_outputs, mem_in_c, mem_out_c)))
+ (k_induction_of machines m)
+
let pp_main_spec fmt =
pp_acsl_cut
(fun fmt () ->
--
GitLab