exn_flow.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2020                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil
open Cil_types

(* 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)

module ExnsStmt =
  State_builder.Hashtbl(Cil_datatype.Stmt.Hashtbl)(Cil_datatype.Typ.Set)
    (struct
      let name = "Exn_flow.ExnsStmt"
      let dependencies = [Ast.self; All_exn.self]
      let size = 53
    end)

let self_fun = Exns.self

let self_stmt = ExnsStmt.self

let purify t =
  let t = Cil.unrollTypeDeep t in
  Cil.type_remove_qualifier_attributes_deep t

class all_exn =
  object
    inherit Visitor.frama_c_inplace
    val mutable all_exn = Cil_datatype.Typ.Set.empty
    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
  end

let compute_all_exn () =
  let vis = new all_exn in
  Visitor.visitFramacFileSameGlobals (vis:>Visitor.frama_c_visitor) (Ast.get());
  vis#get_exn

let all_exn () = All_exn.memo compute_all_exn

let add_exn_var exns v =
  let t = Cil.unrollTypeDeep v.vtype in
  let t = Cil.type_remove_qualifier_attributes t in
  Cil_datatype.Typ.Set.add t exns

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 
   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 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
      | Throw (None,_) ->
          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
        self#add_exn t;
        ExnsStmt.replace s (Cil_datatype.Typ.Set.singleton t);
        SkipChildren
      | TryCatch (t,c,_) ->
        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)
            (Cil_datatype.Typ.Set.empty,false) c
        in
        Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
        ignore (Visitor.visitFramacBlock (self:>Visitor.frama_c_inplace) t);
        let my_exn = Stack.pop possible_exn in
        let uncaught = Cil_datatype.Typ.Set.diff !my_exn catch in
        (* uncaught exceptions are lift to previous set of exn, but
           only if there's no catch-all clause. *)
        Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
        if not catch_all then self#union_exn uncaught;
        List.iter
          (fun (v,b) ->
             (match v with 
              | Catch_all ->
                (* catch_all will catch all exceptions that are not
                   already handled by a previous clause. It must be the
                   last handler (C++11, 15.3§5), thus there's no handler
                   ordering issue
                *)
                Stack.push uncaught current_exn
              | Catch_exn (v,[]) ->
                let catch = add_exn_var Cil_datatype.Typ.Set.empty v in
                Stack.push catch current_exn
              | Catch_exn (_,aux) ->
                let catch =
                  List.fold_left
                    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))
          c;
        let my_exn = !(Stack.pop possible_exn) in
        ExnsStmt.replace s my_exn;
        self#union_exn my_exn;
        SkipChildren
      | 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 ->
             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

  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
          in
          let computed_exn =
            try
              Stack.iter
                (fun (kf', exns) ->
                  if Kernel_function.equal kf kf' then raise (Found.F !exns))
                stack;
              Kernel.fatal "No cycle found!"
            with Found.F exns -> exns
          in
          let known_exn =
            try Exns.find kf with Not_found -> Cil_datatype.Typ.Set.empty
          in
          if Cil_datatype.Typ.Set.subset computed_exn known_exn then begin
            (* Fixpoint found, no need to recurse. *)
            self#union_exn known_exn
          end else begin
            (* add known exns in table and recurse. Termination is ensured
               by the fact that only a finite number of exceptions
               can be thrown. *)
            let kf_exn = Cil_datatype.Typ.Set.union computed_exn known_exn in
            Exns.replace kf kf_exn;
            ignore
              (Visitor.visitFramacFunction 
                 (self:>Visitor.frama_c_visitor)
                 (Kernel_function.get_definition kf));
            let callee_exn = Exns.find kf in
            self#union_exn callee_exn
          end
        end else if Exns.mem kf then begin
          self#union_exn (Exns.find kf)
        end else if Kernel_function.is_definition kf then begin
          let def = Kernel_function.get_definition kf in
          ignore
            (Visitor.visitFramacFunction (self:>Visitor.frama_c_visitor) def);
          let callee_exn = Exns.find kf in
          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
        end;
        SkipChildren
      | Call _ ->
        (* Function pointer: we consider that it can throw any possible
           exception. *)
        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

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. *)

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"
  in "__fc_" ^ aux t

let get_type_enum t = "__fc_exn_kind_" ^ (get_type_tag t)

let get_kf_exn kf =
  if not (Exns.is_computed()) then compute();
  Exns.find kf

let exn_uncaught_name = "exn_uncaught"
let exn_kind_name = "exn_kind"
let exn_obj_name = "exn_obj"

(* enumeration for all possible exceptions *)
let generate_exn_enum exns =
  let loc = Cil_datatype.Location.unknown in
  let v = ref 0 in
  let info =
    { eorig_name = "__fc_exn_enum";
      ename = "__fc_exn_enum";
      eitems = [];
      eattr = [];
      ereferenced = true; (* not generated if no exn can be thrown *)
      ekind = IInt; (* Take into account -enum option? *)
    }
  in
  let create_enum_item t acc =
    let ve = Cil.kinteger ~loc IInt !v in
    let name = get_type_enum t in
    incr v;
    { eiorig_name = name;
      einame = name;
      eival = ve;
      eihost = info;
      eiloc = loc;
    } :: acc
  in
  let enums = Cil_datatype.Typ.Set.fold create_enum_item exns [] in
  info.eitems <- enums;
  info

(* discriminated union (i.e. struct + union) for all possible exceptions. *)
let generate_exn_union e exns =
  let loc = Cil_datatype.Location.unknown in
  let create_union_fields _ =
    let add_one_field t acc = (get_type_tag t, t, None, [], loc) :: acc in
    Cil_datatype.Typ.Set.fold add_one_field exns []
  in
  let union_name = "__fc_exn_union" in
  let exn_kind_union =
    Cil_const.mkCompInfo
      false union_name ~norig:union_name create_union_fields []
  in
  let create_struct_fields _ =
    let uncaught = (exn_uncaught_name, Cil.intType, None, [], loc) in
    let kind = (exn_kind_name, TEnum (e,[]), None, [], loc) in
    let obj =
      (exn_obj_name,
       TComp(exn_kind_union, { scache = Not_Computed } , []), None, [], loc)
    in
    [uncaught; kind; obj]
  in
  let struct_name = "__fc_exn_struct" in
  let exn_struct =
    Cil_const.mkCompInfo
      true struct_name ~norig:struct_name create_struct_fields []
  in
  exn_kind_union, exn_struct

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
  in
  let globs, added = List.fold_left iter_globs ([],false) f.globals in
  let globs =
    if added then List.rev globs
    else List.rev_append globs (List.rev_append typs globs)
  in
  f.globals <- globs;
  f

let make_init_assign loc v init =
  let rec aux lv acc = function
    | SingleInit e -> Cil.mkStmtOneInstr (Set(lv,e,loc)) :: acc
    | CompoundInit(_,l) ->
      let treat_one_offset acc (o,i) = aux (Cil.addOffsetLval o lv) acc i in
      List.fold_left treat_one_offset acc l
  in
  List.rev (aux (Var v, NoOffset) [] init)

let find_exns_func v =
  try Exns.find (Globals.Functions.get v)
  with Not_found -> Cil_datatype.Typ.Set.empty

let find_exns e =
  match e.enode with
    | 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

  val exn_union = Cil_datatype.Typ.Hashtbl.create 7

  val mutable modified_funcs = Cil_datatype.Fundec.Set.empty

  val mutable exn_struct = None

  val mutable exn_var = None

  val mutable can_throw = false

  val mutable fct_can_throw = false

  val mutable catched_var = None

  val mutable label_counter = 0

  val exn_labels = Cil_datatype.Typ.Hashtbl.create 7
  val catch_all_label = Stack.create ()

  method modified_funcs = modified_funcs

  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_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 exn_field_off name =
    List.find (fun fi -> fi.fname = name) (Extlib.the exn_struct).cfields

  method private exn_field name =
    Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)

  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_obj_field = self#exn_field exn_obj_name

  method private exn_obj_field_term = self#exn_field_term exn_obj_name

  method private exn_kind_field = self#exn_field exn_kind_name

  method private exn_kind_field_term = self#exn_field_term exn_kind_name

  method private uncaught_flag_field = self#exn_field exn_uncaught_name

  method private uncaught_flag_field_term =
    self#exn_field_term exn_uncaught_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 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) },_) ->
          let init = Cil.makeZeroInit ~loc rtyp in
          make_init_assign loc rv init @ [goto]
        | Return _ ->
          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
      | 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. *)
        DoChildren

  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

  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. *)
      | 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
      | None, None -> SkipChildren
        (* 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
      | 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
      | 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
        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
      | Instr (Call (_,f,_,loc) as instr) ->
        generate_jumps instr (find_exns f) loc
      | Instr (Local_init(_, ConsInit(f,_,_), loc) as instr) ->
        generate_jumps instr (find_exns_func f) loc
      | Throw _ when not can_throw ->
        Kernel.fatal "Unexpected Throw statement"
      | Throw(Some(e,t),loc) ->
        self#modify_current();
        let s1 = self#set_uncaught_flag loc true in
        let s2 = self#set_exn_kind loc t in
        let s3 = self#set_exn_value loc t e in
        let rv = self#jumps_to_handler loc t in
        let b = mkBlock (s1 :: s2 :: s3 :: rv) in
        s.skind <- Block b;
        SkipChildren
      | Throw (None,loc) ->
        self#modify_current ();
        let s1 = self#set_uncaught_flag loc true in
        let t = purify (Extlib.the exn_var).vtype in
        let rv = self#jumps_to_handler loc t in
        let b = mkBlock (s1 :: rv) in
        s.skind <- Block b;
        SkipChildren
      | TryCatch (t,_,_) when not can_throw ->
        self#modify_current();
        (* no exception can be thrown:
           we can simply remove the catch clauses. *)
        s.skind <- (Block t);
        DoChildren (* visit the block for nested try catch. *)
      | TryCatch (t,c,loc) ->
        self#modify_current();
        (* First, remove handlers of exceptions that cannot be thrown. *)
        let c = List.fold_right self#clean_catch_clause c [] in
        (* Visit the catch clauses first, as they are in the same catch scope
           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)
        in
        label_counter <- label_counter + 1;
        (* now generate the labels for jumping to the appropriate block when
           catching an exception. *)
        List.iter
          (function
            | (Catch_exn (v,aux),b) ->
              (* first thing that we do is to flag the exn as caught *)
              let stmt = self#set_uncaught_flag v.vdecl false in
              let label = (get_type_tag (purify v.vtype)) ^ suf in
              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)
            | (Catch_all, b) ->
              let loc =
                match b.bstmts with [] -> loc | s::_ -> Cil_datatype.Stmt.loc s
              in
              let stmt = self#set_uncaught_flag loc false in
              stmt.labels <- [Label ("catch_all" ^ suf,loc,false)];
              b.bstmts <- stmt :: b.bstmts;
              Stack.push stmt catch_all_label)
          (* We generate the bindings in reverse order, as if two clauses
             match the same type, the first one (which is the one that has
             to be taken), will be visited last, hiding the binding of the
             second in the Hashtbl. *)
          (List.rev c);
        ignore (Visitor.visitFramacBlock (self:>Visitor.frama_c_visitor) t);
        List.iter
          (function
            | (Catch_exn (v,[]), _) ->
              Cil_datatype.Typ.Hashtbl.remove exn_labels (purify v.vtype)
            | Catch_exn(_,l), _ ->
              List.iter
                (fun (v,_) ->
                  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,
                though order does not really matter here. *)
        t.bstmts <- t.bstmts @ stmts;
        s.skind <- Block t;
        SkipChildren
      | _ -> DoChildren
        
end

let prepare_file f =
  if Kernel.SimplifyCfg.get () then begin
    Cfg.prepareCFG ~keepSwitch:false f;
  end;
  File.must_recompute_cfg f

let remove_exn f =
  if Kernel.RemoveExn.get() then begin
    Visitor.visitFramacFileSameGlobals (new exn_visit) f;
    let vis = new erase_exn in
    Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) f;
    let funs = vis#modified_funcs in
    if not (Cil_datatype.Fundec.Set.is_empty funs) then Ast.mark_as_changed ();
    Cil_datatype.Fundec.Set.iter prepare_file funs
  end

let transform_category = File.register_code_transformation_category "remove_exn"

let () =
  let deps = [ (module Kernel.RemoveExn: Parameter_sig.S) ] in
  File.add_code_transformation_after_cleanup ~deps transform_category remove_exn