Commit f8d0e42b authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'fix/slicing/lvar-of-function' into 'master'

[Kernel] Synchronization between logic and C vars representing a C function

Closes #840

See merge request frama-c/frama-c!2609
parents 110e6486 e2bb33a0
......@@ -83,8 +83,6 @@ ML_LINT_KO+=src/kernel_services/ast_queries/file.mli
ML_LINT_KO+=src/kernel_services/ast_queries/logic_const.mli
ML_LINT_KO+=src/kernel_services/ast_transformations/clone.ml
ML_LINT_KO+=src/kernel_services/ast_transformations/clone.mli
ML_LINT_KO+=src/kernel_services/ast_transformations/filter.ml
ML_LINT_KO+=src/kernel_services/ast_transformations/filter.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_category.ml
......
......@@ -1585,7 +1585,9 @@ struct
end else SkipChildren
end
in
let cleanup_var vi = vi.vtype <- Cil.visitCilType cleanup_types vi.vtype in
let cleanup_var vi =
Cil.update_var_type vi (Cil.visitCilType cleanup_types vi.vtype)
in
List.iter cleanup_var c.locals;
!currentFunctionFDEC.slocals <- !currentFunctionFDEC.slocals @ !vars;
let vars = !vars @ c.locals in
......@@ -4332,7 +4334,7 @@ let fixFormalsType formals =
end
in
let treat_one_formal v =
v.vtype <- Cil.visitCilType vis v.vtype;
Cil.update_var_type v (Cil.visitCilType vis v.vtype);
Hashtbl.add table v.vname v;
in
List.iter treat_one_formal formals
......
......@@ -1733,7 +1733,7 @@ let oneFilePass1 (f:file) : unit =
"%s@\nOld declaration is unused, silently removing it"
msg;
ignore_vi oldvi;
vi.vtype <- update_type_repr vi.vtype;
Cil.update_var_type vi (update_type_repr vi.vtype);
H.replace vEnv vi.vname vinode;
vinode.nrep <- vinode;
oldvinode.nrep <- vinode;
......
......@@ -603,10 +603,13 @@ object(self)
(match v with
| Catch_all -> b
| Catch_exn (v,[]) ->
v.vtype <- purify v.vtype; update_locals v b;assign_catched_obj v b; b
Cil.update_var_type v (purify v.vtype);
update_locals v b;
assign_catched_obj v b; b
| Catch_exn(v,aux) ->
let add_one_aux stmts (v,b) =
v.vtype <- purify v.vtype; update_locals v b;
Cil.update_var_type v (purify v.vtype);
update_locals v b;
assign_catched_obj v b;
add_unreachable_block b :: stmts
in
......@@ -615,7 +618,7 @@ object(self)
List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
in
let main_block = Cil.mkBlock aux_blocks in
v.vtype <- purify v.vtype;
Cil.update_var_type v (purify v.vtype);
update_locals v main_block;
main_block)
in
......
......@@ -540,7 +540,9 @@ and varinfo = {
(** the original name of the variable. Need not be unique. *)
mutable vtype: typ;
(** The declared type of the variable. *)
(** The declared type of the variable. For modifications of the field,
{!Cil.update_var_type} helps in synchronizing the type of the C
variable and the one of the associated logic variable. *)
mutable vattr: attributes;
(** A list of attributes associated with the variable.*)
......
......@@ -644,6 +644,14 @@ and enforceGhostBlockCoherence ?(force_ghost=false) block =
let force_ghost = force_ghost || is_ghost_else block in
List.iter (enforceGhostStmtCoherence ~force_ghost) block.bstmts
(* makes sure that the type of a C variable and the type of its associated
logic variable -if any- stay synchronized. See bts 1538 *)
let update_var_type v t =
v.vtype <- if v.vghost then typeAddGhost t else t;
match v.vlogic_var_assoc with
| None -> ()
| Some lv -> lv.lv_type <- Ctype t
(* Make a varinfo. Used mostly as a helper function below *)
let makeVarinfo
?(source=true) ?(temp=false) ?(referenced=false) ?(ghost=false) ?(loc=Location.unknown)
......@@ -728,10 +736,10 @@ let setFormals (f: fundec) (forms: varinfo list) =
assert (getFormalsDecl f.svar == f.sformals);
match unrollType f.svar.vtype with
TFun(rt, _, isva, fa) ->
f.svar.vtype <-
TFun(rt,
Some (List.map (fun a -> (a.vname, a.vtype, a.vattr)) forms),
isva, fa)
update_var_type f.svar
(TFun(rt,
Some (List.map (fun a -> (a.vname, a.vtype, a.vattr)) forms),
isva, fa));
| _ ->
Kernel.fatal "Set formals. %s does not have function type" f.svar.vname
......@@ -2649,9 +2657,10 @@ and childrenVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
let o = Visitor_behavior.Get_orig.logic_var vis#behavior lv in
visitCilLogicVarDecl vis o
in
v.vtype <- visitCilType vis v.vtype;
let typ = visitCilType vis v.vtype in
v.vattr <- visitCilAttributes vis v.vattr;
v.vlogic_var_assoc <- optMapNoCopy visit_orig_var_assoc v.vlogic_var_assoc;
update_var_type v typ;
v
and visitCilVarUse vis v =
......@@ -3610,7 +3619,7 @@ let getReturnType t =
let setReturnTypeVI (v: varinfo) (t: typ) =
match unrollType v.vtype with
| TFun (_, args, va, a) ->
v.vtype <- TFun (t, args, va, a)
update_var_type v (TFun (t, args, va, a));
| _ -> Kernel.fatal "setReturnType: not a function type"
let setReturnType (f:fundec) (t:typ) =
......@@ -5383,12 +5392,11 @@ let setFunctionType (f: fundec) (t: typ) =
if List.length f.sformals <> List.length args then
Kernel.fatal ~current:true "setFunctionType: number of arguments differs from the number of formals" ;
(* Change the function type. *)
f.svar.vtype <- t;
update_var_type f.svar t;
(* Change the sformals and we know that indirectly we'll change the
* function type *)
List.iter2
(fun (_an,at,aa) f ->
f.vtype <- at; f.vattr <- aa)
(fun (_an,at,aa) f -> update_var_type f at; f.vattr <- aa)
args f.sformals
| _ -> Kernel.fatal ~current:true "setFunctionType: not a function type"
......@@ -5402,7 +5410,7 @@ let setFunctionTypeMakeFormals (f: fundec) (t: typ) =
Kernel.fatal ~current:true "setFunctionTypMakeFormals called on function %s with some formals already"
f.svar.vname ;
(* Change the function type. *)
f.svar.vtype <- t;
update_var_type f.svar t;
f.sformals <-
List.map (fun (n,t,_a) -> makeLocal ~formal:true f n t) args;
setFunctionType f t
......@@ -6505,14 +6513,6 @@ let is_modifiable_lval lv =
| _ -> (not (isConstType t)
|| is_mutable_or_initialized lv) && isCompleteType t
(* makes sure that the type of a C variable and the type of its associated
logic variable -if any- stay synchronized. See bts 1538 *)
let update_var_type v t =
v.vtype <- if v.vghost then typeAddGhost t else t;
match v.vlogic_var_assoc with
| None -> ()
| Some lv -> lv.lv_type <- Ctype t
(** Uniquefy the variable names *)
let uniqueVarNames (f: file) : unit =
(* Setup the alpha conversion table for globals *)
......
......@@ -33,13 +33,13 @@ module type RemoveInfo = sig
(** exception that fun_assign_visible should raise to indicate that
the corresponding assigns clause should be erased entirely
*)
*)
exception EraseAssigns
(** exception that fun_frees_visible or fun_allocates_visible should
raise to indicate that the corresponding allocation clause should
(** exception that fun_frees_visible or fun_allocates_visible should
raise to indicate that the corresponding allocation clause should
be erased entirely
*)
*)
exception EraseAllocation
(** some type for the whole project information *)
......@@ -49,22 +49,22 @@ module type RemoveInfo = sig
type fct
(** This function will be called for each function of the source program.
* A new function will be created for each element of the returned list.
* A new function will be created for each element of the returned list.
*)
val fct_info : proj -> kernel_function -> fct list
(** useful when we want to have several functions in the result for one
* source function. If it is not the case, you can return [varinfo.vname].
* It is the responsibility of the user to given different names to different
* function. *)
* source function. If it is not the case, you can return [varinfo.vname].
* It is the responsibility of the user to given different names to different
* function. *)
val fct_name : varinfo -> fct -> string
(** tells if the n-th formal parameter is visible. *)
val param_visible : fct -> int -> bool
(** tells if the body of a function definition is visible.
* True is most cases, but can be defined to be false when we want to export
* only the declaration of a function instead of its definition *)
* True is most cases, but can be defined to be false when we want to export
* only the declaration of a function instead of its definition *)
val body_visible : fct -> bool
(** tells if the local variable is visible. *)
......@@ -87,35 +87,35 @@ module type RemoveInfo = sig
val fun_allocates_visible : fct -> identified_term -> bool
val fun_assign_visible : fct -> from -> bool
(** true if the assigned value (first component of the from) is visible
@raise EraseAssigns to indicate that the corresponding assigns clause
should be erased entirely (i.e. assigns everything. If it were to
just return false to all elements, this would result in assigns \nothing
*)
(** true if the assigned value (first component of the from) is visible
@raise EraseAssigns to indicate that the corresponding assigns clause
should be erased entirely (i.e. assigns everything. If it were to
just return false to all elements, this would result in assigns \nothing
*)
val fun_deps_visible : fct -> identified_term -> bool
(** true if the corresponding functional dependency is visible. *)
(** true if the corresponding functional dependency is visible. *)
(** [called_info] will be called only if the call statement is visible.
* If it returns [None], the source call will be visible,
* else it will use the returned [fct] to know if the return value and the
* arguments are visible.
* The input [fct] parameter is the one of the caller function.
* *)
* If it returns [None], the source call will be visible,
* else it will use the returned [fct] to know if the return value and the
* arguments are visible.
* The input [fct] parameter is the one of the caller function.
* *)
val called_info : proj * fct -> stmt ->
(kernel_function * fct) option
(kernel_function * fct) option
(** tells if the lvalue of the call has to be visible *)
val res_call_visible : fct -> stmt -> bool
(** tells if the function returns something or if the result is [void].
* Notice that if this function returns [true] the function will have the same
* return type than the original function. So, if it was already [void], it
* makes no difference if this function returns true or false.
*
* - For a defined function, this should give the same result than
* [inst_visible fct_info (Kernel_function.find_return kf)].
* - [res_call_visible] must return [false]
* if [result_visible] returns false on the called function.
* Notice that if this function returns [true] the function will have the same
* return type than the original function. So, if it was already [void], it
* makes no difference if this function returns true or false.
*
* - For a defined function, this should give the same result than
* [inst_visible fct_info (Kernel_function.find_return kf)].
* - [res_call_visible] must return [false]
* if [result_visible] returns false on the called function.
*)
val result_visible : kernel_function -> fct -> bool
......@@ -128,7 +128,7 @@ module type RemoveInfo = sig
end
(** Given a module that match the module type described above,
* [F.build_cil_file] initializes a new project containing the slices
* [F.build_cil_file] initializes a new project containing the slices
*)
module F (Info : RemoveInfo) : sig
......
......@@ -248,7 +248,8 @@ let inliner functions_to_inline = object (self)
(* Inlining will prevent r to be syntactically seen as initialized
or const: *)
r.vdefined <- false;
r.vtype <- Cil.typeRemoveAttributes ["const"] r.vtype;
Cil.update_var_type
r (Cil.typeRemoveAttributes ["const"] r.vtype);
false, None, (Cil.mkAddrOf loc (Cil.var r)) :: args
| Some _, _ ->
Kernel.fatal "Attempt to initialize an inexistent varinfo"
......
......@@ -125,7 +125,7 @@ class visit_adding_code_for_synchronisation =
- what about varargs?
*)
let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
vi_pre.vtype <- TFun(Cil.voidType, args, varargs,[]);
Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
vi_pre.vattr <- [];
(* in particular get rid of __no_return if set in vi*)
......
......@@ -584,7 +584,7 @@ let inject_in_fundec main fundec =
(* convert ghost variables *)
vi.vghost <- false;
let unghost_local vi =
vi.vtype <- Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype ;
Cil.update_var_type vi (Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype);
vi.vghost <- false
in
List.iter unghost_local fundec.slocals;
......@@ -621,12 +621,12 @@ let unghost_vi vi =
(* do not convert extern ghost variables, because they can't be linked,
see bts #1392 *)
if vi.vstorage <> Extern then vi.vghost <- false;
vi.vtype <- Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype ;
Cil.update_var_type vi (Cil.typeRemoveAttributesDeep ["ghost"] vi.vtype);
match Cil.unrollType vi.vtype with
| TFun(res, Some l, va, attr) ->
(* unghostify function's parameters *)
let retype (n, t, a) = n, t, Cil.dropAttribute Cil.frama_c_ghost_formal a in
vi.vtype <- TFun(res, Some (List.map retype l), va, attr)
Cil.update_var_type vi (TFun(res, Some (List.map retype l), va, attr))
| _ ->
()
......
......@@ -454,7 +454,7 @@ let update_variable_validity ?(make_weak=false) base sizev =
(* Mutating the type of a varinfo is not exactly a good idea. This is
probably fine here, because the type of a malloced variable is
almost never used. *)
vi.vtype <- weaken_type vi.vtype;
Cil.update_var_type vi (weaken_type vi.vtype);
end;
Base.update_variable_validity variable_v
~weak:make_weak ~min_alloc:min_sure_bits ~max_alloc:max_valid_bits;
......
......@@ -40,7 +40,7 @@ class transform prj = object(_self)
typ, Some (vtype @ [ "ok", Cil.intType, [] ]),
varity, attr)
in
vi.vtype <- new_fun_typ;
Cil.update_var_type vi new_fun_typ;
Project.on
prj
(fun () -> Cil.setFormalsDecl vi new_fun_typ;) ();
......
/* run.config*
OPT: -slice-pragma main -then-last -print
*/
int g(int x) { return x; }
int main() {
/*@ assert &g == &g; */
/*@ slice pragma stmt; */
g(0);
}
[kernel] Parsing tests/slicing/function_lvar.i (no preprocessing)
[slicing] slicing requests in progress...
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
2 functions analyzed (out of 2): 100% coverage.
In these functions, 5 statements reached (out of 5): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
0 alarms generated by the analysis.
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 1 valid 0 unknown 0 invalid 1 total
Preconditions 0 valid 0 unknown 0 invalid 0 total
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[slicing] initializing slicing ...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function main
[from] Computing for function g
[from] Done for function g
[pdg] done for function main
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[slicing] applying all slicing requests...
[slicing] applying 1 actions...
[slicing] applying actions: 1/1...
[pdg] computing for function g
[pdg] done for function g
[slicing] exporting project to 'Slicing export'...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
int g(int x);
void g_slice_1(void)
{
return;
}
void main(void)
{
/*@ assert &g ≡ &g; */ ;
/*@ slice pragma stmt; */
g_slice_1();
return;
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment