Source file commons.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's Luncov plug-in.                    *)
(*                                                                        *)
(*  Copyright (C) 2012-2022                                               *)
(*    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 LICENSE)                       *)
(*                                                                        *)
(**************************************************************************)


open Cil_types

let label_function_name = "__PC__LABEL"
let bind_function_name = "__PC__LABEL_BINDINGS"
let starting_time = ref 0.

(** Checks if the provided expression is a string constant *)
let rec cil_isString exp =
  match exp.enode with
  | Const (CStr str) -> Some str
  | CastE (_, exp) -> cil_isString exp
  | _ -> None

let to_lval_exp varinfo =  (* transform a varinfo into expression *)
  Cil.dummy_exp (Lval (Cil.var varinfo))

let location_string loc =
  let line = (fst loc).Filepath.pos_lnum in
  let file = Filename.basename (Filepath.Normalized.to_pretty_string (fst loc).Filepath.pos_path) in
  file^":"^string_of_int line

let rec last_element list =
  match list with
  | [] -> None
  | [e] -> Some(e)
  | _::t -> last_element t

let dump_ast ?file ?name () =
  let file = match file with Some file -> file | None -> Ast.get () in
  let name =
    match name with
    | Some name -> name
    | None ->
      let project = Project.get_name (Project.current ()) in
      ".luncov_dump_"^project^".c"
  in
  let out = open_out name in
  let f = Format.formatter_of_out_channel out in
  Printer.pp_file f file;
  Format.pp_print_flush f ();
  close_out out


let suceed_or_dump_ast ?file ?name f arg =
  try
    f arg
  with e ->
    let file = match file with Some file -> file | None -> Ast.get () in
    let name =
      match name with
      | Some name -> name
      | None ->
        let project = Project.get_name (Project.current ()) in
        ".luncov_dump_"^project^".c"
    in
    at_exit (fun () -> dump_ast ~file ~name ());
    raise e


type 'a okko = Ok of 'a | Ko of exn

