Source file meta_bindings.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 Meta_options
open Meta_utils
open Logic_ptree
open Logic_typing
open Cil_types

(* Gathered bindings *)
let types = Str_Hashtbl.create 5

let setname base = base ^ "_set"
let sizename base = base ^ "_size"
let capname base = base ^ "_capacity"

(* Replace \bound(name) by name_set[name_i] where name_i is a newly created
 * quantified logic variable, which is remembered in the 'quantifiers' table to
 * close the predicate at the end (see after_parse)
*)
let parse_bound tc loc quantifiers bn = match bn.lexpr_node with
  | PLvar bname ->
    let content_type = begin match Str_Hashtbl.find_opt types bname with
      | Some x -> x
      | None -> tc.error loc "The name '%s' is used but not bound anywhere" bname
    end in
    let tabvar = tc.find_var (setname bname) in
    let quantvar = begin match Str_Hashtbl.find_opt quantifiers bname with
      | Some x -> x
      | None ->
        let res = Cil_const.make_logic_var_quant (bname ^ "_i") Linteger
        in Str_Hashtbl.add quantifiers bname res; res
    end in
    let tlv = (TVar tabvar, TIndex (Logic_const.tvar quantvar, TNoOffset)) in
    Logic_const.term (TLval tlv) content_type
  | _ -> tc.error loc "Expecting a simple variable name for \\bound"

(* Replace a \bind(val, name) by the pair associating the actual C variable
   to the name. Used afterwards at the end of the translation process.
*)
let parse_bind tc loc cvar_name gvar_name =
  let cvar = tc.find_var cvar_name in
  let bdg_type = begin match cvar.lv_type with
    | Ctype _ as lt -> lt
    | _ -> tc.error loc "Only C variables can be bound to names"
  end in
  begin match Str_Hashtbl.find_opt types gvar_name with
    | None -> Str_Hashtbl.add types gvar_name bdg_type
    | Some old_type ->
      if not @@ Logic_utils.is_same_type bdg_type old_type then
        tc.error loc
          "The name %s was previously bound with variables of type %a \
           but now you are trying to bind it with a variable of type %a"
          gvar_name Printer.pp_logic_type old_type
          Printer.pp_logic_type bdg_type
  end;
  let cvar_term = Logic_const.tvar cvar in
  let name_term =
    Logic_const.term (TConst (LStr gvar_name)) (Ctype Cil_const.charPtrType)
  in
  Ext_terms [cvar_term; name_term]

(* Called by the delayed parser for each predicate
 * quanthash is a hash table with a pair for each \bound(val, name) associating
 * 'name' with the quantified logic_variable used to replace bound.
 * The predicate is closed with universal quantification on each of these
 * variables, with a proper interval 0 <= quant < name_size
*)
let after_parse tc pred quanthash =
  let open Logic_const in
  let quantifiers = Str_Hashtbl.fold (fun _ -> List.cons) quanthash [] in
  let conditions = Str_Hashtbl.fold (fun name var conds ->
      let mainterm = tvar var in
      let sizeterm = tc.find_var (sizename name) |> tvar in
      let supzero = prel (Rle, tinteger 0, mainterm) in
      let infmax = prel (Rlt, mainterm, sizeterm) in
      supzero :: infmax :: conds
    ) quanthash [] in
  let with_cond = pimplies (pands conditions, pred) in
  pforall (quantifiers, with_cond)

let ext_flags = ref None

(* to_add maps sids to statements that must be inserted before the
 * corresponding statements *)
let to_add = Stmt_Hashtbl.create 5

(* Toggles the inline visitor *)
let visit_inline = ref false

(* Add ghost code needed for bindings, i.e. declarations of name_set/size and
 * their modification when encountering \binds *)
