Source file instrument_label.ml

(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Instrument

let get_label id =
  let value = get id in
  match value with
  | Label linfo -> linfo
  | _ -> assert false

let get_loc id =
  (get_label id).li_loc

let get_tag id =
  (get_label id).li_tag

let get_annotable_stmt id =
  (get_label id).li_annotable

let get_predicate id =
  (get_label id).li_predicate

let get_kf_id id =
  (get_label id).li_kf_id

let at = ref Req

(** Visitor that removes all but a single label (given its id),
    add a single assertion whose validity implies the uncoverability of a label,
    and provides information to get a Property.t
*)
class label_selector lblid info prj = object (self)
  inherit Visitor.frama_c_copy prj

  val mutable remove_locals = []

  method private clean_locals locals =
    List.filter
      (fun vi ->
         not (List.exists
                (fun vi' -> Cil_datatype.Varinfo.equal vi vi') remove_locals))
      locals

  method private clean_skips stmtl =
    List.filter (fun s ->
        s.labels <> [] || not @@ Cil.is_skip s.skind
      ) stmtl

  method! vfunc _ =
    Cil.DoChildrenPost (fun f ->
        f.slocals <- self#clean_locals f.slocals;
        File.must_recompute_cfg f;
        remove_locals <- [];
        f
      )

  method !vblock _ =
    Cil.DoChildrenPost
      (fun b ->
         b.bstmts <- self#clean_skips b.bstmts;
         b.blocals <- self#clean_locals b.blocals;
         b)

  method! vstmt_aux stmt =
    match stmt.skind, is_stmt_by_sid stmt.sid with
    | _, [lblid'] when lblid' = lblid ->
      self#add_label_annot ();
      Cil.JustCopy
    | Block b, [_] ->
      remove_locals <- b.blocals @ remove_locals;
      stmt.skind <- Instr (Skip Fileloc.unknown);
      Cil.JustCopy
    | Instr i, _ ->
      begin match i with
        | Set ((Var v,_), _, _)
        | Local_init (v, _, _)
        | Call (Some (Var v, _),_,_,_) ->
          let vn = "__SEQ_STATUS_" in
          if String.length v.vname > String.length vn
          && String.sub v.vname 0 (String.length vn) = vn then begin
            if String.split_on_char '_' v.vname |> List.rev |> List.hd |> int_of_string <> lblid then
              begin
                stmt.skind <- Instr (Skip Fileloc.unknown);
                remove_locals <- [v] @ remove_locals;
              end
          end;
          Cil.JustCopy
        | _ -> Cil.JustCopy
      end
    | _, _ -> Cil.DoChildren

  method private add_label_annot () =
    let lblinfo = get_label lblid in
    let old_kf = Option.get self#current_kf in
    let new_kf = Visitor_behavior.Get.kernel_function self#behavior old_kf in
    let cond = Visitor.visitFramacExpr (self :> Visitor.frama_c_visitor) lblinfo.li_predicate in
    let pred = Logic_utils.expr_to_predicate cond in
    let pred = if !at = Req then Logic_const.pnot pred  else pred in (* NB negated*)
    let top_pred = Logic_const.toplevel_predicate ~kind:Check pred in
    let code_annot = AAssert ([], top_pred) in
    let queued_action () =
      let code_annotation = Logic_const.new_code_annotation code_annot in
      Annotations.add_code_annot ~kf:new_kf wp_emitter lblinfo.li_annotable code_annotation;
      let ip = Property.ip_of_code_annot_single new_kf lblinfo.li_annotable code_annotation in
      info := Some ip;
    in
    Queue.add queued_action self#get_filling_actions
end

let create_project_for_label ?name id =
  let name = match name with None -> "label_"^string_of_int id | Some name -> name in
  let info = ref None in
  let prj = File.create_project_from_visitor name (new label_selector id info) in
  prj, !info