inline_stmt_contracts.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

let emitter =
  Emitter.create
    "inline_stmt_contract" [Emitter.Code_annot] ~correctness:[] ~tuning:[]

let category = File.register_code_transformation_category "inline_stmt_contract"

let fresh_pred p =
  let v = new Visitor.frama_c_refresh (Project.current()) in
  Visitor.visitFramacPredicate v p

let nb_labels = ref 0

let new_label () =
  let res = Printf.sprintf "__fc_inline_contract_label_%d" !nb_labels in
  incr nb_labels; res

let treat_behavior for_list stmt acc b =
  let loc = Cil_datatype.Stmt.loc stmt in
  let pand p1 p2 = Logic_const.pand ~loc (p1,p2.ip_content.tp_statement) in
  let assumes = List.fold_left pand Logic_const.ptrue b.b_assumes in
  let mk_annot p =
    let p = fresh_pred p in
    let p = Logic_const.toplevel_predicate p in
    Logic_const.new_code_annotation (AAssert (for_list,p))
  in
  let add_assert p =
    let p = Logic_const.pimplies ~loc (assumes, p.ip_content.tp_statement) in
    let annot = mk_annot p in
    Annotations.add_code_annot emitter stmt annot
  in
  let treat_post_cond acc (k,p) =
    match k with
    | Normal ->
      if Logic_utils.is_trivially_true assumes then
        mk_annot p.ip_content.tp_statement :: acc
      else begin
        (match List.filter (fun l -> not (Cil.is_case_label l)) stmt.labels with
         | [] -> stmt.labels <- Label (new_label(),loc,false) :: stmt.labels
         | _ -> ());
        let p =
          Logic_const.(
            pimplies ~loc
              (pat ~loc (assumes,StmtLabel (ref stmt)),
               p.ip_content.tp_statement))
        in
        mk_annot p :: acc
      end
    | _ -> acc
  in
  List.iter add_assert b.b_requires;
  List.fold_left treat_post_cond acc b.b_post_cond

class inline_stmt_contract =
  object(self)
    inherit Visitor.frama_c_inplace
    method! vstmt_aux s =
      let loc = Cil_datatype.Stmt.loc s in
      match Annotations.code_annot ~filter:Logic_utils.is_contract s with
      | [ { annot_content = AStmtSpec (l,spec) } ] ->
        let bhvs = spec.spec_behavior in
        let posts = List.fold_left (treat_behavior l s) [] bhvs in
        (match posts with
         | [] -> Cil.DoChildren
         | _ ->
           let nop = Cil.mkStmtOneInstr ~valid_sid:true (Skip loc) in
           let kf = Option.get self#current_kf in
           List.iter (Annotations.add_code_annot emitter ~kf nop) posts;
           let b = Cil.mkBlockNonScoping [s; nop] in
           let b = Cil.transient_block b in
           let res = Cil.mkStmt ~valid_sid:true (Block b) in
           Ast.mark_as_changed ();
           File.must_recompute_cfg (Option.get self#current_func);
           ChangeTo res
        )
      | [ _ ] -> Kernel.fatal "code annotation was expected to be a contract"
      | _ :: _ -> Kernel.fatal "a statement can only have one contract"
      | [] -> Cil.DoChildren

    method! vfunc _ = nb_labels:= 0; Cil.DoChildren

    method! vexpr _ = Cil.SkipChildren
    method! vlval _ = Cil.SkipChildren
    method! vtype _ = Cil.SkipChildren
    method! vspec _ = Cil.SkipChildren
    method! vcode_annot _ = Cil.SkipChildren
    method! vinst _ = Cil.SkipChildren

  end

let inline_stmt_contract ast =
  if Kernel.InlineStmtContracts.get () then
    begin
      let vis = new inline_stmt_contract in
      Visitor.visitFramacFileSameGlobals vis ast
    end

let () =
  let deps = [ (module Kernel.InlineStmtContracts: Parameter_sig.S) ] in
  File.add_code_transformation_after_cleanup ~deps category inline_stmt_contract