CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

open Utils

open Format

open Lustre_types

open Machine_code_types

open C_backend_common

open Corelang

open Spec_types

open Machine_code_common

module Mpfr = Lustrec_mpfr

(**************************************************************************)

(*     Printing spec for c *)

(**************************************************************************)

let pp_acsl_basic_type_desc t_desc =

  if Types.is_bool_type t_desc then

    (* if !Options.cpp then "bool" else "_Bool" *)

    "_Bool"

  else if Types.is_int_type t_desc then

    (* !Options.int_type *)

    if t_desc.tid = -1 then "int" else "integer"

  else if Types.is_real_type t_desc then

    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type

  else assert false

(* Not a basic C type. Do not handle arrays or pointers *)

let pp_acsl pp fmt = fprintf fmt "@[<v>/*%@ @[<v>%a@]@,*/@]" pp

let pp_acsl_cut pp fmt = fprintf fmt "%a@," (pp_acsl pp)

let pp_acsl_line pp fmt = fprintf fmt "//%@ @[<h>%a@]" pp

let pp_acsl_line' ?(ghost = false) pp fmt x =

  let op = if ghost then "" else "*" in

  let cl = if ghost then "@" else "*" in

  fprintf fmt "/%s%@ @[<h>%a@] %s/" op pp x cl

let pp_acsl_line'_cut pp fmt = fprintf fmt "%a@," (pp_acsl_line' pp)

let pp_requires pp fmt = fprintf fmt "requires %a;" pp

let pp_ensures pp fmt = fprintf fmt "ensures %a;" pp

let pp_assumes pp fmt = fprintf fmt "assumes %a;" pp

let pp_terminates pp fmt = fprintf fmt "terminates %a;" pp

let pp_assigns pp =

  pp_comma_list

    ~pp_prologue:(fun fmt () -> pp_print_string fmt "assigns ")

    ~pp_epilogue:pp_print_semicolon'

    pp

let pp_ghost pp fmt = fprintf fmt "ghost %a" pp

let pp_assert pp fmt = fprintf fmt "assert %a;" pp

let pp_loop_invariant pp fmt = fprintf fmt "loop invariant %a;" pp

let pp_mem_valid pp_var fmt (name, var) =

  fprintf fmt "%s_valid(%a)" name pp_var var

let pp_mem_valid' = pp_mem_valid pp_print_string

let pp_ref pp fmt = fprintf fmt "&%a" pp

let pp_ref' = pp_ref pp_print_string

let pp_indirect pp_ptr pp_field fmt (ptr, field) =

  fprintf fmt "%a->%a" pp_ptr ptr pp_field field

let pp_indirect' = pp_indirect pp_print_string pp_print_string

let pp_access pp_stru pp_field fmt (stru, field) =

  fprintf fmt "%a.%a" pp_stru stru pp_field field

let pp_access' = pp_access pp_print_string pp_print_string

let pp_var_decl fmt v = pp_print_string fmt v.var_id

let pp_reg self fmt field =

  pp_access pp_indirect' pp_var_decl fmt ((self, "_reg"), field)

let pp_true fmt () = pp_print_string fmt "\\true"

let pp_cast pp_ty pp fmt (ty, x) = fprintf fmt "(%a) %a" pp_ty ty pp x

let pp_bool_cast pp fmt x = pp_cast pp_print_string pp fmt ("_Bool", x)

let pp_double_cast pp fmt x = pp_cast pp_print_string pp fmt ("double", x)

let pp_true_c_bool fmt () = pp_bool_cast pp_print_string fmt "1"

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 pp_at_pre pp_v fmt v = pp_at pp_v fmt (v, "Pre")

let find_machine f = List.find (fun m -> m.mname.node_id = f)

let instances machines m =

  let open List in

  let grow paths i td mems =

    match paths with

    | [] ->

      [ [ i, (td, mems) ] ]

    | _ ->

      map (cons (i, (td, mems))) paths

  in

  let rec aux paths m =

    map

      (fun (i, (td, _)) ->

        try

          let m = find_machine (node_name td) machines in

          aux (grow paths i td m.mmemory) m

        with Not_found -> grow paths i td [])

      m.minstances

    |> flatten

  in

  aux [] m |> map rev

let memories insts =

  List.(

    map

      (fun path ->

        let _, (_, mems) = hd (rev path) in

        map (fun mem -> path, mem) mems)

      insts

    |> flatten)

let pp_instance ?(indirect = true) pp ptr =

  pp_print_list

    ~pp_prologue:(fun fmt () -> fprintf fmt "%a->" pp ptr)

    ~pp_sep:(fun fmt () -> pp_print_string fmt (if indirect then "->" else "."))

    (fun fmt (i, _) -> pp_print_string fmt i)

