diff --git a/.Makefile.lint b/.Makefile.lint
index c2648ca66aafcbf1311b68871dfb983d47a9fbd4..80fb691a8370490eea2a7db9b60c1fae64ab498a 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -52,7 +52,6 @@ ML_LINT_KO+=src/kernel_services/analysis/dataflow2.mli
ML_LINT_KO+=src/kernel_services/analysis/dataflows.ml
ML_LINT_KO+=src/kernel_services/analysis/dataflows.mli
ML_LINT_KO+=src/kernel_services/analysis/dominators.ml
-ML_LINT_KO+=src/kernel_services/analysis/exn_flow.ml
ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.ml
ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.mli
ML_LINT_KO+=src/kernel_services/analysis/logic_interp.ml
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index a75151352f640348731a343532d6cfa4da1a5646..f31a727c80275794f9265fc86312e1fd673e7dbf 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -23,20 +23,20 @@
open Cil
open Cil_types
-(* all exceptions that can be raised somewhere in the AST.
+(* all exceptions that can be raised somewhere in the AST.
Used to handle function pointers without exn specification
- *)
+*)
module All_exn =
State_builder.Option_ref(Cil_datatype.Typ.Set)
(struct let name = "Exn_flow.All_exn" let dependencies = [Ast.self] end)
-
+
module Exns =
State_builder.Hashtbl(Kernel_function.Hashtbl)(Cil_datatype.Typ.Set)
(struct
- let name = "Exn_flow.Exns"
- let dependencies = [Ast.self; All_exn.self]
- let size = 47
- end)
+ let name = "Exn_flow.Exns"
+ let dependencies = [Ast.self; All_exn.self]
+ let size = 47
+ end)
module ExnsStmt =
State_builder.Hashtbl(Cil_datatype.Stmt.Hashtbl)(Cil_datatype.Typ.Set)
@@ -61,10 +61,10 @@ class all_exn =
method get_exn = all_exn
method! vstmt_aux s =
match s.skind with
- | Throw (Some (_,t),_) ->
- all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
- SkipChildren
- | _ -> DoChildren
+ | Throw (Some (_,t),_) ->
+ all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
+ SkipChildren
+ | _ -> DoChildren
end
let compute_all_exn () =
@@ -82,41 +82,41 @@ let add_exn_var exns v =
let add_exn_clause exns (v,_) = add_exn_var exns v
(* We're not really interested by intra-procedural Dataflow here: all the
- interesting stuff happens at inter-procedural level (except for Throw
+ interesting stuff happens at inter-procedural level (except for Throw
encapsulated directly in a TryCatch, but even then it is easily captured
- at syntactical level). Therefore, we can as well use a syntactic pass
+ at syntactical level). Therefore, we can as well use a syntactic pass
at intra-procedural level
- *)
+*)
class exn_visit =
-object (self)
- inherit Visitor.frama_c_inplace
- val stack = Stack.create ()
- val possible_exn = Stack.create ()
- (* current set of exn included in a catch-all clause. Used to
- handle Throw None;
- *)
- val current_exn = Stack.create ()
-
- method private recursive_call kf =
- try
- Stack.iter
- (fun (kf',_) -> if Kernel_function.equal kf kf' then raise Exit) stack;
- false
- with Exit -> true
-
- method private add_exn t =
- let current_uncaught = Stack.top possible_exn in
- current_uncaught:= Cil_datatype.Typ.Set.add t !current_uncaught
-
- method private union_exn s =
- let current_uncaught = Stack.top possible_exn in
- current_uncaught := Cil_datatype.Typ.Set.union s !current_uncaught
-
- method! vstmt_aux s =
- match s.skind with
+ object (self)
+ inherit Visitor.frama_c_inplace
+ val stack = Stack.create ()
+ val possible_exn = Stack.create ()
+ (* current set of exn included in a catch-all clause. Used to
+ handle Throw None;
+ *)
+ val current_exn = Stack.create ()
+
+ method private recursive_call kf =
+ try
+ Stack.iter
+ (fun (kf',_) -> if Kernel_function.equal kf kf' then raise Exit) stack;
+ false
+ with Exit -> true
+
+ method private add_exn t =
+ let current_uncaught = Stack.top possible_exn in
+ current_uncaught:= Cil_datatype.Typ.Set.add t !current_uncaught
+
+ method private union_exn s =
+ let current_uncaught = Stack.top possible_exn in
+ current_uncaught := Cil_datatype.Typ.Set.union s !current_uncaught
+
+ method! vstmt_aux s =
+ match s.skind with
| Throw (None,_) ->
- let my_exn = Stack.top current_exn in
- self#union_exn my_exn; ExnsStmt.replace s my_exn; SkipChildren
+ let my_exn = Stack.top current_exn in
+ self#union_exn my_exn; ExnsStmt.replace s my_exn; SkipChildren
| Throw(Some (_,t),_) ->
let t = Cil.unrollTypeDeep t in
let t = Cil.type_remove_qualifier_attributes t in
@@ -127,14 +127,14 @@ object (self)
let catch, catch_all =
List.fold_left
(fun (catch, catch_all) ->
- function
- | (Catch_all,_) -> catch, true
- | (Catch_exn(v,[]),_) ->
- let catch = add_exn_var catch v in
- catch, catch_all
- | (Catch_exn(_,aux), _) ->
- let catch = List.fold_left add_exn_clause catch aux in
- catch, catch_all)
+ function
+ | (Catch_all,_) -> catch, true
+ | (Catch_exn(v,[]),_) ->
+ let catch = add_exn_var catch v in
+ catch, catch_all
+ | (Catch_exn(_,aux), _) ->
+ let catch = List.fold_left add_exn_clause catch aux in
+ catch, catch_all)
(Cil_datatype.Typ.Set.empty,false) c
in
Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
@@ -147,7 +147,7 @@ object (self)
if not catch_all then self#union_exn uncaught;
List.iter
(fun (v,b) ->
- (match v with
+ (match v with
| Catch_all ->
(* catch_all will catch all exceptions that are not
already handled by a previous clause. It must be the
@@ -164,9 +164,9 @@ object (self)
add_exn_clause Cil_datatype.Typ.Set.empty aux
in
Stack.push catch current_exn);
- ignore
- (Visitor.visitFramacBlock (self:>Visitor.frama_c_inplace) b);
- ignore (Stack.pop current_exn))
+ ignore
+ (Visitor.visitFramacBlock (self:>Visitor.frama_c_inplace) b);
+ ignore (Stack.pop current_exn))
c;
let my_exn = !(Stack.pop possible_exn) in
ExnsStmt.replace s my_exn;
@@ -175,34 +175,34 @@ object (self)
| If _ | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| TryFinally _ | TryExcept _
| Instr _ -> (* must take into account exceptions thrown by a fun call*)
- Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
- DoChildrenPost
- (fun s ->
+ Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
+ DoChildrenPost
+ (fun s ->
let my_exn = !(Stack.pop possible_exn) in
ExnsStmt.replace s my_exn;
self#union_exn my_exn;
s)
(* No exception can be thrown here. *)
| Return _ | Goto _ | Break _ | Continue _ ->
- ExnsStmt.replace s Cil_datatype.Typ.Set.empty;
- SkipChildren
+ ExnsStmt.replace s Cil_datatype.Typ.Set.empty;
+ SkipChildren
- method! vinst =
- function
+ method! vinst =
+ function
| Call(_,{ enode = Lval(Var f,NoOffset) },_,_)
| Local_init(_, ConsInit(f, _, _), _) ->
let kf = Globals.Functions.get f in
if self#recursive_call kf then begin
let module Found =
- struct
- exception F of Cil_datatype.Typ.Set.t
- end
+ struct
+ exception F of Cil_datatype.Typ.Set.t
+ end
in
let computed_exn =
try
Stack.iter
(fun (kf', exns) ->
- if Kernel_function.equal kf kf' then raise (Found.F !exns))
+ if Kernel_function.equal kf kf' then raise (Found.F !exns))
stack;
Kernel.fatal "No cycle found!"
with Found.F exns -> exns
@@ -220,7 +220,7 @@ object (self)
let kf_exn = Cil_datatype.Typ.Set.union computed_exn known_exn in
Exns.replace kf kf_exn;
ignore
- (Visitor.visitFramacFunction
+ (Visitor.visitFramacFunction
(self:>Visitor.frama_c_visitor)
(Kernel_function.get_definition kf));
let callee_exn = Exns.find kf in
@@ -236,9 +236,9 @@ object (self)
self#union_exn callee_exn
end else begin (* TODO: introduce extension to declare
exceptions that can be thrown by prototypes. *)
- Kernel.warning
- "Assuming declared function %a can't throw any exception"
- Kernel_function.pretty kf
+ Kernel.warning
+ "Assuming declared function %a can't throw any exception"
+ Kernel_function.pretty kf
end;
SkipChildren
| Call _ ->
@@ -247,60 +247,60 @@ object (self)
self#union_exn (all_exn()); SkipChildren
| _ -> SkipChildren
- method! vfunc f =
- let my_exns = ref Cil_datatype.Typ.Set.empty in
- let kf = Globals.Functions.get f.svar in
- Stack.push (kf,my_exns) stack;
- Stack.push my_exns possible_exn;
- let after_visit f =
- let callee_exn = Stack.pop possible_exn in
- Exns.add kf !callee_exn;
- ignore (Stack.pop stack); f
- in
- DoChildrenPost after_visit
+ method! vfunc f =
+ let my_exns = ref Cil_datatype.Typ.Set.empty in
+ let kf = Globals.Functions.get f.svar in
+ Stack.push (kf,my_exns) stack;
+ Stack.push my_exns possible_exn;
+ let after_visit f =
+ let callee_exn = Stack.pop possible_exn in
+ Exns.add kf !callee_exn;
+ ignore (Stack.pop stack); f
+ in
+ DoChildrenPost after_visit
-end
+ end
let compute_kf kf =
if Kernel_function.is_definition kf then
ignore
(Visitor.visitFramacFunction (new exn_visit)
(Kernel_function.get_definition kf))
- (* just ignore prototypes. *)
+(* just ignore prototypes. *)
let compute () = Globals.Functions.iter compute_kf
let get_type_tag t =
let rec aux t =
match t with
- | TVoid _ -> "v"
- | TInt (IBool,_) -> "B"
- | TInt (IChar,_) -> "c"
- | TInt (ISChar,_) -> "sc"
- | TInt (IUChar,_) -> "uc"
- | TInt (IInt,_) -> "i"
- | TInt (IUInt,_) -> "ui"
- | TInt (IShort,_) -> "s"
- | TInt (IUShort,_) -> "us"
- | TInt (ILong,_) -> "l"
- | TInt (IULong,_) -> "ul"
- | TInt (ILongLong,_) -> "ll"
- | TInt (IULongLong,_) -> "ull"
- | TFloat(FFloat,_) -> "f"
- | TFloat(FDouble,_) -> "d"
- | TFloat (FLongDouble,_) -> "ld"
- | TPtr(t,_) -> "p" ^ aux t
- | TArray(t,_,_,_) -> "a" ^ aux t
- | TFun(rt,l,_,_) ->
- let base = "fun" ^ aux rt in
- (match l with
- | None -> base
- | Some l ->
- List.fold_left (fun acc (_,t,_) -> acc ^ aux t) base l)
- | TNamed _ -> Kernel.fatal "named type not correctly unrolled"
- | TComp (s,_,_) -> (if s.cstruct then "S" else "U") ^ s.cname
- | TEnum (e,_) -> "E" ^ e.ename
- | TBuiltin_va_list _ -> "va"
+ | TVoid _ -> "v"
+ | TInt (IBool,_) -> "B"
+ | TInt (IChar,_) -> "c"
+ | TInt (ISChar,_) -> "sc"
+ | TInt (IUChar,_) -> "uc"
+ | TInt (IInt,_) -> "i"
+ | TInt (IUInt,_) -> "ui"
+ | TInt (IShort,_) -> "s"
+ | TInt (IUShort,_) -> "us"
+ | TInt (ILong,_) -> "l"
+ | TInt (IULong,_) -> "ul"
+ | TInt (ILongLong,_) -> "ll"
+ | TInt (IULongLong,_) -> "ull"
+ | TFloat(FFloat,_) -> "f"
+ | TFloat(FDouble,_) -> "d"
+ | TFloat (FLongDouble,_) -> "ld"
+ | TPtr(t,_) -> "p" ^ aux t
+ | TArray(t,_,_,_) -> "a" ^ aux t
+ | TFun(rt,l,_,_) ->
+ let base = "fun" ^ aux rt in
+ (match l with
+ | None -> base
+ | Some l ->
+ List.fold_left (fun acc (_,t,_) -> acc ^ aux t) base l)
+ | TNamed _ -> Kernel.fatal "named type not correctly unrolled"
+ | TComp (s,_,_) -> (if s.cstruct then "S" else "U") ^ s.cname
+ | TEnum (e,_) -> "E" ^ e.ename
+ | TBuiltin_va_list _ -> "va"
in "__fc_" ^ aux t
let get_type_enum t = "__fc_exn_kind_" ^ (get_type_tag t)
@@ -372,9 +372,9 @@ let generate_exn_union e exns =
let add_types_and_globals typs globs f =
let iter_globs (acc,added) g =
match g with
- | GVarDecl _ | GVar _ | GFun _ as g when not added ->
- (g :: List.rev_append globs (List.rev_append typs acc), true)
- | _ -> g :: acc, added
+ | GVarDecl _ | GVar _ | GFun _ as g when not added ->
+ (g :: List.rev_append globs (List.rev_append typs acc), true)
+ | _ -> g :: acc, added
in
let globs, added = List.fold_left iter_globs ([],false) f.globals in
let globs =
@@ -399,130 +399,130 @@ let find_exns_func v =
let find_exns e =
match e.enode with
- | Lval(Var v, NoOffset) -> find_exns_func v
- | _ -> all_exn ()
+ | Lval(Var v, NoOffset) -> find_exns_func v
+ | _ -> all_exn ()
class erase_exn =
-object(self)
- inherit Visitor.frama_c_inplace
- (* reverse before filling. *)
- val mutable new_types = []
-
- val exn_enum = Cil_datatype.Typ.Hashtbl.create 7
+ object(self)
+ inherit Visitor.frama_c_inplace
+ (* reverse before filling. *)
+ val mutable new_types = []
- val exn_union = Cil_datatype.Typ.Hashtbl.create 7
+ val exn_enum = Cil_datatype.Typ.Hashtbl.create 7
- val mutable modified_funcs = Cil_datatype.Fundec.Set.empty
+ val exn_union = Cil_datatype.Typ.Hashtbl.create 7
- val mutable exn_struct = None
+ val mutable modified_funcs = Cil_datatype.Fundec.Set.empty
- val mutable exn_var = None
+ val mutable exn_struct = None
- val mutable can_throw = false
+ val mutable exn_var = None
- val mutable fct_can_throw = false
+ val mutable can_throw = false
- val mutable catched_var = None
+ val mutable fct_can_throw = false
- val mutable label_counter = 0
+ val mutable catched_var = None
- val exn_labels = Cil_datatype.Typ.Hashtbl.create 7
- val catch_all_label = Stack.create ()
+ val mutable label_counter = 0
- method modified_funcs = modified_funcs
+ val exn_labels = Cil_datatype.Typ.Hashtbl.create 7
+ val catch_all_label = Stack.create ()
- method private update_enum_bindings enum exns =
- let update_one_binding t =
- let s = get_type_enum t in
- let ei = List.find (fun ei -> ei.einame = s) enum.eitems in
- Cil_datatype.Typ.Hashtbl.add exn_enum t ei
- in
- Cil_datatype.Typ.Set.iter update_one_binding exns
+ method modified_funcs = modified_funcs
- method private update_union_bindings union exns =
- let update_one_binding t =
- let s = get_type_tag t in
- Kernel.debug ~dkey:Kernel.dkey_exn_flow
- "Registering %a as possible exn type" Cil_datatype.Typ.pretty t;
- let fi = List.find (fun fi -> fi.fname = s) union.cfields in
- Cil_datatype.Typ.Hashtbl.add exn_union t fi
- in
- Cil_datatype.Typ.Set.iter update_one_binding exns
-
- method private exn_kind t = Cil_datatype.Typ.Hashtbl.find exn_enum t
-
- method private is_thrown t = Cil_datatype.Typ.Hashtbl.mem exn_enum t
+ method private update_enum_bindings enum exns =
+ let update_one_binding t =
+ let s = get_type_enum t in
+ let ei = List.find (fun ei -> ei.einame = s) enum.eitems in
+ Cil_datatype.Typ.Hashtbl.add exn_enum t ei
+ in
+ Cil_datatype.Typ.Set.iter update_one_binding exns
+
+ method private update_union_bindings union exns =
+ let update_one_binding t =
+ let s = get_type_tag t in
+ Kernel.debug ~dkey:Kernel.dkey_exn_flow
+ "Registering %a as possible exn type" Cil_datatype.Typ.pretty t;
+ let fi = List.find (fun fi -> fi.fname = s) union.cfields in
+ Cil_datatype.Typ.Hashtbl.add exn_union t fi
+ in
+ Cil_datatype.Typ.Set.iter update_one_binding exns
- method private exn_field_off name =
- List.find (fun fi -> fi.fname = name) (Extlib.the exn_struct).cfields
+ method private exn_kind t = Cil_datatype.Typ.Hashtbl.find exn_enum t
- method private exn_field name =
- Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)
+ method private is_thrown t = Cil_datatype.Typ.Hashtbl.mem exn_enum t
- method private exn_field_term name =
- TVar(Cil.cvar_to_lvar (Extlib.the exn_var)),
- TField(self#exn_field_off name, TNoOffset)
+ method private exn_field_off name =
+ List.find (fun fi -> fi.fname = name) (Extlib.the exn_struct).cfields
- method private exn_obj_field = self#exn_field exn_obj_name
+ method private exn_field name =
+ Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)
- method private exn_obj_field_term = self#exn_field_term exn_obj_name
+ method private exn_field_term name =
+ TVar(Cil.cvar_to_lvar (Extlib.the exn_var)),
+ TField(self#exn_field_off name, TNoOffset)
- method private exn_kind_field = self#exn_field exn_kind_name
+ method private exn_obj_field = self#exn_field exn_obj_name
- method private exn_kind_field_term = self#exn_field_term exn_kind_name
+ method private exn_obj_field_term = self#exn_field_term exn_obj_name
- method private uncaught_flag_field = self#exn_field exn_uncaught_name
+ method private exn_kind_field = self#exn_field exn_kind_name
- method private uncaught_flag_field_term =
- self#exn_field_term exn_uncaught_name
+ method private exn_kind_field_term = self#exn_field_term exn_kind_name
- method private exn_obj_kind_field t =
- Kernel.debug ~dkey:Kernel.dkey_exn_flow
- "Searching for %a as possible exn type" Cil_datatype.Typ.pretty t;
- Cil_datatype.Typ.Hashtbl.find exn_union t
+ method private uncaught_flag_field = self#exn_field exn_uncaught_name
- method private test_uncaught_flag loc b =
- let e1 = Cil.new_exp ~loc (Lval self#uncaught_flag_field) in
- let e2 = if b then Cil.one ~loc else Cil.zero ~loc in
- Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil.intType))
+ method private uncaught_flag_field_term =
+ self#exn_field_term exn_uncaught_name
- method private pred_uncaught_flag loc b =
- let e1 =
- Logic_const.term
- ~loc (TLval self#uncaught_flag_field_term) Linteger
- in
- let e2 =
- if b then Logic_const.tinteger ~loc 1
- else Logic_const.tinteger ~loc 0
- in
- Logic_const.prel ~loc (Req,e1,e2)
-
- method private set_uncaught_flag loc b =
- let e = if b then Cil.one ~loc else Cil.zero ~loc in
- Cil.mkStmtOneInstr (Set(self#uncaught_flag_field,e,loc))
-
- method private set_exn_kind loc t =
- let e = self#exn_kind (purify t) in
- let e = Cil.new_exp ~loc (Const (CEnum e)) in
- Cil.mkStmtOneInstr(Set(self#exn_kind_field,e,loc))
-
- method private set_exn_value loc t e =
- let lv = self#exn_obj_field in
- let union_field = self#exn_obj_kind_field (purify t) in
- let lv = Cil.addOffsetLval (Field (union_field, NoOffset)) lv in
- Cil.mkStmtOneInstr (Set(lv,e,loc))
-
- method private jumps_to_default_handler loc =
- if Stack.is_empty catch_all_label then begin
- (* no catch-all clause in the function: just go up in the stack. *)
- fct_can_throw <- true;
- let kf = Extlib.the self#current_kf in
- let ret = Kernel_function.find_return kf in
- let rtyp = Kernel_function.get_return_type kf in
- if ret.labels = [] then
- ret.labels <- [Label("__ret_label",Cil_datatype.Stmt.loc ret,false)];
- let goto = mkStmt (Goto (ref ret,loc)) in
- match ret.skind with
+ method private exn_obj_kind_field t =
+ Kernel.debug ~dkey:Kernel.dkey_exn_flow
+ "Searching for %a as possible exn type" Cil_datatype.Typ.pretty t;
+ Cil_datatype.Typ.Hashtbl.find exn_union t
+
+ method private test_uncaught_flag loc b =
+ let e1 = Cil.new_exp ~loc (Lval self#uncaught_flag_field) in
+ let e2 = if b then Cil.one ~loc else Cil.zero ~loc in
+ Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil.intType))
+
+ method private pred_uncaught_flag loc b =
+ let e1 =
+ Logic_const.term
+ ~loc (TLval self#uncaught_flag_field_term) Linteger
+ in
+ let e2 =
+ if b then Logic_const.tinteger ~loc 1
+ else Logic_const.tinteger ~loc 0
+ in
+ Logic_const.prel ~loc (Req,e1,e2)
+
+ method private set_uncaught_flag loc b =
+ let e = if b then Cil.one ~loc else Cil.zero ~loc in
+ Cil.mkStmtOneInstr (Set(self#uncaught_flag_field,e,loc))
+
+ method private set_exn_kind loc t =
+ let e = self#exn_kind (purify t) in
+ let e = Cil.new_exp ~loc (Const (CEnum e)) in
+ Cil.mkStmtOneInstr(Set(self#exn_kind_field,e,loc))
+
+ method private set_exn_value loc t e =
+ let lv = self#exn_obj_field in
+ let union_field = self#exn_obj_kind_field (purify t) in
+ let lv = Cil.addOffsetLval (Field (union_field, NoOffset)) lv in
+ Cil.mkStmtOneInstr (Set(lv,e,loc))
+
+ method private jumps_to_default_handler loc =
+ if Stack.is_empty catch_all_label then begin
+ (* no catch-all clause in the function: just go up in the stack. *)
+ fct_can_throw <- true;
+ let kf = Extlib.the self#current_kf in
+ let ret = Kernel_function.find_return kf in
+ let rtyp = Kernel_function.get_return_type kf in
+ if ret.labels = [] then
+ ret.labels <- [Label("__ret_label",Cil_datatype.Stmt.loc ret,false)];
+ let goto = mkStmt (Goto (ref ret,loc)) in
+ match ret.skind with
| Return (None,_) -> [goto]
(* rt is void: do not need to create a dummy return value *)
| Return (Some { enode = Lval(Var rv, NoOffset) },_) ->
@@ -532,232 +532,232 @@ object(self)
Kernel.fatal "exception removal should be used after oneRet"
| _ ->
Kernel.fatal "find_return did not give a Return statement"
- end else begin
- let stmt = Stack.top catch_all_label in
- [mkStmt (Goto (ref stmt, loc))]
- end
-
- method private jumps_to_handler loc t =
- let t = purify t in
- try
- let stmt = Cil_datatype.Typ.Hashtbl.find exn_labels t in
- [mkStmt (Goto (ref stmt, loc))]
- with
+ end else begin
+ let stmt = Stack.top catch_all_label in
+ [mkStmt (Goto (ref stmt, loc))]
+ end
+
+ method private jumps_to_handler loc t =
+ let t = purify t in
+ try
+ let stmt = Cil_datatype.Typ.Hashtbl.find exn_labels t in
+ [mkStmt (Goto (ref stmt, loc))]
+ with
| Not_found -> self#jumps_to_default_handler loc
- method! vfile f =
- let exns = all_exn () in
- if not (Cil_datatype.Typ.Set.is_empty exns) then begin
- let loc = Cil_datatype.Location.unknown in
- let e = generate_exn_enum exns in
- let u,s = generate_exn_union e exns in
- let exn =
- Cil.makeGlobalVar "__fc_exn" (TComp (s,{scache = Not_Computed},[]))
- in
- self#update_enum_bindings e exns;
- self#update_union_bindings u exns;
- exn_struct <- Some s;
- can_throw <- true;
- new_types <-
- GCompTag (s,loc) ::
- GCompTag (u,loc) ::
- GEnumTag (e,loc) :: new_types;
- exn_var <- Some exn;
- let exn_init = Cil.makeZeroInit ~loc (TComp(s,{scache=Not_Computed},[]))
- in
- let gexn_var = GVar(exn, { init = Some exn_init }, loc) in
- ChangeDoChildrenPost(
- f,add_types_and_globals (List.rev new_types) [gexn_var])
- end else (* nothing can be thrown in the first place, but we still have
- to get rid of (useless) try/catch blocks if any. *)
+ method! vfile f =
+ let exns = all_exn () in
+ if not (Cil_datatype.Typ.Set.is_empty exns) then begin
+ let loc = Cil_datatype.Location.unknown in
+ let e = generate_exn_enum exns in
+ let u,s = generate_exn_union e exns in
+ let exn =
+ Cil.makeGlobalVar "__fc_exn" (TComp (s,{scache = Not_Computed},[]))
+ in
+ self#update_enum_bindings e exns;
+ self#update_union_bindings u exns;
+ exn_struct <- Some s;
+ can_throw <- true;
+ new_types <-
+ GCompTag (s,loc) ::
+ GCompTag (u,loc) ::
+ GEnumTag (e,loc) :: new_types;
+ exn_var <- Some exn;
+ let exn_init = Cil.makeZeroInit ~loc (TComp(s,{scache=Not_Computed},[]))
+ in
+ let gexn_var = GVar(exn, { init = Some exn_init }, loc) in
+ ChangeDoChildrenPost(
+ f,add_types_and_globals (List.rev new_types) [gexn_var])
+ end else (* nothing can be thrown in the first place, but we still have
+ to get rid of (useless) try/catch blocks if any. *)
DoChildren
- method private visit_catch_clause loc (v,b) =
- let loc =
- match b.bstmts with
+ method private visit_catch_clause loc (v,b) =
+ let loc =
+ match b.bstmts with
| [] -> loc
| [x] -> Cil_datatype.Stmt.loc x
| x::tl ->
fst (Cil_datatype.Stmt.loc x),
snd (Cil_datatype.Stmt.loc (Extlib.last tl))
- in
- let add_unreachable_block b =
- Cil.mkStmt (If(Cil.zero ~loc, b, Cil.mkBlock [], loc))
- in
- let assign_catched_obj v b =
- let exn_obj = self#exn_obj_field in
- let kind_field = self#exn_obj_kind_field (purify v.vtype) in
- let lv = Cil.addOffsetLval (Field (kind_field,NoOffset)) exn_obj in
- let s =
- Cil.mkStmtOneInstr
- (Set ((Var v, NoOffset), Cil.new_exp ~loc (Lval lv), loc))
in
- b.bstmts <- s :: b.bstmts
- in
- let f = Extlib.the self#current_func in
- let update_locals v b =
- if not (List.memq v b.blocals) then b.blocals <- v::b.blocals;
- if not (List.memq v f.slocals) then f.slocals <- v::f.slocals
- in
- let b =
- (match v with
- | Catch_all -> b
- | Catch_exn (v,[]) ->
- 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) =
- Cil.update_var_type v (purify v.vtype);
- update_locals v b;
- assign_catched_obj v b;
- add_unreachable_block b :: stmts
- in
- b.blocals <- List.filter (fun v' -> v!=v') b.blocals;
- let aux_blocks =
- List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
- in
- let main_block = Cil.mkBlock aux_blocks in
- Cil.update_var_type v (purify v.vtype);
- update_locals v main_block;
- main_block)
- in
- ignore (Visitor.visitFramacBlock (self :> Visitor.frama_c_visitor) b);
- add_unreachable_block b
-
- method! vfunc _ =
- label_counter <- 0;
- fct_can_throw <- false;
- let update_body f =
- if fct_can_throw then begin
- Oneret.encapsulate_local_vars f
- end;
- f
- in
- DoChildrenPost update_body
+ let add_unreachable_block b =
+ Cil.mkStmt (If(Cil.zero ~loc, b, Cil.mkBlock [], loc))
+ in
+ let assign_catched_obj v b =
+ let exn_obj = self#exn_obj_field in
+ let kind_field = self#exn_obj_kind_field (purify v.vtype) in
+ let lv = Cil.addOffsetLval (Field (kind_field,NoOffset)) exn_obj in
+ let s =
+ Cil.mkStmtOneInstr
+ (Set ((Var v, NoOffset), Cil.new_exp ~loc (Lval lv), loc))
+ in
+ b.bstmts <- s :: b.bstmts
+ in
+ let f = Extlib.the self#current_func in
+ let update_locals v b =
+ if not (List.memq v b.blocals) then b.blocals <- v::b.blocals;
+ if not (List.memq v f.slocals) then f.slocals <- v::f.slocals
+ in
+ let b =
+ (match v with
+ | Catch_all -> b
+ | Catch_exn (v,[]) ->
+ 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) =
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v b;
+ assign_catched_obj v b;
+ add_unreachable_block b :: stmts
+ in
+ b.blocals <- List.filter (fun v' -> v!=v') b.blocals;
+ let aux_blocks =
+ List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
+ in
+ let main_block = Cil.mkBlock aux_blocks in
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v main_block;
+ main_block)
+ in
+ ignore (Visitor.visitFramacBlock (self :> Visitor.frama_c_visitor) b);
+ add_unreachable_block b
+
+ method! vfunc _ =
+ label_counter <- 0;
+ fct_can_throw <- false;
+ let update_body f =
+ if fct_can_throw then begin
+ Oneret.encapsulate_local_vars f
+ end;
+ f
+ in
+ DoChildrenPost update_body
- method private modify_current () =
- modified_funcs <-
- Cil_datatype.Fundec.Set.add (Extlib.the self#current_func) modified_funcs;
+ method private modify_current () =
+ modified_funcs <-
+ Cil_datatype.Fundec.Set.add (Extlib.the self#current_func) modified_funcs;
- method private aux_handler_goto target (v,b) =
- let loc = v.vdecl in
- let goto_main_handler = Cil.mkStmt (Goto (ref target,loc)) in
- let suf =
- if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
- in
- let lab = (get_type_tag (purify v.vtype)) ^ suf in
- label_counter <- label_counter + 1;
- b.bstmts <- b.bstmts @ [goto_main_handler];
- (* we have at least the goto statement in the block *)
- let s = List.hd b.bstmts in
- s.labels <- (Label(lab,loc,false)::s.labels);
- Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) s
-
- method private guard_post_cond (kind,pred as orig) =
- match kind with
- (* If we exit explicitly with exit,
- we haven't seen an uncaught exception anyway. *)
+ method private aux_handler_goto target (v,b) =
+ let loc = v.vdecl in
+ let goto_main_handler = Cil.mkStmt (Goto (ref target,loc)) in
+ let suf =
+ if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
+ in
+ let lab = (get_type_tag (purify v.vtype)) ^ suf in
+ label_counter <- label_counter + 1;
+ b.bstmts <- b.bstmts @ [goto_main_handler];
+ (* we have at least the goto statement in the block *)
+ let s = List.hd b.bstmts in
+ s.labels <- (Label(lab,loc,false)::s.labels);
+ Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) s
+
+ method private guard_post_cond (kind,pred as orig) =
+ match kind with
+ (* If we exit explicitly with exit,
+ we haven't seen an uncaught exception anyway. *)
| Exits | Breaks | Continues -> orig
| Returns | Normal ->
- let loc = pred.ip_content.pred_loc in
- let p = self#pred_uncaught_flag loc false in
- let pred' = Logic_const.pred_of_id_pred pred in
- (kind,
- (Logic_const.new_predicate
- (Logic_const.pimplies ~loc (p,pred'))))
-
- method! vbehavior b =
- match self#current_kf, self#current_stmt with
+ let loc = pred.ip_content.pred_loc in
+ let p = self#pred_uncaught_flag loc false in
+ let pred' = Logic_const.pred_of_id_pred pred in
+ (kind,
+ (Logic_const.new_predicate
+ (Logic_const.pimplies ~loc (p,pred'))))
+
+ method! vbehavior b =
+ match self#current_kf, self#current_stmt with
| None, None -> SkipChildren
- (* Prototype is assumed to not throw any exception. *)
+ (* Prototype is assumed to not throw any exception. *)
| None, Some _ ->
- Kernel.fatal
- "Inconsistent visitor state: visiting a statement \
- outside of any function."
- | Some f, None when not (Kernel_function.is_definition f) ->
- (* By hypothesis, prototypes do not throw anything. *)
- SkipChildren
+ Kernel.fatal
+ "Inconsistent visitor state: visiting a statement \
+ outside of any function."
+ | Some f, None when not (Kernel_function.is_definition f) ->
+ (* By hypothesis, prototypes do not throw anything. *)
+ SkipChildren
| Some f, None -> (* function contract *)
- let exns = Exns.find f in
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
- ChangeTo b (* need to register the new clauses. *)
- end
+ let exns = Exns.find f in
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
+ ChangeTo b (* need to register the new clauses. *)
+ end
| Some _, Some s -> (* statement contract *)
- let exns = ExnsStmt.find s in
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
- ChangeTo b
- end
-
- method private clean_catch_clause (bind,b as handler) acc =
- let remove_local v =
- let f =
- Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
- in
- let v = Visitor_behavior.Get.varinfo self#behavior v in
- f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
- in
- match bind with
- | Catch_all -> handler :: acc
- | Catch_exn (v, []) ->
- if self#is_thrown (purify v.vtype) then handler :: acc
- else begin remove_local v; acc end
- | Catch_exn (v, l) ->
- let caught, remove =
- List.partition (fun (v,_) -> self#is_thrown (purify v.vtype)) l
- in
- List.iter (fun (v,_) -> remove_local v) remove;
- if caught = [] then begin remove_local v; acc end
- else (Catch_exn (v,caught), b) :: acc
-
- method! vstmt_aux s =
- let generate_jumps instr exns loc =
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- self#modify_current ();
- let make_jump t (stmts, uncaught) =
- let t = purify t in
- if Cil_datatype.Typ.Hashtbl.mem exn_labels t then begin
- let e = self#exn_kind t in
- let e = Cil.new_exp ~loc (Const (CEnum e)) in
- let b = self#jumps_to_handler loc t in
- let s = Cil.mkStmt (Block (Cil.mkBlock b)) in
- s.labels <- [Case (e,loc)];
- s::stmts, uncaught
- end else stmts, true
+ let exns = ExnsStmt.find s in
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
+ ChangeTo b
+ end
+
+ method private clean_catch_clause (bind,b as handler) acc =
+ let remove_local v =
+ let f =
+ Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
in
- let stmts, uncaught =
- Cil_datatype.Typ.Set.fold make_jump exns ([],false)
+ let v = Visitor_behavior.Get.varinfo self#behavior v in
+ f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
+ in
+ match bind with
+ | Catch_all -> handler :: acc
+ | Catch_exn (v, []) ->
+ if self#is_thrown (purify v.vtype) then handler :: acc
+ else begin remove_local v; acc end
+ | Catch_exn (v, l) ->
+ let caught, remove =
+ List.partition (fun (v,_) -> self#is_thrown (purify v.vtype)) l
in
- let stmts =
- if uncaught then begin
- let default =
+ List.iter (fun (v,_) -> remove_local v) remove;
+ if caught = [] then begin remove_local v; acc end
+ else (Catch_exn (v,caught), b) :: acc
+
+ method! vstmt_aux s =
+ let generate_jumps instr exns loc =
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ self#modify_current ();
+ let make_jump t (stmts, uncaught) =
+ let t = purify t in
+ if Cil_datatype.Typ.Hashtbl.mem exn_labels t then begin
+ let e = self#exn_kind t in
+ let e = Cil.new_exp ~loc (Const (CEnum e)) in
+ let b = self#jumps_to_handler loc t in
+ let s = Cil.mkStmt (Block (Cil.mkBlock b)) in
+ s.labels <- [Case (e,loc)];
+ s::stmts, uncaught
+ end else stmts, true
+ in
+ let stmts, uncaught =
+ Cil_datatype.Typ.Set.fold make_jump exns ([],false)
+ in
+ let stmts =
+ if uncaught then begin
+ let default =
Cil.mkStmt (
Block (Cil.mkBlock (self#jumps_to_default_handler loc)))
- in
- default.labels <- [Default loc];
- List.rev_append stmts [default]
- end else List.rev stmts
- in
- let test = self#test_uncaught_flag loc true in
- let cases = Cil.new_exp ~loc (Lval self#exn_kind_field) in
- let switch = Cil.mkStmt (Switch(cases,Cil.mkBlock stmts,stmts,loc)) in
- let handler =
- Cil.mkStmt (If(test,Cil.mkBlock [switch],Cil.mkBlock [],loc))
- in
- let instr =
- Visitor.visitFramacInstr (self:>Visitor.frama_c_visitor) instr
- in
- let call = Cil.mkStmtOneInstr (List.hd instr) in
- s.skind <- Block (Cil.mkBlockNonScoping [call;handler]);
- SkipChildren
- end
- in
- match s.skind with
+ in
+ default.labels <- [Default loc];
+ List.rev_append stmts [default]
+ end else List.rev stmts
+ in
+ let test = self#test_uncaught_flag loc true in
+ let cases = Cil.new_exp ~loc (Lval self#exn_kind_field) in
+ let switch = Cil.mkStmt (Switch(cases,Cil.mkBlock stmts,stmts,loc)) in
+ let handler =
+ Cil.mkStmt (If(test,Cil.mkBlock [switch],Cil.mkBlock [],loc))
+ in
+ let instr =
+ Visitor.visitFramacInstr (self:>Visitor.frama_c_visitor) instr
+ in
+ let call = Cil.mkStmtOneInstr (List.hd instr) in
+ s.skind <- Block (Cil.mkBlockNonScoping [call;handler]);
+ SkipChildren
+ end
+ in
+ match s.skind with
| Instr (Call (_,f,_,loc) as instr) ->
generate_jumps instr (find_exns f) loc
| Instr (Local_init(_, ConsInit(f,_,_), loc) as instr) ->
@@ -795,7 +795,7 @@ object(self)
than the current block. As we are adding statements in the
auxiliary blocks, we need to do that before adding labels to the
entry points of these blocks.
- *)
+ *)
let stmts = List.map (self#visit_catch_clause loc) c in
let suf =
if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
@@ -812,10 +812,10 @@ object(self)
stmt.labels <- [Label (label,v.vdecl,false)];
b.bstmts <- stmt :: b.bstmts;
(match aux with
- | [] ->
- Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) stmt
- | _ :: _ ->
- List.iter (self#aux_handler_goto stmt) aux)
+ | [] ->
+ Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) stmt
+ | _ :: _ ->
+ List.iter (self#aux_handler_goto stmt) aux)
| (Catch_all, b) ->
let loc =
match b.bstmts with [] -> loc | s::_ -> Cil_datatype.Stmt.loc s
@@ -837,7 +837,7 @@ object(self)
| Catch_exn(_,l), _ ->
List.iter
(fun (v,_) ->
- Cil_datatype.Typ.Hashtbl.remove exn_labels (purify v.vtype))
+ Cil_datatype.Typ.Hashtbl.remove exn_labels (purify v.vtype))
l
| Catch_all,_ -> ignore (Stack.pop catch_all_label))
c; (* we remove bindings in the reverse order as we added them,
@@ -846,8 +846,8 @@ object(self)
s.skind <- Block t;
SkipChildren
| _ -> DoChildren
-
-end
+
+ end
let prepare_file f =
if Kernel.SimplifyCfg.get () then begin