let add_ghost_code flags =
  ext_flags := Some flags;
  visit_inline := true;
  let f = Ast.get () in
  let unkloc = Cil_datatype.Location.unknown in
  (* Declare _set and _size global variables *)
  let make_global name typ =
    let base_type = Logic_utils.logicCType typ in
    (* The _set is either a fixed array or a pointer *)
    let ctype = match flags.static_bindings with
      | Some n -> Cil_const.mk_tarray base_type (Some (Cil.integer ~loc:unkloc n))
      | None -> Cil_const.mk_tptr base_type
    in
    let var = Cil.makeGlobalVar (setname name) ctype in
    let svar = Cil.makeGlobalVar (sizename name) Cil_const.uintType in
    var.vghost <- true; svar.vghost <- true;
    let sinit = {init = Some (Cil.makeZeroInit ~loc:unkloc Cil_const.uintType)} in
    Globals.Vars.add_decl var; Globals.Vars.add svar sinit;
    let pre = [GVarDecl (var, unkloc); GVar (svar, sinit, unkloc)] in
    match flags.static_bindings with
      | Some _ -> pre
      | None -> (* For dynamic arrays, add a capacity variable *)
        let cvar = Cil.makeGlobalVar (capname name) Cil_const.uintType in
        cvar.vghost <- true;
        Globals.Vars.add cvar sinit;
        GVar (cvar, sinit, unkloc) :: pre
  in
  let globs = Str_Hashtbl.fold (fun a b c -> (make_global a b) @ c) types [] in
  f.globals <- globs @ f.globals;
  (* Visit the file, resetting to_add when encoutering a function (since sids
   * are unique only within a function) and inserting values of to_add in
   * correct blocks
  *)
  let changed_funcs = ref Fundec_Set.empty in
  let mark_changed f = changed_funcs := Fundec_Set.add f !changed_funcs in
  let vis = object (self)
    inherit Visitor.frama_c_inplace
    method! vblock _ = Cil.DoChildrenPost (fun block ->
        let rec aux = function
          | [] -> []
          | s :: t ->
            let aux_stmt = find_hash_list Stmt_Hashtbl.find_opt to_add s in
            if aux_stmt <> [] then
              mark_changed (Option.get self#current_func);
            aux_stmt @ [s] @ (aux t)
        in block.bstmts <- aux block.bstmts;
        block
      )
    method! vfunc _ =
      Stmt_Hashtbl.clear to_add;
      Cil.DoChildren
  end in
  Visitor.visitFramacFile vis f;
  if not (Fundec_Set.is_empty !changed_funcs) then
    begin
      let reinit_cfg f =
        Cfg.clearCFGinfo ~clear_id:false f;
        Cfg.cfgFun f
      in
      Fundec_Set.iter reinit_cfg !changed_funcs;
      Ast.mark_as_changed ()
    end

let search_global_var name =
  try
    Globals.Vars.find_from_astinfo name Global
  with Not_found -> Self.fatal "search_global_var: failed to find %s" name

let search_kernel_function name =
  try
    Globals.Functions.find_by_name name
  with Not_found -> Self.fatal "search_kernel_function: failed to find %s" name

(* Replace \binds by code adequately modifying _set and _size *)
let make_static_modif_code name lvar =
  let open Cil_builder.Pure in
  let v_set = var (search_global_var (setname name)) in
  let v_size = var (search_global_var (sizename name)) in
  let res = var (Option.get lvar.lv_origin) in
  List.rev_map ghost [
    v_set .@[ v_size ] := res;
    v_size := v_size + of_int 1
  ]

let () = Cmdline.run_after_loading_stage (fun _ -> File.never_remove_global "realloc")

(* Dynamic version *)
let make_dynamic_modif_code name lvar =
  let open Cil_builder.Pure in
  let v_set = var (search_global_var (setname name)) in
  let v_size = var (search_global_var (sizename name)) in
  let v_capacity = var (search_global_var (capname name)) in
  let res = var (Option.get lvar.lv_origin) in
  let realloc = search_kernel_function "realloc" in
  List.rev_map ghost [
    if_ (v_size > v_capacity) ~then_:[
      call realloc [
        cast (ptr void) v_set;
        of_int 2 * (v_size + of_int 1)]
    ] ~else_:[];
    mem (binop PlusPI v_set v_size) := res;
    v_size := v_size + of_int 1;
  ]

let gf () =
  match !ext_flags with
    | None -> Meta_options.Self.fatal "uninitialized bindings"
    | Some { static_bindings = None } -> make_dynamic_modif_code
    | Some { static_bindings = Some _ } -> make_static_modif_code

(* When encountering an ID, create the correct ghost stmt and fill to_add *)
let process_imeta vis = if !visit_inline then function
    | Ext_terms [ { term_node = TLval(TVar lvar, TNoOffset) };
                  { term_node = TConst(LStr name) }] ->
      let s = Option.get vis#current_stmt in
      let gf = gf () in
      let loc = Cil_datatype.Location.unknown in
      List.iter (fun v ->
          let stmt = Cil_builder.Pure.cil_stmt ~loc v in
          add_to_hash_list Stmt_Hashtbl.(find_opt, replace) to_add s stmt
        ) (gf name lvar);
      Cil.SkipChildren
    | _ -> Cil.SkipChildren
  else fun _ -> Cil.SkipChildren