let with_project ?selection prj (f : 'a -> 'b) (arg : 'a) : 'b=
  let g () =
    try
      Ok (f arg)
    with e -> Ko e
  in
  match Project.on ?selection prj g () with
  | Ko e -> raise e
  | Ok res -> res


let is_label_stmt stmt lblid =
  match stmt.skind with
  | Instr (Call (None, {enode=(Lval (Var {vname=name}, NoOffset))}, idexp::_::tagexp::_, _))
    when name = label_function_name ->
    begin
      match Cil.isInteger idexp, cil_isString tagexp  with
      | Some id, Some _ ->
        if Integer.to_int_exn id = lblid then
          true, true
        else
          true, false
      | _ -> false, false
    end
  | _ -> false, false


let copy_parameters ?src dst =
  let open Wp in
  let wp_prm_states = [
    Wp_parameters.Model.self;
    Wp_parameters.RTE.self;
    Wp_parameters.ExtEqual.self;
    Wp_parameters.ExternArrays.self;
    Wp_parameters.Literals.self;
    Wp_parameters.Provers.self;
    Wp_parameters.Steps.self;
    Wp_parameters.Timeout.self;
    Wp_parameters.ProofTrace.self;
    Wp_parameters.Procs.self;
    Wp_parameters.Print.self;
    Wp_parameters.Simpl.self;
    Wp_parameters.Prune.self;
    Wp_parameters.Let.self;
    Wp_parameters.Clean.self;
    Wp_parameters.Cache.self;
  ] in
  let selection = State_selection.of_list wp_prm_states in
  Project.copy ~selection ?src dst


class variable_harvester exprs =
  object
    inherit Visitor.frama_c_inplace

    method! vexpr e =
      match e.enode with
      | Lval _ | AddrOf _ | StartOf _ ->
        exprs := Cil_datatype.ExpStructEq.Set.add e !exprs;
        Cil.SkipChildren
      | _ ->
        Cil.DoChildren

    method! vstmt_aux s =
      match s.skind with
      | Instr _ (*Voir pour skip children en cas de Call*) (*MD: qu'est-ce que ça veut dire?*)
      | Return _
      | If _ | Switch _ -> (* the actual bodies of if/switch are not visited, see vblock*)
        Cil.DoChildren
      | _ -> Cil.SkipChildren

    method! vblock _ =
      Cil.SkipChildren
  end


let collect_variables stmt =
  let vars = ref Cil_datatype.ExpStructEq.Set.empty in
  let _ = Visitor.visitFramacStmt (new variable_harvester vars) stmt in
  !vars

let collect_fun_param fdec =
  List.fold_left (fun acc v -> Cil_datatype.ExpStructEq.Set.add (to_lval_exp v) acc) Cil_datatype.ExpStructEq.Set.empty fdec.sformals

(* Create a predicate from an operator, an expression, and an integer *)
let const_to_pred op exp cst =
  let var = Logic_utils.expr_to_term ~coerce:true exp in
  let value = Cil.lconstant cst in
  Logic_const.prel (op, var, value)

(* Create a predicate asserting the interval of some expression *)
let interval_to_exp ~about min max =
  if Option.is_some min then
    let rmin =  const_to_pred Rge about (Option.get min) in
    if Option.is_some max then
      let rmax = const_to_pred Rle about (Option.get max) in
      Some (Logic_const.pands [rmin;rmax])
    else
      Some rmin
  else
  if Option.is_some max then
    Some (const_to_pred Rle about (Option.get max))
  else
    None

let interval_to_congruence_exp lv min max rem modulo = (* convertit interval+ congruence en prédicat *)
  let res = interval_to_exp ~about:lv min max in
  if Integer.equal modulo Integer.one then
    res
  else
    let var = Logic_utils.expr_to_term ~coerce:true lv in
    let cst_mod = Cil.lconstant modulo in
    let cst_rem = Cil.lconstant rem in
    let ltyp = Logic_utils.coerce_type (Cil.typeOf lv) in
    let left = Logic_const.term (TBinOp (Mod, var, cst_mod)) ltyp in
    let congru_assert =  Logic_const.prel (Req, left, cst_rem) in
    if Option.is_some res then
      Some (Logic_const.pands [(Option.get res);congru_assert])
    else
      Some congru_assert

let max_enumerate = 8

(** Create a predicate from an interval ([ival]) about some expression *)
let pred_of_ival ~about:lve iv =
  if Ival.is_bottom iv then
    None (* Should be FALSE ?? *)
  else if Ival.is_singleton_int iv then
    Some (const_to_pred Req lve (Ival.project_int iv))
  else if Ival.is_int iv then
    match Ival.project_small_set iv with
    | Some lc when List.length lc <= max_enumerate ->
      let predlc = List.map (fun v -> const_to_pred Req lve v) lc in
      Some (Logic_const.pors predlc)
    | _ -> let min, max, rem, modulo = Ival.min_max_r_mod iv in
      interval_to_congruence_exp lve min max rem modulo
  else None

exception Project_Ival_Fail
exception Project_Ival_Unreachable

let ival_of_exp ~at:stmt expr =
  assert (Eva.Analysis.is_computed ());
  (* first check if the state is actually reachable *)
  if Eva.Results.is_reachable stmt then
    (match Eva.Results.(before stmt |> eval_exp expr |> as_ival) with
     | Ok iv -> iv
     | Error _ -> raise Project_Ival_Fail)
  else
    raise Project_Ival_Unreachable

let exp_to_pred ~at expr =
  try
    let ival = ival_of_exp ~at expr in
    let pred = pred_of_ival ~about:expr ival in
    begin
      match pred with
      | Some p ->
        Options.debug "Projecting %a on sid:%d → Ok (%a)" Printer.pp_exp expr at.sid Printer.pp_predicate_node p.pred_content
      | None ->
        Options.debug "Projecting %a on sid:%d →  Ok (None)" Printer.pp_exp expr at.sid
    end;
    pred
  with
  | Project_Ival_Fail ->
    Options.debug "Projecting: %a on sid:%d → failed" Printer.pp_exp expr at.sid;
    None
  | Project_Ival_Unreachable ->
    Options.debug "Can't get %a value in stmt:[%d] code unreachable" Printer.pp_exp expr at.sid;
    None


let rec numbered_backup n filepath =
  let filepathn = filepath^"."^string_of_int n in
  if Sys.file_exists filepathn then
    numbered_backup (n+1) filepath
  else
    Sys.rename filepath filepathn

let backup filepath =
  if Sys.file_exists filepath then
    numbered_backup 1 filepath

let replace_or_add_list tbl key value =
  if Hashtbl.mem tbl key then begin
    let old = Hashtbl.find tbl key in
    Hashtbl.replace tbl key (value::old)
  end
  else
    Hashtbl.add tbl key [value]