(**************************************************************************)
(* *)
(* 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 = Globals.Vars.find_from_astinfo name Global
(* Replace \binds by code adequately modifying _set and _size *)
let make_static_modif_code name lvar =
let unkloc = Cil_datatype.Location.unknown in
let tabvar = search_global_var (setname name) in
let sizevar = search_global_var (sizename name) in
List.rev [
(let tabcell = (Var tabvar, Index (Cil.evar sizevar, NoOffset)) in
let value = Option.get lvar.lv_origin |> Cil.evar in
Cil.mkStmtOneInstr ~ghost:true (Set (tabcell, value, unkloc)));
(let increxp = Cil.increm (Cil.evar sizevar) 1 in
Cil.mkStmtOneInstr ~ghost:true (Set (Cil.var sizevar, increxp, unkloc)))
]
(* Dynamic version *)
let make_dynamic_modif_code name lvar =
let unkloc = Cil_datatype.Location.unknown in
let tabvar = search_global_var (setname name) in
let sizevar = search_global_var (sizename name) in
let capvar = search_global_var (capname name) in
List.rev [
(let cond = Cil.mkBinOp ~loc:unkloc Gt (Cil.evar sizevar) (Cil.evar capvar) in
let newsize = Cil.mkBinOp ~loc:unkloc Mult (Cil.integer ~loc:unkloc 2)
(Cil.increm (Cil.evar sizevar) 1) in
let realloc = Globals.Functions.find_by_name "realloc" |>
Kernel_function.get_vi |> Cil.evar in
let arg = Cil.(new_exp ~loc:unkloc (CastE (Cil_const.voidPtrType, evar tabvar))) in
let incinstr = Call (None, realloc, [arg; newsize], unkloc) in
let inc = Cil.mkStmtOneInstr ~ghost:true incinstr in
Cil.mkStmt ~ghost:true (If (cond, Cil.mkBlock [inc], Cil.mkBlock [], unkloc)));
(let addr = Cil.mkBinOp ~loc:unkloc PlusPI (Cil.evar tabvar) (Cil.evar sizevar) in
let tabcell = Cil.mkMem ~addr ~off:NoOffset in
let value = Option.get lvar.lv_origin |> Cil.evar in
Cil.mkStmtOneInstr ~ghost:true (Set (tabcell, value, unkloc)));
(let increxp = Cil.increm (Cil.evar sizevar) 1 in
Cil.mkStmtOneInstr ~ghost:true (Set (Cil.var sizevar, increxp, unkloc)))
]
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
List.iter (fun (v : stmt) ->
add_to_hash_list Stmt_Hashtbl.(find_opt, replace) to_add s v
) (gf name lvar);
Cil.SkipChildren
| _ -> Cil.SkipChildren
else fun _ -> Cil.SkipChildren