package frama-c-metacsl
MetAcsl plugin of Frama-C for writing pervasives properties
Install
Dune Dependency
Authors
Maintainers
Sources
meta-0.9-beta.tar.bz2
md5=32bd324617144e618a39e0015445effb
sha512=d96bc4fb9e4c9771efeca815aa1d6f2bae0676cce56d9ed227370bacf4fb04c0811d53470cd15981406ae11a0e95af9f16ab31f7cac04ae2a92cbf85233fb496
doc/src/frama-c-metacsl.core/meta_bindings.ml.html
Source file meta_bindings.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
(**************************************************************************) (* *) (* 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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>