From e5647c8d35b529b71e741e57bf627ed8cbb046a9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 31 Mar 2020 20:29:33 +0200
Subject: [PATCH] linting
---
.Makefile.lint | 2 -
.../ast_transformations/filter.ml | 756 +++++++++---------
.../ast_transformations/filter.mli | 62 +-
3 files changed, 410 insertions(+), 410 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 0fffac31e24..e0d284e28cb 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -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
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 74c0ccc4622..95bbf5768ae 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -91,9 +91,9 @@ end = struct
with Not_found ->
let fundec =
match kf.fundec with
- | Definition(f,l) -> Definition ( { f with svar = v },l)
- | Declaration(_,_,arg,l) ->
- Declaration(Cil.empty_funspec(),v,arg,l)
+ | Definition(f,l) -> Definition ( { f with svar = v },l)
+ | Declaration(_,_,arg,l) ->
+ Declaration(Cil.empty_funspec(),v,arg,l)
in
let kf = { fundec = fundec; spec = Cil.empty_funspec() } in
Cil_datatype.Varinfo.Hashtbl.add tbl v kf; kf
@@ -101,13 +101,13 @@ end = struct
let rec can_skip keep_stmts stmt =
stmt.labels = [] &&
match stmt.skind with
- | Instr (Skip _) ->
- debug "@[Statement %d: can%s skip@]@." stmt.sid
- (if Stmt.Set.mem stmt keep_stmts then "'t" else "");
- not (Stmt.Set.mem stmt keep_stmts)
- | Block b -> is_empty_block keep_stmts b
- | UnspecifiedSequence seq -> is_empty_unspecified_sequence keep_stmts seq
- | _ -> false
+ | Instr (Skip _) ->
+ debug "@[Statement %d: can%s skip@]@." stmt.sid
+ (if Stmt.Set.mem stmt keep_stmts then "'t" else "");
+ not (Stmt.Set.mem stmt keep_stmts)
+ | Block b -> is_empty_block keep_stmts b
+ | UnspecifiedSequence seq -> is_empty_unspecified_sequence keep_stmts seq
+ | _ -> false
and is_empty_block keep_stmts block =
List.for_all (can_skip keep_stmts) block.bstmts
@@ -117,44 +117,44 @@ end = struct
let rec mk_new_block keep_stmts s blk loc =
(* vblock has already cleaned up the statements (removed skip, etc...),
- * but now the block can still be empty or include only one statement. *)
+ * but now the block can still be empty or include only one statement. *)
match blk.bstmts with
- | [] | _ when is_empty_block keep_stmts blk ->
- (* don't care about local variables since the block is empty. *)
- mk_new_stmt s (mk_skip loc)
- | { labels = [] } as s1 :: [] ->
- (* one statement only, and no label *)
- begin
- match s1.skind with
- | Block b ->
- (* drop blk, but keep local declarations. *)
- b.blocals <- b.blocals @ blk.blocals;
- mk_new_block keep_stmts s b loc
- | UnspecifiedSequence seq when blk.blocals = [] ->
- mk_new_unspecified_sequence keep_stmts s seq loc
- | _ when blk.blocals = [] -> mk_new_stmt s s1.skind
- | _ -> mk_new_stmt s (Block blk)
- end
- | _ -> mk_new_stmt s (Block blk)
+ | [] | _ when is_empty_block keep_stmts blk ->
+ (* don't care about local variables since the block is empty. *)
+ mk_new_stmt s (mk_skip loc)
+ | { labels = [] } as s1 :: [] ->
+ (* one statement only, and no label *)
+ begin
+ match s1.skind with
+ | Block b ->
+ (* drop blk, but keep local declarations. *)
+ b.blocals <- b.blocals @ blk.blocals;
+ mk_new_block keep_stmts s b loc
+ | UnspecifiedSequence seq when blk.blocals = [] ->
+ mk_new_unspecified_sequence keep_stmts s seq loc
+ | _ when blk.blocals = [] -> mk_new_stmt s s1.skind
+ | _ -> mk_new_stmt s (Block blk)
+ end
+ | _ -> mk_new_stmt s (Block blk)
(* same as above, but for unspecified sequences. *)
and mk_new_unspecified_sequence keep_stmts s seq loc =
(* vblock has already cleaned up the statements (removed skip, etc...),
* but now the block can still be empty or include only one statement. *)
match seq with
- | [] -> mk_new_stmt s (mk_skip loc)
- | _ when is_empty_unspecified_sequence keep_stmts seq ->
- mk_new_stmt s (mk_skip loc)
- | [stmt,_,_,_,_] -> (* one statement only *)
- begin
- if stmt.labels <> [] then s.labels <- s.labels @ stmt.labels;
- match stmt.skind with
- | UnspecifiedSequence seq ->
- mk_new_unspecified_sequence keep_stmts s seq loc
- | Block b -> mk_new_block keep_stmts s b loc
- | _ -> mk_new_stmt s stmt.skind
- end
- | _ -> mk_new_stmt s (UnspecifiedSequence seq)
+ | [] -> mk_new_stmt s (mk_skip loc)
+ | _ when is_empty_unspecified_sequence keep_stmts seq ->
+ mk_new_stmt s (mk_skip loc)
+ | [stmt,_,_,_,_] -> (* one statement only *)
+ begin
+ if stmt.labels <> [] then s.labels <- s.labels @ stmt.labels;
+ match stmt.skind with
+ | UnspecifiedSequence seq ->
+ mk_new_unspecified_sequence keep_stmts s seq loc
+ | Block b -> mk_new_block keep_stmts s b loc
+ | _ -> mk_new_stmt s stmt.skind
+ end
+ | _ -> mk_new_stmt s (UnspecifiedSequence seq)
let add_label_if_needed mk_label finfo s =
let rec pickLabel = function
@@ -162,141 +162,141 @@ end = struct
| Label _ as lab :: _ when Info.label_visible finfo s lab -> Some lab
| _ :: rest -> pickLabel rest
in match pickLabel s.labels with
- | Some _ -> None
- | None ->
- let label = mk_label (Cil_datatype.Stmt.loc s) in
- debug "add label to sid:%d : %a" s.sid Printer.pp_label label;
- s.labels <- label::s.labels;
- Some label
-
- let rm_break_cont ?(cont=true) ?(break=true) mk_label finfo blk =
+ | Some _ -> None
+ | None ->
+ let label = mk_label (Cil_datatype.Stmt.loc s) in
+ debug "add label to sid:%d : %a" s.sid Printer.pp_label label;
+ s.labels <- label::s.labels;
+ Some label
+
+ let rm_break_cont ?(cont=true) ?(break=true) mk_label finfo blk =
let change loc s =
let dest = match s.succs with dest::_ -> dest | [] -> assert false in
let new_l = add_label_if_needed mk_label finfo dest in
- mk_new_stmt s (Goto (ref dest, loc));
- debug "changed break/continue into @[%a@]@."
- Printer.pp_stmt s;
- new_l
+ mk_new_stmt s (Goto (ref dest, loc));
+ debug "changed break/continue into @[%a@]@."
+ Printer.pp_stmt s;
+ new_l
in
let rec rm_aux cont break s =
match s.skind with
- | Break loc when break && Info.inst_visible finfo s ->
- let _ = change loc s in ()
- | Continue loc when cont && Info.inst_visible finfo s ->
- let _ = change loc s in ()
- | Instr _ | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> ()
- | If (_, bthen, belse, _) ->
- List.iter (rm_aux cont break) bthen.bstmts;
- List.iter (rm_aux cont break) belse.bstmts;
- | Block blk ->
- List.iter (rm_aux cont break) blk.bstmts
- | UnspecifiedSequence seq ->
- let blk = Cil.block_from_unspecified_sequence seq in
- List.iter (rm_aux cont break) blk.bstmts
- | Loop _ -> (* don't go inside : break and continue change meaning*)
- ()
- | Switch (_, blk, _, _) ->
- (* if change [continue] do it, but stop changing [break] *)
- if cont then
- let break = false in List.iter (rm_aux cont break) blk.bstmts
- | TryFinally _ | TryExcept _ | TryCatch _ -> (* TODO ? *) ()
+ | Break loc when break && Info.inst_visible finfo s ->
+ let _ = change loc s in ()
+ | Continue loc when cont && Info.inst_visible finfo s ->
+ let _ = change loc s in ()
+ | Instr _ | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> ()
+ | If (_, bthen, belse, _) ->
+ List.iter (rm_aux cont break) bthen.bstmts;
+ List.iter (rm_aux cont break) belse.bstmts;
+ | Block blk ->
+ List.iter (rm_aux cont break) blk.bstmts
+ | UnspecifiedSequence seq ->
+ let blk = Cil.block_from_unspecified_sequence seq in
+ List.iter (rm_aux cont break) blk.bstmts
+ | Loop _ -> (* don't go inside : break and continue change meaning*)
+ ()
+ | Switch (_, blk, _, _) ->
+ (* if change [continue] do it, but stop changing [break] *)
+ if cont then
+ let break = false in List.iter (rm_aux cont break) blk.bstmts
+ | TryFinally _ | TryExcept _ | TryCatch _ -> (* TODO ? *) ()
in List.iter (rm_aux cont break) blk.bstmts
(** filter [params] according to [ff] input visibility.
- * Can be used to slice both the parameters, the call arguments,
- * and the param types.
- * Notice that this is just a filtering of the list.
- * It doesn't do any transformation of any kind on the element,
- * so at the end they are shared with the original list.
- * *)
+ * Can be used to slice both the parameters, the call arguments,
+ * and the param types.
+ * Notice that this is just a filtering of the list.
+ * It doesn't do any transformation of any kind on the element,
+ * so at the end they are shared with the original list.
+ * *)
let filter_params finfo params =
let do_param (n, new_params) var =
let new_params =
if not (Info.param_visible finfo n) then new_params
else new_params @ [var]
in
- (n+1, new_params)
+ (n+1, new_params)
in let _, new_params = List.fold_left do_param (1, []) params in
- new_params
+ new_params
let ff_var (fun_vars: t) kf finfo =
let fct_var = Kernel_function.get_vi kf in
let name = Info.fct_name fct_var finfo in
- try
- let ff_var = Hashtbl.find fun_vars name in
- debug "[ff_var] Use fct var %s:%d@." ff_var.vname ff_var.vid;
- ff_var
- with Not_found ->
- let ff_var = Cil.copyVarinfo fct_var name in
- if not (Info.result_visible kf finfo) then
- Cil.setReturnTypeVI ff_var Cil.voidType;
- (* Notice that we don't have to filter the parameter types here :
- * they will be update by [Cil.setFormals] later on. *)
- debug "[ff_var] Mem fct var %s:%d@."
- ff_var.vname ff_var.vid;
- Hashtbl.add fun_vars name ff_var;
- ff_var
+ try
+ let ff_var = Hashtbl.find fun_vars name in
+ debug "[ff_var] Use fct var %s:%d@." ff_var.vname ff_var.vid;
+ ff_var
+ with Not_found ->
+ let ff_var = Cil.copyVarinfo fct_var name in
+ if not (Info.result_visible kf finfo) then
+ Cil.setReturnTypeVI ff_var Cil.voidType;
+ (* Notice that we don't have to filter the parameter types here :
+ * they will be update by [Cil.setFormals] later on. *)
+ debug "[ff_var] Mem fct var %s:%d@."
+ ff_var.vname ff_var.vid;
+ Hashtbl.add fun_vars name ff_var;
+ ff_var
let optim_if fct keep_stmts s_orig s cond_opt bthen belse loc =
let empty_then = is_empty_block keep_stmts bthen in
let empty_else = is_empty_block keep_stmts belse in
debug "[optim_if] @[sid:%d (orig:%d)@ \
- with %s cond, %s empty then, %s empty else@]@."
+ with %s cond, %s empty then, %s empty else@]@."
s.sid s_orig.sid
(if cond_opt = None then "no" else "")
(if empty_then then "" else "not")
(if empty_else then "" else "not");
match cond_opt with
- | Some cond ->
- if empty_then && empty_else then mk_new_stmt s (mk_skip loc)
- else (* cond visible and something in blocks : keep if *)
- mk_new_stmt s (If (cond, bthen, belse, loc))
+ | Some cond ->
+ if empty_then && empty_else then mk_new_stmt s (mk_skip loc)
+ else (* cond visible and something in blocks : keep if *)
+ mk_new_stmt s (If (cond, bthen, belse, loc))
| None -> (* no cond *)
- let go_then, go_else = Info.cond_edge_visible fct s_orig in
- debug
- "[condition_truth_value] can go in then = %b - can go in else =%b@."
- go_then go_else;
- match go_then, empty_then, go_else, empty_else with
- | _, true, _, true -> (* both blocks empty -> skip *)
- mk_new_stmt s (mk_skip loc)
- | true, false, false, true ->
- (* else empty and always go to then -> block then *)
- mk_new_block keep_stmts s bthen loc
- | false, true, true, false ->
- (* then empty and always go to else -> block else *)
- mk_new_block keep_stmts s belse loc
- | false, false, true, _ ->
- (* always goes in the 'else' branch,
- * but the then branch is not empty : *)
- mk_new_stmt s (If (Cil.zero ~loc, bthen, belse, loc))
- | true, false, false, false ->
- (* always goes in the 'then' branch,
- * but the else branch is not empty :
- *)
- mk_new_stmt s (If (Cil.one ~loc, bthen, belse, loc))
- | true, true, false, false ->
- (* always goes in the 'then' empty branch,
- * but the else branch is not empty :
- * build (if (0) belse else empty.
- *)
- mk_new_stmt s (If (Cil.zero ~loc, belse, bthen, loc))
- | true, false, true, false
- | false, false, false, false ->
- (* if both go_then and go_else are true:
- * can go in both branch but don't depend on cond ?
- * probably unreachable IF with reachable blocks by goto.
- * if both go_else and go_else are false:
- * never goes in any branch ?
- * both branch visible -> dummy condition *)
- mk_new_stmt s (If (Cil.one ~loc, bthen, belse, loc))
- | true, _, true, true
- | false, _, false, true ->
- (* can go in both or no branch (see above) : empty else *)
- mk_new_block keep_stmts s bthen loc
- | true, true, true, _
- | false, true, false, _ ->
- (* can go in both or no branch (see above) : empty then *)
- mk_new_block keep_stmts s belse loc
+ let go_then, go_else = Info.cond_edge_visible fct s_orig in
+ debug
+ "[condition_truth_value] can go in then = %b - can go in else =%b@."
+ go_then go_else;
+ match go_then, empty_then, go_else, empty_else with
+ | _, true, _, true -> (* both blocks empty -> skip *)
+ mk_new_stmt s (mk_skip loc)
+ | true, false, false, true ->
+ (* else empty and always go to then -> block then *)
+ mk_new_block keep_stmts s bthen loc
+ | false, true, true, false ->
+ (* then empty and always go to else -> block else *)
+ mk_new_block keep_stmts s belse loc
+ | false, false, true, _ ->
+ (* always goes in the 'else' branch,
+ * but the then branch is not empty : *)
+ mk_new_stmt s (If (Cil.zero ~loc, bthen, belse, loc))
+ | true, false, false, false ->
+ (* always goes in the 'then' branch,
+ * but the else branch is not empty :
+ *)
+ mk_new_stmt s (If (Cil.one ~loc, bthen, belse, loc))
+ | true, true, false, false ->
+ (* always goes in the 'then' empty branch,
+ * but the else branch is not empty :
+ * build (if (0) belse else empty.
+ *)
+ mk_new_stmt s (If (Cil.zero ~loc, belse, bthen, loc))
+ | true, false, true, false
+ | false, false, false, false ->
+ (* if both go_then and go_else are true:
+ * can go in both branch but don't depend on cond ?
+ * probably unreachable IF with reachable blocks by goto.
+ * if both go_else and go_else are false:
+ * never goes in any branch ?
+ * both branch visible -> dummy condition *)
+ mk_new_stmt s (If (Cil.one ~loc, bthen, belse, loc))
+ | true, _, true, true
+ | false, _, false, true ->
+ (* can go in both or no branch (see above) : empty else *)
+ mk_new_block keep_stmts s bthen loc
+ | true, true, true, _
+ | false, true, false, _ ->
+ (* can go in both or no branch (see above) : empty then *)
+ mk_new_block keep_stmts s belse loc
let visible_lval vars_visible lval =
let visitor = object
@@ -318,13 +318,13 @@ end = struct
in List.fold_right build l []
(** This visitor is to be used to filter a function.
- * It does a deep copy of the source function without the invisible elements.
- * It also change the function declaration and filter the function calls.
- *
- * Many ideas come from [Cil.copyFunctionVisitor] but we were not able to
- * directly inherit from it since some processing would not have worked in our
- * context (like the [sid] computation for instance).
- * *)
+ * It does a deep copy of the source function without the invisible elements.
+ * It also change the function declaration and filter the function calls.
+ *
+ * Many ideas come from [Cil.copyFunctionVisitor] but we were not able to
+ * directly inherit from it since some processing would not have worked in our
+ * context (like the [sid] computation for instance).
+ * *)
class filter_visitor pinfo prj = object(self)
inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy prj)
@@ -340,19 +340,19 @@ end = struct
val lab_num = ref 0;
val lab_prefix = "break_cont"
- method private fresh_label loc =
+ method private fresh_label loc =
incr lab_num;
let lname = Printf.sprintf "%s_%d" lab_prefix !lab_num in
Label (lname, loc, false)
method private is_our_label label = match label with
- | Label (lname, _, false) ->
- let ok =
- try
- let prefix = String.sub lname 0 (String.length lab_prefix) in
- prefix = lab_prefix
- with Invalid_argument _ -> false
- in ok
- | _ -> false
+ | Label (lname, _, false) ->
+ let ok =
+ try
+ let prefix = String.sub lname 0 (String.length lab_prefix) in
+ prefix = lab_prefix
+ with Invalid_argument _ -> false
+ in ok
+ | _ -> false
method private get_finfo () = Extlib.the fi
@@ -366,7 +366,7 @@ end = struct
if v.vglob
then
try let v' = (Hashtbl.find fun_vars v.vname) in
- Cil.ChangeTo v'
+ Cil.ChangeTo v'
with Not_found ->
Cil.SkipChildren
else Cil.SkipChildren (*copy has already been done by default visitor*)
@@ -394,17 +394,17 @@ end = struct
let formals = filter_params (self#get_finfo ()) formals in
List.map
(fun v ->
- Varinfo.Hashtbl.add local_visible v ();
- let v' = Cil.copyVarinfo v v.vname in
- Visitor_behavior.Set.varinfo self#behavior v v';
- Visitor_behavior.Set_orig.varinfo self#behavior v' v;
- (match v.vlogic_var_assoc, v'.vlogic_var_assoc with
- None, None -> ()
- | Some lv, Some lv' ->
- Visitor_behavior.Set.logic_var self#behavior lv lv';
- Visitor_behavior.Set_orig.logic_var self#behavior lv' lv
- | _ -> assert false (* copy should be faithful *));
- v')
+ Varinfo.Hashtbl.add local_visible v ();
+ let v' = Cil.copyVarinfo v v.vname in
+ Visitor_behavior.Set.varinfo self#behavior v v';
+ Visitor_behavior.Set_orig.varinfo self#behavior v' v;
+ (match v.vlogic_var_assoc, v'.vlogic_var_assoc with
+ None, None -> ()
+ | Some lv, Some lv' ->
+ Visitor_behavior.Set.logic_var self#behavior lv lv';
+ Visitor_behavior.Set_orig.logic_var self#behavior lv' lv
+ | _ -> assert false (* copy should be faithful *));
+ v')
formals
method private filter_locals locals =
@@ -421,15 +421,15 @@ end = struct
Visitor_behavior.Set.varinfo self#behavior var var';
Visitor_behavior.Set_orig.varinfo self#behavior var' var;
(match var.vlogic_var_assoc, var'.vlogic_var_assoc with
- None, None -> ()
- | Some lv, Some lv' ->
- Visitor_behavior.Set.logic_var self#behavior lv lv';
- Visitor_behavior.Set_orig.logic_var self#behavior lv' lv
- | _ -> assert false (* copy should be faithful *));
+ None, None -> ()
+ | Some lv, Some lv' ->
+ Visitor_behavior.Set.logic_var self#behavior lv lv';
+ Visitor_behavior.Set_orig.logic_var self#behavior lv' lv
+ | _ -> assert false (* copy should be faithful *));
var' :: (filter locals)
end else filter locals
in let new_locals = filter locals in
- new_locals
+ new_locals
method! vcode_annot v =
Extlib.may Cil.CurrentLoc.set (Cil_datatype.Code_annotation.loc v);
@@ -495,18 +495,18 @@ end = struct
(* This optim must be performed after the sliced annotations have
been put in the new table. Hence, we must put the action into
the queue.
- *)
+ *)
Queue.add
(fun () ->
- b'.bstmts <-
- List.filter
- (fun st ->
- not (Cil.is_skip st.skind)
- || st.labels <> []
- || Annotations.has_code_annot st
- (*|| ((*Format.eprintf "Skipping %d@.@." st.sid;*) false)*)
- )
- b'.bstmts)
+ b'.bstmts <-
+ List.filter
+ (fun st ->
+ not (Cil.is_skip st.skind)
+ || st.labels <> []
+ || Annotations.has_code_annot st
+ (*|| ((*Format.eprintf "Skipping %d@.@." st.sid;*) false)*)
+ )
+ b'.bstmts)
self#get_filling_actions;
b'
in
@@ -526,7 +526,7 @@ end = struct
Visitor_behavior.Set.stmt self#behavior orig s;
Visitor_behavior.Set_orig.stmt self#behavior s orig;
if keep then self#add_stmt_keep s;
- debug "@[finalize sid:%d->sid:%d@]@\n@." old s.sid
+ debug "@[finalize sid:%d->sid:%d@]@\n@." old s.sid
method private process_invisible_stmt s =
let finfo = self#get_finfo () in
@@ -537,37 +537,37 @@ end = struct
self#change_sid s;
s.skind <- oldskind;
(match s.skind with
- | If (_,bthen,belse,loc) ->
- let bthen = Cil.visitCilBlock (self:>Cil.cilVisitor) bthen in
- let belse = Cil.visitCilBlock (self:>Cil.cilVisitor) belse in
- let s_orig = Visitor_behavior.Get_orig.stmt self#behavior s in
- optim_if finfo keep_stmts s_orig s None bthen belse loc
- | Switch (_exp, body, _, loc) ->
- (* the switch is invisible : it can be translated into a block. *)
- rm_break_cont ~cont:false (self#fresh_label) finfo body;
- let block = Cil.visitCilBlock (self:>Cil.cilVisitor) body in
- (mk_new_block keep_stmts s block loc)
- | Loop (_, body, loc, _lcont, _lbreak) ->
- rm_break_cont (self#fresh_label) finfo body;
- let bloop = Cil.visitCilBlock (self:>Cil.cilVisitor) body in
- mk_new_block keep_stmts s bloop loc
- | Block _ | UnspecifiedSequence _ ->
- assert false (* a block is always visible *)
- | TryFinally _ | TryExcept _ -> assert false (*TODO*)
- | Return (_,l) -> mk_new_stmt s (Return (None,l))
- | Instr (Local_init (v, _, _)) ->
- (* The initialization of the variable is useless (e.g. because it is
- overwritten before being read). Just treat it as uninitialized.
- Note that if the variable itself is invisible, we don't have
- anything to do: it will not appear at all in the function.
- *)
- if Info.loc_var_visible (self#get_finfo()) v then begin
- let v' = Visitor_behavior.Get.varinfo self#behavior v in
- v'.vdefined <- false;
- end;
- mk_new_stmt s (mk_stmt_skip s)
- | _ -> mk_new_stmt s (mk_stmt_skip s));
- debug "@[<hov 10>[process_invisible_stmt] gives sid:%d@ @[%a@]@]@."
+ | If (_,bthen,belse,loc) ->
+ let bthen = Cil.visitCilBlock (self:>Cil.cilVisitor) bthen in
+ let belse = Cil.visitCilBlock (self:>Cil.cilVisitor) belse in
+ let s_orig = Visitor_behavior.Get_orig.stmt self#behavior s in
+ optim_if finfo keep_stmts s_orig s None bthen belse loc
+ | Switch (_exp, body, _, loc) ->
+ (* the switch is invisible : it can be translated into a block. *)
+ rm_break_cont ~cont:false (self#fresh_label) finfo body;
+ let block = Cil.visitCilBlock (self:>Cil.cilVisitor) body in
+ (mk_new_block keep_stmts s block loc)
+ | Loop (_, body, loc, _lcont, _lbreak) ->
+ rm_break_cont (self#fresh_label) finfo body;
+ let bloop = Cil.visitCilBlock (self:>Cil.cilVisitor) body in
+ mk_new_block keep_stmts s bloop loc
+ | Block _ | UnspecifiedSequence _ ->
+ assert false (* a block is always visible *)
+ | TryFinally _ | TryExcept _ -> assert false (*TODO*)
+ | Return (_,l) -> mk_new_stmt s (Return (None,l))
+ | Instr (Local_init (v, _, _)) ->
+ (* The initialization of the variable is useless (e.g. because it is
+ overwritten before being read). Just treat it as uninitialized.
+ Note that if the variable itself is invisible, we don't have
+ anything to do: it will not appear at all in the function.
+ *)
+ if Info.loc_var_visible (self#get_finfo()) v then begin
+ let v' = Visitor_behavior.Get.varinfo self#behavior v in
+ v'.vdefined <- false;
+ end;
+ mk_new_stmt s (mk_stmt_skip s)
+ | _ -> mk_new_stmt s (mk_stmt_skip s));
+ debug "@[<hov 10>[process_invisible_stmt] gives sid:%d@ @[%a@]@]@."
s.sid Printer.pp_stmt s;
s
in
@@ -579,10 +579,10 @@ end = struct
we must remove the local static attr indicating that they in fact
come from a block:
- if the block in which they are in scope disappears completely,
- or if the enclosing function itself disappears
- (making the variable a good candidate to be removed altogether)
+ or if the enclosing function itself disappears
+ (making the variable a good candidate to be removed altogether)
- or if we make multiple copies of the enclosing functions (otherwise,
- we would have multiple syntactic scope for the same variable).
+ we would have multiple syntactic scope for the same variable).
*)
method private remove_local_static_attr v =
let new_v = Visitor_behavior.Get.varinfo self#behavior v in
@@ -592,74 +592,74 @@ end = struct
debug "[process_visible_stmt] does sid:%d@." s.sid;
let finfo = self#get_finfo () in
(match s.skind with
- | Instr (Call (lval, f, args, loc)) ->
- let new_call = self#process_call false s lval f args loc in
- mk_new_stmt s new_call
- | Instr (Local_init(v, ConsInit(f, args, kind), loc)) ->
- let new_call =
- Cil.treat_constructor_as_func
- (self#process_call true s) v f args kind loc
- in
- (match new_call with
- | Instr(Call _) ->
- (* initialization's result was found to be useless. *)
- v.vdefined <- false
- | _ -> ());
- mk_new_stmt s new_call
- | _ -> () (* copy the statement before modifying it *)
- (* mk_new_stmt s [] s.skind *)
+ | Instr (Call (lval, f, args, loc)) ->
+ let new_call = self#process_call false s lval f args loc in
+ mk_new_stmt s new_call
+ | Instr (Local_init(v, ConsInit(f, args, kind), loc)) ->
+ let new_call =
+ Cil.treat_constructor_as_func
+ (self#process_call true s) v f args kind loc
+ in
+ (match new_call with
+ | Instr(Call _) ->
+ (* initialization's result was found to be useless. *)
+ v.vdefined <- false
+ | _ -> ());
+ mk_new_stmt s new_call
+ | _ -> () (* copy the statement before modifying it *)
+ (* mk_new_stmt s [] s.skind *)
);
let do_after s' =
self#change_sid s';
(match s'.skind with
- | If (cond,bthen,belse,loc) ->
- let s_orig = Visitor_behavior.Get_orig.stmt self#behavior s' in
- optim_if finfo keep_stmts s_orig s' (Some cond) bthen belse loc
- | Switch (e,b,c,l) ->
- let c' = List.filter (not $ (can_skip keep_stmts)) c in
- s'.skind <- Switch(e,b,c',l)
- | Block b ->
- let loc = Stmt.loc s' in
- (* must be performed after the optimisation
- of the block itself (see comment in vblock) *)
- Queue.add
- (fun () ->
- if b.bstmts = [] && b.battrs = [] then begin
- List.iter self#remove_local_static_attr b.bstatics;
- s'.skind <- (Instr (Skip loc))
- end)
- self#get_filling_actions
- | UnspecifiedSequence _ ->
- let loc = Stmt.loc s' in
- let visible_stmt =
- let info = self#get_finfo () in
- (fun s -> Info.inst_visible info !s)
- in
- Queue.add
- (fun () ->
- match s'.skind with
- | UnspecifiedSequence l ->
- let res =
- List.filter (fun (s,_,_,_,_) -> not (is_skip s.skind)) l
- in
- let res =
- List.map
- (fun (s,m,w,r,c) ->
- (s,
- List.filter (visible_lval local_visible) m,
- List.filter (visible_lval local_visible) w,
- List.filter (visible_lval local_visible) r,
- List.filter visible_stmt c
+ | If (cond,bthen,belse,loc) ->
+ let s_orig = Visitor_behavior.Get_orig.stmt self#behavior s' in
+ optim_if finfo keep_stmts s_orig s' (Some cond) bthen belse loc
+ | Switch (e,b,c,l) ->
+ let c' = List.filter (not $ (can_skip keep_stmts)) c in
+ s'.skind <- Switch(e,b,c',l)
+ | Block b ->
+ let loc = Stmt.loc s' in
+ (* must be performed after the optimisation
+ of the block itself (see comment in vblock) *)
+ Queue.add
+ (fun () ->
+ if b.bstmts = [] && b.battrs = [] then begin
+ List.iter self#remove_local_static_attr b.bstatics;
+ s'.skind <- (Instr (Skip loc))
+ end)
+ self#get_filling_actions
+ | UnspecifiedSequence _ ->
+ let loc = Stmt.loc s' in
+ let visible_stmt =
+ let info = self#get_finfo () in
+ (fun s -> Info.inst_visible info !s)
+ in
+ Queue.add
+ (fun () ->
+ match s'.skind with
+ | UnspecifiedSequence l ->
+ let res =
+ List.filter (fun (s,_,_,_,_) -> not (is_skip s.skind)) l
+ in
+ let res =
+ List.map
+ (fun (s,m,w,r,c) ->
+ (s,
+ List.filter (visible_lval local_visible) m,
+ List.filter (visible_lval local_visible) w,
+ List.filter (visible_lval local_visible) r,
+ List.filter visible_stmt c
+ )
)
- )
- res
- in
- (match res with
- [] -> s'.skind <- (Instr (Skip loc))
- | _ -> s'.skind <- UnspecifiedSequence res)
- | _ -> ())
- self#get_filling_actions
- | _ -> ());
+ res
+ in
+ (match res with
+ [] -> s'.skind <- (Instr (Skip loc))
+ | _ -> s'.skind <- UnspecifiedSequence res)
+ | _ -> ())
+ self#get_filling_actions
+ | _ -> ());
debug "@[<hov 10>[process_visible_stmt] gives sid:%d@ @[%a@]@]@."
s'.sid Printer.pp_stmt s';
s'
@@ -672,7 +672,7 @@ end = struct
| [] -> []
| l :: labs ->
let keep = Info.label_visible finfo s l || self#is_our_label l in
- debug "[filter_labels] %svisible %a@."
+ debug "[filter_labels] %svisible %a@."
(if keep then "" else "in") Printer.pp_label l;
if keep then l::(filter_labels labs) else filter_labels labs
in
@@ -708,7 +708,7 @@ end = struct
keep_stmts <- Stmt.Set.empty;
Varinfo.Hashtbl.clear local_visible;
Varinfo.Hashtbl.add spec_table f.svar
- (visitCilFunspec (self:>Cil.cilVisitor)
+ (visitCilFunspec (self:>Cil.cilVisitor)
(Annotations.funspec ~populate:false (Extlib.the self#current_kf)));
SkipChildren
@@ -740,29 +740,29 @@ end = struct
let ensure_visible (_,p) = Info.fun_postcond_visible finfo p.ip_content in
b.b_post_cond <-
filter_list ensure_visible (fun (k,p) -> k,self#visit_pred p)
- b.b_post_cond;
+ b.b_post_cond;
let allocates_visible a = Info.fun_allocates_visible finfo a in
let frees_visible a = Info.fun_frees_visible finfo a in
(match b.b_allocation with
- FreeAllocAny -> ()
- | FreeAlloc(f,a) ->
- try
- let frees = filter_list frees_visible self#visit_identified_term f in
- let allocates = filter_list allocates_visible self#visit_identified_term a in
- b.b_allocation <- FreeAlloc (frees, allocates)
- with Info.EraseAllocation -> b.b_allocation <- FreeAllocAny
+ FreeAllocAny -> ()
+ | FreeAlloc(f,a) ->
+ try
+ let frees = filter_list frees_visible self#visit_identified_term f in
+ let allocates = filter_list allocates_visible self#visit_identified_term a in
+ b.b_allocation <- FreeAlloc (frees, allocates)
+ with Info.EraseAllocation -> b.b_allocation <- FreeAllocAny
);
let from_visible a = Info.fun_assign_visible finfo a in
let from_visit a = visitCilFrom (self:>Cil.cilVisitor) a in
(match b.b_assigns with
- WritesAny -> ()
- | Writes l ->
- try
- let assigns = filter_list from_visible from_visit l in
- b.b_assigns <- Writes assigns
- with Info.EraseAssigns -> b.b_assigns <- WritesAny
+ WritesAny -> ()
+ | Writes l ->
+ try
+ let assigns = filter_list from_visible from_visit l in
+ b.b_assigns <- Writes assigns
+ with Info.EraseAssigns -> b.b_assigns <- WritesAny
);
SkipChildren (* see the warning on [SkipChildren] in [vspec] ! *)
@@ -779,7 +779,7 @@ end = struct
| Some (t,n) -> if Info.fun_variant_visible finfo t
then Some (visitCilTerm (self:>Cil.cilVisitor) t, n)
else None
- in
+ in
spec.spec_variant <- new_variant ;
let new_term = match spec.spec_terminates with
@@ -797,7 +797,7 @@ end = struct
has been visited above.
we need to put links to the appropriate copies of
variables (both pure C and logical ones)
- *)
+ *)
method private build_proto finfo loc =
let kf = Extlib.the self#current_kf in
@@ -805,70 +805,72 @@ end = struct
let new_var = ff_var fun_vars kf finfo in
(* we're building a prototype. *)
if not (Varinfo.Hashtbl.mem fi_table new_var) then begin
- new_var.vdefined <- false;
- let new_kf = make_new_kf my_kf kf new_var in
- Varinfo.Hashtbl.add fi_table new_var finfo;
- debug "@[[build_cil_proto] -> %s@\n@]@." new_var.vname;
- let action =
- let (rt,args,va,attrs) = Cil.splitFunctionType new_var.vtype in
- (match args with
- | None -> ()
- | Some args ->
- let old_formals = Kernel_function.get_formals kf in
- let old_formals = filter_params finfo old_formals in
- let args = filter_params finfo args in
- let mytype = TFun(rt,Some args,va,attrs) in
- let new_formals = List.map makeFormalsVarDecl args in
- self#add_formals_bindings new_var new_formals;
- Cil.update_var_type new_var mytype;
- List.iter2
- (fun x y ->
- Visitor_behavior.Set.varinfo self#behavior x y;
- Visitor_behavior.Set_orig.varinfo self#behavior y x;
- match x.vlogic_var_assoc with
- None -> ();
- | Some lv ->
- let lv' = Cil.cvar_to_lvar y in
- Visitor_behavior.Set.logic_var self#behavior lv lv';
- Visitor_behavior.Set_orig.logic_var self#behavior lv' lv)
- old_formals
- new_formals;
- (* adds the new parameters to the formals decl table *)
- Queue.add
- (fun () -> Cil.unsafeSetFormalsDecl new_var new_formals)
- self#get_filling_actions);
- let res =
- Cil.visitCilFunspec (self :> Cil.cilVisitor)
- (Annotations.funspec ~populate:false kf)
+ new_var.vdefined <- false;
+ let new_kf = make_new_kf my_kf kf new_var in
+ Varinfo.Hashtbl.add fi_table new_var finfo;
+ debug "@[[build_cil_proto] -> %s@\n@]@." new_var.vname;
+ let action =
+ let (rt,args,va,attrs) = Cil.splitFunctionType new_var.vtype in
+ (match args with
+ | None -> ()
+ | Some args ->
+ let old_formals = Kernel_function.get_formals kf in
+ let old_formals = filter_params finfo old_formals in
+ let args = filter_params finfo args in
+ let mytype = TFun(rt,Some args,va,attrs) in
+ let new_formals = List.map makeFormalsVarDecl args in
+ self#add_formals_bindings new_var new_formals;
+ Cil.update_var_type new_var mytype;
+ List.iter2
+ (fun x y ->
+ Visitor_behavior.Set.varinfo self#behavior x y;
+ Visitor_behavior.Set_orig.varinfo self#behavior y x;
+ match x.vlogic_var_assoc with
+ None -> ();
+ | Some lv ->
+ let lv' = Cil.cvar_to_lvar y in
+ Visitor_behavior.Set.logic_var self#behavior lv lv';
+ Visitor_behavior.Set_orig.logic_var self#behavior lv' lv)
+ old_formals
+ new_formals;
+ (* adds the new parameters to the formals decl table *)
+ Queue.add
+ (fun () -> Cil.unsafeSetFormalsDecl new_var new_formals)
+ self#get_filling_actions);
+ let res =
+ Cil.visitCilFunspec (self :> Cil.cilVisitor)
+ (Annotations.funspec ~populate:false kf)
+ in
+ let action () =
+ (* Replace the funspec copied by the default visitor, as
+ varinfo of formals would not be taken into account correctly
+ otherwise: everything would be mapped to the last set of
+ formals... *)
+ Queue.add
+ (fun () ->
+ new_kf.spec <- res;
+ Annotations.register_funspec ~force:true new_kf)
+ self#get_filling_actions
+ in
+ action
in
- let action () =
- (* Replace the funspec copied by the default visitor, as
- varinfo of formals would not be taken into account correctly
- otherwise: everything would be mapped to the last set of
- formals... *)
- Queue.add
- (fun () ->
- new_kf.spec <- res;
- Annotations.register_funspec ~force:true new_kf)
- self#get_filling_actions
- in
- action
- in
- let orig_var = Ast_info.Function.get_vi kf.fundec in
- (* The first copy is also the default one for varinfo that are not handled
- by ff_var but directly by the visitor *)
- if (Visitor_behavior.Get.varinfo self#behavior orig_var) == orig_var then
- Visitor_behavior.Set.varinfo self#behavior orig_var new_var;
- (* Set the new_var as an already known one, coming from the vi associated
- to the current kf.
- *)
- Visitor_behavior.Set.varinfo self#behavior new_var new_var;
- Visitor_behavior.Set_orig.varinfo self#behavior new_var orig_var;
- Visitor_behavior.Set.kernel_function self#behavior kf new_kf;
- Visitor_behavior.Set_orig.kernel_function self#behavior new_kf kf;
- Queue.add
- (fun () -> Globals.Functions.register new_kf) self#get_filling_actions;
- GFunDecl (Cil.empty_funspec(), new_var, loc), action
+ let orig_var = Ast_info.Function.get_vi kf.fundec in
+ (* The first copy is also the default one for varinfo that are not handled
+ by ff_var but directly by the visitor *)
+ if (Visitor_behavior.Get.varinfo self#behavior orig_var) == orig_var
+ then
+ Visitor_behavior.Set.varinfo self#behavior orig_var new_var;
+
+ (* Set the new_var as an already known one, coming from the vi associated
+ to the current kf.
+ *)
+ Visitor_behavior.Set.varinfo self#behavior new_var new_var;
+ Visitor_behavior.Set_orig.varinfo self#behavior new_var orig_var;
+ Visitor_behavior.Set.kernel_function self#behavior kf new_kf;
+ Visitor_behavior.Set_orig.kernel_function self#behavior new_kf kf;
+ Queue.add
+ (fun () -> Globals.Functions.register new_kf) self#get_filling_actions;
+ GFunDecl (Cil.empty_funspec(), new_var, loc), action
end else begin
let old_finfo = Varinfo.Hashtbl.find fi_table new_var in
if not (finfo = old_finfo) then
@@ -917,24 +919,24 @@ end = struct
let action () =
Queue.add
(fun () ->
- new_kf.spec <- Varinfo.Hashtbl.find spec_table new_fct_var;
- Annotations.register_funspec ~force:true new_kf)
+ new_kf.spec <- Varinfo.Hashtbl.find spec_table new_fct_var;
+ Annotations.register_funspec ~force:true new_kf)
self#get_filling_actions
in let f = Kernel_function.get_definition new_kf in
(* [JS 2009/03/23] do not call self#vfunc in the assertion;
otherwise does not work whenever frama-c is compiled with
-no-assert *)
- let res = self#vfunc f in
- assert (res = SkipChildren);
+ let res = self#vfunc f in
+ assert (res = SkipChildren);
(* if this ever changes, we must do some work. *)
- GFun (f,loc), action
+ GFun (f,loc), action
end
in
(match List.filter Info.body_visible finfo_list with
- | [ _ ] -> ()
- | [] | _ :: _ :: _ ->
- let vars = static_from_kf kf in
- List.iter self#remove_local_static_attr vars);
+ | [ _ ] -> ()
+ | [] | _ :: _ :: _ ->
+ let vars = static_from_kf kf in
+ List.iter self#remove_local_static_attr vars);
List.map do_f finfo_list
method! vglob_aux g =
diff --git a/src/kernel_services/ast_transformations/filter.mli b/src/kernel_services/ast_transformations/filter.mli
index dc0616c892e..e41f394b6ea 100644
--- a/src/kernel_services/ast_transformations/filter.mli
+++ b/src/kernel_services/ast_transformations/filter.mli
@@ -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
--
GitLab