let pp_memory ?(indirect = true) ptr fmt (path, mem) =

  pp_access

    ((if indirect then pp_indirect else pp_access)

       (pp_instance ~indirect pp_print_string ptr)

       pp_print_string)

    pp_var_decl

    fmt

    ((path, "_reg"), mem)

let prefixes l =

  let rec pref acc = function

    | x :: l ->

      pref ([ x ] :: List.map (List.cons x) acc) l

    | [] ->

      acc

  in

  pref [] (List.rev l)

let powerset_instances paths =

  List.map prefixes paths |> List.flatten |> remove_duplicates

let pp_separated pp_self pp_mem pp_ptr fmt (self, mem, paths, ptrs) =

  fprintf

    fmt

    "\\separated(@[<v>%a, %a%a%a@])"

    pp_self

    self

    pp_mem

    mem

    (pp_comma_list ~pp_prologue:pp_print_comma (pp_instance pp_self self))

    paths

    (pp_comma_list ~pp_prologue:pp_print_comma pp_ptr)

    ptrs

let pp_separated' self mem fmt (paths, ptrs) =

  pp_separated

    pp_print_string

    pp_print_string

    pp_var_decl

    fmt

    (self, mem, paths, ptrs)

let pp_separated'' =

  pp_comma_list

    ~pp_prologue:(fun fmt () -> pp_print_string fmt "\\separated(")

    ~pp_epilogue:pp_print_cpar

    pp_var_decl

let pp_forall pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r

let pp_exists pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r

let pp_equal pp_l pp_r fmt (l, r) = fprintf fmt "%a == %a" pp_l l pp_r r

let pp_gequal pp_l pp_r fmt (l, r) = fprintf fmt "%a >= %a" pp_l l pp_r r

let pp_implies pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v>%a ==>@ %a@]" pp_l l pp_r r

let pp_and pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ && %a@]" pp_l l pp_r r

let pp_and_l pp_v fmt =

  pp_print_list

    ~pp_open_box:pp_open_vbox0

    ~pp_sep:(fun fmt () -> fprintf fmt "@,&& ")

    ~pp_nil:pp_true

    pp_v

    fmt

let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r

let pp_or_l pp_v fmt =

  pp_print_list

    ~pp_open_box:pp_open_vbox0

    ~pp_sep:(fun fmt () -> fprintf fmt "@,|| ")

    pp_v

    fmt

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 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

let pp_paren pp fmt v = fprintf fmt "(%a)" pp v

let pp_initialization pp_mem fmt (name, mem) =

  fprintf fmt "%s_initialization(%a)" name pp_mem mem

let pp_init pp_mem fmt (name, mem) = fprintf fmt "%s_init(%a)" name pp_mem mem

let pp_initialization' = pp_initialization pp_print_string

let pp_local m =

  pp_c_decl_local_var ~pp_c_basic_type_desc:pp_acsl_basic_type_desc m

let pp_locals m =

  pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (pp_local m)

let pp_ptr_decl fmt v = pp_ptr fmt v.var_id

let pp_basic_assign_spec ?(pp_op=pp_equal) pp_l pp_r fmt typ var_name value =

  if Types.is_real_type typ && !Options.mpfr then assert false

    (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)

  else pp_op pp_l pp_r fmt (var_name, value)

let pp_assign_spec ?pp_op m self_l pp_var_l indirect_l self_r pp_var_r indirect_r fmt

    (var_type, var_name, value) =

  let depth = expansion_depth value in

  let loop_vars = mk_loop_variables m var_type depth in

  let reordered_loop_vars = reorder_loop_variables loop_vars in

  let aux typ fmt vars =

    match vars with

    | [] ->

      pp_basic_assign_spec ?pp_op

        (pp_value_suffix

           ~indirect:indirect_l

           m

           self_l

           var_type

           loop_vars

           pp_var_l)

        (pp_value_suffix

           ~indirect:indirect_r

           m

           self_r

           var_type

           loop_vars

           pp_var_r)

        fmt

        typ

        var_name

        value

    | (_d, LVar _i) :: _q ->

      assert false

    (* let typ' = Types.array_element_type typ in

     * fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

     *   i i i pp_c_dimension d i

     *   (aux typ') q *)

    | (_d, LInt _r) :: _q ->

      assert false

    (* let typ' = Types.array_element_type typ in

     * let szl = Utils.enumerate (Dimension.size_const_dimension d) in

     * fprintf fmt "@[<v 2>{@,%a@]@,}"

     *   (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl *)

    | _ ->

      assert false

  in

  reset_loop_counter ();

  aux var_type fmt reordered_loop_vars

let pp_memory_pack_aux ?i pp_mem pp_self fmt (name, mem, self) =

  fprintf

    fmt

    "%s_pack%a(@[<hov>%a,@ %a@])"

    name

    (pp_print_option pp_print_int)

    i

    pp_mem

    mem

    pp_self

    self

let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =

  pp_memory_pack_aux

    ?i:mp.mpindex

    pp_mem

    pp_self

    fmt

    (mp.mpname.node_id, mem, self)

let pp_transition_aux ?i stateless pp_mem_in pp_mem_out pp_var fmt

    (name, vars, mem_in, mem_out) =

  fprintf

    fmt

    "%s_transition%a(@[<hov>%t%a%t@])"

    name

    (pp_print_option pp_print_int)

    i

    (fun fmt -> if not stateless then pp_mem_in fmt mem_in)

    (pp_comma_list

       ~pp_prologue:(fun fmt () -> if not stateless then pp_print_comma fmt ())

       pp_var)

    vars

    (fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)

let pp_transition stateless pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out)

    =

  pp_transition_aux

    ?i:t.tindex

    stateless

    pp_mem_in

    pp_mem_out

    pp_var

    fmt

    (t.tname.node_id, t.tvars, mem_in, mem_out)

let pp_transition_aux' ?i m =

  let stateless = fst (get_stateless_status m) in

  pp_transition_aux ?i stateless pp_print_string pp_print_string (fun fmt v ->

      (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)

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

    | [] ->

      pp_print_string fmt mem

    | (x, is_mem) :: fields ->

      fprintf

        fmt

        "{ @[<hov>%a@ \\with .%s%s = %s@] }"

        aux

        fields

        (if is_mem then "_reg." else "")

        x

        x

  in

  aux

    fmt

    (List.map (fun (x, _) -> x, false) (Utils.IMap.bindings insts)

    @ List.map (fun x -> x, true) (Utils.ISet.elements mems))

module PrintSpec = struct

  type mode =

    | MemoryPackMode

    | TransitionMode

    | TransitionFootprintMode

    | ResetIn

    | 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 pp_expr ?(test_output = false) m mem fmt = function

    | Val v ->

      let pp = pp_c_val m mem (pp_c_var_read ~test_output m) in

      (if not_var v

       then if Types.is_bool_type v.value_type

         then pp_bool_cast pp

         else if Types.is_real_type v.value_type

         then pp_double_cast pp

         else pp

       else pp) fmt v

    | Tag t ->

      pp_print_string fmt t

    | Var v ->

      pp_var_decl fmt v

    | Memory r ->

      pp_reg mem fmt r

  let pp_predicate mode m mem_in mem_in' mem_out mem_out' fmt p =

    let test_output, mem_update =

      match mode with

      | InstrMode _ ->

        true, false

      | TransitionFootprintMode ->

        false, true

      | _ ->

        false, false

    in

    let pp_expr test_output fmt e = pp_expr ~test_output m mem_out fmt e in

    match p with

    | Transition (stateless, f, inst, i, vars, r, mems, insts) ->

      let pp_mem_in, pp_mem_out =

        match inst with

        | None ->

          ( pp_print_string,

            if mem_update then pp_functional_update mems insts

            else pp_print_string )

        | Some inst ->

          ( (fun fmt mem_in ->

              if r then pp_print_string fmt mem_in

              else pp_access' fmt (mem_in, inst)),

            fun fmt mem_out -> pp_access' fmt (mem_out, inst) )

      in

      pp_transition_aux

        ?i

        stateless

        pp_mem_in

        pp_mem_out

        (pp_expr test_output)

        fmt

        (f, vars, mem_in', mem_out')

    | 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_equal pp_print_string pp_access')

        fmt

        (r, (mem_out, 1), (mem_out, (mem_in, inst)))

    | MemoryPack (f, inst, i) ->

      let pp_mem, pp_self =

        match inst with

        | None ->

          pp_print_string, pp_print_string

        | Some inst ->

          ( (fun fmt mem -> pp_access' fmt (mem, inst)),

            fun fmt self -> pp_indirect' fmt (self, inst) )

      in

      pp_memory_pack_aux ?i pp_mem pp_self fmt (f, mem_out, mem_in)

    | ResetCleared f ->

      pp_reset_cleared' fmt (f, mem_in, mem_out)

    (* fprintf fmt "ResetCleared_%a" pp_print_string f *)

    | Initialization ->

      ()

  let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool

  let val_of_expr = function

    | Val v ->

      v

    | Tag t ->

      id_to_tag t

    | Var v ->

      vdecl_to_val v

    | Memory (StateVar v) ->

      vdecl_to_val v

    | Memory ResetFlag ->

      vdecl_to_val reset_flag

  let find_arrow loc m =

    match List.find_opt (fun (_, (td, _)) -> Arrow.td_is_arrow td) m.minstances with

    | Some (f, _) -> Some f

    | None ->

      Error.pp_warning loc

        (fun fmt -> pp_print_string fmt "Generating stateful spec for uninitialized state variables.");

      None

  let rec has_memory_val m v =

    let has_mem = has_memory_val m in

    match v.value_desc with

    | Var v ->

      is_memory m v

    | Array vl | Fun (_, vl) ->

      List.exists has_mem vl

    | Access (t, i) | Power (t, i) ->

      has_mem t || has_mem i

    | _ ->

      false

  let has_memory m = function Val v -> has_memory_val m v | _ -> false

  let pp_spec mode m =

    let rec pp_spec mode fmt f =

      let mem_in, mem_in', indirect_r, mem_out, mem_out', indirect_l =

        let self = mk_self m in

        let mem = mk_mem m in

        let mem_in = mk_mem_in m in

        let mem_out = mk_mem_out m in

        let mem_reset = mk_mem_reset m in

        match mode with

        | MemoryPackMode ->

          self, self, true, mem, mem, false

        | TransitionMode ->

          mem_in, mem_in, false, mem_out, mem_out, false

        | TransitionFootprintMode ->

          mem_in, mem_in, false, mem_out, mem_out, false

        | ResetIn ->

          mem_reset, mem_reset, false, mem_out, mem_out, false

        | ResetOut ->

          mem_in, mem_in, false, mem_reset, mem_reset, false

        | InstrMode self ->

          let mem = "*" ^ mem in

          fprintf str_formatter "%a" (pp_at pp_print_string) (mem, reset_label);

          self, flush_str_formatter (), false, mem, mem, false

      in

      let pp_expr fmt e = pp_expr m mem_out fmt e in

      let pp_spec' = pp_spec mode in

      match f with

      | True ->

        pp_true fmt ()

      | False ->

        pp_false fmt ()

      | Equal (a, b) ->

        let pp_eq fmt () =

          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

            (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)

        in

        if has_memory m b then

          let inst = find_arrow Location.dummy m in

          pp_print_option

            ~none:pp_eq

            (fun fmt inst ->

               pp_paren

                 (pp_implies (pp_not (pp_initialization pp_access')) pp_eq)

                 fmt

                 ((Arrow.arrow_id, (mem_in, inst)), ()))

            fmt inst

        else pp_eq fmt ()

      | GEqual (a, b) ->

        pp_assign_spec ~pp_op:pp_gequal

          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

          (Spec_common.type_of_l_value a, val_of_expr a, val_of_expr b)

      | And fs ->

        pp_and_l pp_spec' fmt fs

      | Or fs ->

        pp_or_l pp_spec' fmt fs

      | Imply (a, b) ->

        pp_paren (pp_implies pp_spec' pp_spec') fmt (a, b)

      | Exists (xs, a) ->

        pp_exists (pp_locals m) pp_spec' fmt (xs, a)

      | Forall (xs, a) ->

        pp_forall (pp_locals m) pp_spec' fmt (xs, a)

      | Ternary (e, a, b) ->

        pp_ite pp_expr pp_spec' pp_spec' fmt (e, a, b)

      | 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) ->

        let v' = vdecl_to_val v in

        let pp_eq fmt () =

          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

            (v.var_type, v', v')

        in

        let inst = find_arrow Location.dummy m in

        pp_print_option

          ~none:pp_eq

          (fun fmt inst ->

             pp_paren

               (pp_implies

                  (pp_not (pp_initialization pp_access'))

                  pp_eq)

               fmt

               ((Arrow.arrow_id, (mem_out, inst)), ()))

          fmt inst

      | ExistsMem (f, rc, tr) ->

        pp_exists

          (pp_machine_decl' ~ghost:true)

          (pp_and (pp_spec ResetOut) (pp_spec ResetIn))

          fmt

          ((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

    in

    pp_spec mode

end

let pp_predicate pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>predicate %a =@,%a;@]" pp_l l pp_r r

let pp_lemma pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r

let pp_axiomatic pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r

let pp_axiom pp_l pp_r fmt (l, r) =

  fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r

let pp_mem_valid_def fmt m =

  if not (fst (get_stateless_status m) || m.mis_contract) then

    let name = m.mname.node_id in

    let self = mk_self m in

    pp_acsl

      (pp_predicate

         (pp_mem_valid (pp_machine_decl pp_ptr))

         (pp_and

            (pp_and_l (fun fmt (inst, (td, _)) ->

                 if Arrow.td_is_arrow td then

                   pp_valid pp_indirect' fmt [ self, inst ]

                 else pp_mem_valid pp_indirect' fmt (node_name td, (self, inst))))

            (pp_valid pp_print_string)))

      fmt

      ((name, (name, self)), (m.minstances, [ self ]))

let pp_memory_pack_def m fmt mp =

  if not (fst (get_stateless_status m) || m.mis_contract) then

    let name = mp.mpname.node_id in

    let self = mk_self m in

    let mem = mk_mem m in

    pp_acsl_cut

      (pp_predicate

         (pp_memory_pack

            (pp_machine_decl' ~ghost:true)

            (pp_machine_decl pp_ptr))

         (PrintSpec.pp_spec MemoryPackMode m))

      fmt

      ((mp, (name, mem), (name, self)), mp.mpformula)

let pp_machine_ghost_struct fmt m =

  pp_acsl (pp_ghost (pp_machine_struct ~ghost:true)) fmt m

let pp_memory_pack_defs fmt m =

  if not (fst (get_stateless_status m)) then

    fprintf

      fmt

      "%a@,%a"

      pp_machine_ghost_struct

      m

      (pp_print_list

         ~pp_sep:pp_print_nothing

         ~pp_epilogue:pp_print_cut

         ~pp_open_box:pp_open_vbox0

         (pp_memory_pack_def m))

      m.mspec.mmemory_packs

let pp_transition_def m fmt t =

  let name = t.tname.node_id in

  let mem_in = mk_mem_in m in

  let mem_out = mk_mem_out m in

  let stateless = fst (get_stateless_status m) in

  pp_acsl

    (pp_predicate

       (pp_transition

          stateless

          (pp_machine_decl' ~ghost:true)

          (pp_machine_decl' ~ghost:true)

          (pp_local m))

       (PrintSpec.pp_spec TransitionMode m))

    fmt

    ((t, (name, mem_in), (name, mem_out)), t.tformula)

let pp_transition_defs fmt m =

  pp_print_list

    ~pp_epilogue:pp_print_cut

    ~pp_open_box:pp_open_vbox0

    (pp_transition_def m)

    fmt

    m.mspec.mtransitions

let pp_transition_footprint fmt t =

  fprintf

    fmt

    "%s_transition%a_footprint"

    t.tname.node_id

    (pp_print_option pp_print_int)

    t.tindex

let pp_transition_footprint_lemma m fmt t =

  let name = t.tname.node_id in

  let mem_in = mk_mem_in m in

  let mem_out = mk_mem_out m in

  let stateless = fst (get_stateless_status m) in

  let mems =

    ISet.(

      diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)

  in

  let insts =

    IMap.(

      diff

        (of_list (List.map (fun (x, (td, _)) -> x, node_name td) m.minstances))

        t.tinst_footprint)

  in

  let memories =

    List.map

      (fun v -> { v with var_type = { v.var_type with tid = -1 } })

      (List.filter (fun v -> ISet.mem v.var_id mems) m.mmemory)

  in

  let mems_empty = ISet.is_empty mems in

  let insts_empty = IMap.is_empty insts in

  let instances = List.map (fun (i, f) -> f, i) (IMap.bindings insts) in

  let tr ?mems ?insts () =

    Spec_common.mk_transition

      ?mems

      ?insts

      ?i:t.tindex

      stateless

      name

      (vdecls_to_vals t.tvars)

  in

  if not ((mems_empty && insts_empty) || m.mis_contract) then

    pp_acsl_cut

      (pp_lemma

         pp_transition_footprint

         (pp_forall

            (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))

            ((if insts_empty then fun pp fmt (_, x) -> pp fmt x

             else pp_forall (pp_comma_list (pp_machine_decl' ~ghost:true)))

               ((if mems_empty then fun pp fmt (_, x) -> pp fmt x

                else pp_forall (pp_locals m))

                  (PrintSpec.pp_spec TransitionFootprintMode m)))))

      fmt

      ( t,

        ( (m.mname.node_id, [ mem_in; mem_out ]),

          ( instances,

            (memories, Forall (t.tvars, Imply (tr (), tr ~mems ~insts ()))) ) )

      )