Source file meta_simplify.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's MetACSL plug-in.                   *)
(*                                                                        *)
(*  Copyright (C) 2018-2025                                               *)
(*    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

(* Check if a logic variable corresponds to a C variable in the source code
 * (to easily discard a separation between it and something else if there is no
 * origin)
*)
let is_not_orig_variable lv =
  lv.lv_name = "__retres" ||
  String.starts_with ~prefix:"__fc_" lv.lv_name ||
  match lv.lv_origin with
    | Some v ->
      not v.vsource || v.vtemp || Ast_info.start_with_frama_c_builtin v.vname
    | None -> true

(*
 * Returns true if two tlvals are obviously \separated
 * That is, if they are both named variables with different names or with non-overlapping
 * offsets
 *)
let neq_lval tl1 tl2 =
  let (h1, of1), (h2, of2) = tl1, tl2 in
  let rec offset_neq o1 o2 = match (o1, o2) with
    | TNoOffset, _  | _, TNoOffset -> false
    | TField (d1, tt1), TField (d2, tt2) ->
      if Cil_datatype.Compinfo.equal d1.fcomp d2.fcomp && d1.fcomp.cstruct then
        if Cil_datatype.Fieldinfo.equal d1 d2 then
          offset_neq tt1 tt2
        else true
      else false
    | TModel (d1, tt1), TModel (d2, tt2) ->
      if Logic_utils.is_same_model_info d1 d2 then offset_neq tt1 tt2 else true
    | TIndex _, TIndex _ -> false (* Could be improved *)
    | _ -> true
  in
  (* TODO correct management of type inclusion / structure !
   * struct S { int a, char b; } s;
   * struct S* sp;
   * \untouched(s); \untouched(sp)
   * long* p = &(s.b);
   * *p = 42; //SHOUD EMIT ALARM FOR BOTH s AND sp
   * Q: Is there a field type of S that can be casted to the type of p
  *)
  (* For now, never discard when the *target* (a) is a struct/union *)
  (*let st2 = Cil.isStructOrUnionType ft2 in*)
  match (h1, h2) with
    | TVar lv, _ when is_not_orig_variable lv -> true
    | _, TVar lv when is_not_orig_variable lv -> true
    | TVar l1, TVar l2 ->
      not (Logic_utils.is_same_var l1 l2) || offset_neq of1 of2
    | _ -> false

(*
   Assuming t is a term representing an address,
   returns the lval it is an address of
*)
let get_addressed_lval t = match t.term_node with
  | TAddrOf l -> l
  | TStartOf l -> l
  | _ -> (TMem t, TNoOffset)

(*
    If t is explicitely the address of an object,
    returns that object.
*)
let get_addressed_var_opt t = match t.term_node with
  | TAddrOf l -> Some l
  | TStartOf l -> Some l
  | _ -> None

(*
 * Simplifies \separated predicates to \true or \false when possible, and
 * propagates through common logic operators. Also simplifies equality and
 * difference when terms are the same
 *)
class simplifier_visitor = object(_)
  inherit Visitor.frama_c_inplace

  method! vpredicate_node = function
    | Pseparated [t1; t2] when Logic_utils.is_same_term t1 t2 ->
      Cil.ChangeTo Pfalse
    | Pseparated [t1; t2] ->
      let l1 = get_addressed_lval t1 in
      let l2 = get_addressed_lval t2 in
      if neq_lval l1 l2 then Cil.ChangeTo Ptrue
      else Cil.DoChildren
    | Prel (Rneq, t1, t2) when Logic_utils.is_same_term t1 t2 ->
      Cil.ChangeTo Pfalse
    | Prel (Req, t1, t2) when Logic_utils.is_same_term t1 t2 ->
      Cil.ChangeTo Ptrue
    | Prel ((Req | Rneq) as rel, t1, t2)
      when Option.is_some (get_addressed_var_opt t1)
        && Option.is_some (get_addressed_var_opt t2) ->
      let l1 = Option.get (get_addressed_var_opt t1) in
      let l2 = Option.get (get_addressed_var_opt t2) in
      if neq_lval l1 l2 then
        if rel = Rneq then Cil.ChangeTo Ptrue
        else Cil.ChangeTo Pfalse
      else Cil.DoChildren
    | Pnot _ -> Cil.DoChildrenPost (function
        | Pnot t when Logic_utils.is_trivially_true t -> Pfalse
        | Pnot t when Logic_utils.is_trivially_false t -> Ptrue
        | p -> p
      )
    | Pforall _ -> Cil.DoChildrenPost (function
        | Pforall (_, p) when Logic_utils.is_trivially_true p -> Ptrue
        | Pforall (_, p) when Logic_utils.is_trivially_false p -> Pfalse
        | p -> p
      )
    | Plet (_, _) -> Cil.DoChildrenPost (function
        | Plet (_, p) when Logic_utils.is_trivially_true p -> Ptrue
        | Plet (_, p) when Logic_utils.is_trivially_false p -> Pfalse
        | p -> p
      )
    | Pimplies _ -> Cil.DoChildrenPost (function
        | Pimplies (p1, _) when Logic_utils.is_trivially_false p1 -> Ptrue
        | Pimplies (_, p2) when Logic_utils.is_trivially_true p2 -> Ptrue
        | Pimplies (p1, p2) when Logic_utils.is_trivially_true p1
                              && Logic_utils.is_trivially_false p2 -> Pfalse
        | Pimplies (p1, p2) when Logic_utils.is_trivially_false p2 ->
          Pnot p1
        | Pimplies (p1, p2) when Logic_utils.is_trivially_true p1 ->
          p2.pred_content
        | p -> p
      )
    | Pand _ -> Cil.DoChildrenPost (function
        | Pand (p1, _) when Logic_utils.is_trivially_false p1 -> Pfalse
        | Pand (_, p2) when Logic_utils.is_trivially_false p2 -> Pfalse
        | Pand (p1, p2) when Logic_utils.is_trivially_true p1
                          && Logic_utils.is_trivially_true p2 -> Ptrue
        | Pand (p1, p2) when Logic_utils.is_trivially_true p1 ->
          p2.pred_content
        | Pand (p1, p2) when Logic_utils.is_trivially_true p2 ->
          p1.pred_content
        | p -> p
      )
    | Por _ -> Cil.DoChildrenPost (function
        | Por (p1, _) when Logic_utils.is_trivially_true p1 -> Ptrue
        | Por (_, p2) when Logic_utils.is_trivially_true p2 -> Ptrue
        | Por (p1, p2) when Logic_utils.is_trivially_false p1
                         && Logic_utils.is_trivially_false p2 -> Pfalse
        | Por (p1, p2) when Logic_utils.is_trivially_false p1 ->
          p2.pred_content
        | Por (p1, p2) when Logic_utils.is_trivially_false p2 ->
          p1.pred_content
        | p -> p
      )
    | _ -> Cil.DoChildren
end

let simplify pred =
  let vis = new simplifier_visitor in
  Visitor.visitFramacPredicate vis pred

(*
 * Given a predicate and the statement (and kf) it will be attached to,
 * return another predicate where every quantified, local or formal logic
 * variable whose name conflict with a C name already in scope has been alpha
 * converted
 *)
let remove_alpha_conflicts pred kf stmt =
  if stmt.ghost then pred else
    let enclosing = Kernel_function.find_all_enclosing_blocks stmt in
    (* List of local variables in scope and formal variables *)
    let reserved = List.map (fun v -> v.vname) @@ List.fold_left
        (fun names block -> (block.blocals @ block.bstatics) @ names)
        (Kernel_function.get_formals kf) enclosing in
    let visitor = object (self)
      inherit Visitor.frama_c_inplace
      (* Names that cannot be used *)
      val mutable reserved_up = reserved
      (* New names created for reserved names *)
      val mutable assoc = []
      (* Name that can be used but not when creating new names *)
      val mutable preserve = []
      method common lv = match lv.lv_kind with
        | LVQuant | LVLocal | LVFormal ->
          let name = lv.lv_name in
          if List.mem name reserved_up then
            match List.assoc_opt name assoc with
              | Some lv -> Cil.ChangeTo lv
              | None ->
                let rec find_valid_suffix cur =
                  let conc = name ^ (string_of_int cur) in
                  if List.mem conc (reserved_up @ preserve) then
                    find_valid_suffix @@ cur + 1
                  else conc in
                let nn = find_valid_suffix 1 in
                let new_lv = { lv with lv_name = nn } in
                assoc <- (name, new_lv) :: assoc ;
                reserved_up <- nn :: reserved_up ;
                Cil.ChangeTo new_lv
          else (preserve <- name :: preserve ; Cil.SkipChildren)
        | _ -> Cil.SkipChildren
      method! vlogic_var_decl = self#common
      method! vlogic_var_use = self#common
    end in
    Visitor.visitFramacPredicate (visitor :> Visitor.frama_c_visitor) pred