|
|
@ -6,9 +6,11 @@
|
|
|
|
* LICENSE file in the root directory of this source tree. An additional grant
|
|
|
|
* LICENSE file in the root directory of this source tree. An additional grant
|
|
|
|
* of patent rights can be found in the PATENTS file in the same directory.
|
|
|
|
* of patent rights can be found in the PATENTS file in the same directory.
|
|
|
|
*)
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
open LAst
|
|
|
|
open LAst
|
|
|
|
|
|
|
|
|
|
|
|
exception ImproperTypeError of string
|
|
|
|
exception ImproperTypeError of string
|
|
|
|
|
|
|
|
exception MalformedMetadata of string
|
|
|
|
exception Unimplemented of string
|
|
|
|
exception Unimplemented of string
|
|
|
|
|
|
|
|
|
|
|
|
let ident_of_variable (var : LAst.variable) : Ident.t = (* TODO: use unique stamps *)
|
|
|
|
let ident_of_variable (var : LAst.variable) : Ident.t = (* TODO: use unique stamps *)
|
|
|
@ -34,27 +36,41 @@ let rec trans_typ : LAst.typ -> Sil.typ = function
|
|
|
|
| Tlabel -> raise (ImproperTypeError "Tried to generate Sil type from LLVM label type.")
|
|
|
|
| Tlabel -> raise (ImproperTypeError "Tried to generate Sil type from LLVM label type.")
|
|
|
|
| Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.")
|
|
|
|
| Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.")
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let location_of_annotation_option (metadata : LAst.metadata_map)
|
|
|
|
|
|
|
|
: LAst.annotation option -> Sil.location = function
|
|
|
|
|
|
|
|
| None -> Sil.dummy_location (* no annotation means no source location *)
|
|
|
|
|
|
|
|
| Some (Annotation i) ->
|
|
|
|
|
|
|
|
begin match MetadataMap.find i metadata with
|
|
|
|
|
|
|
|
| TypOperand (_, Const (Cint line_num)) :: _ -> let open Sil in
|
|
|
|
|
|
|
|
{ line = line_num; col = -1; file = DB.source_file_empty; nLOC = -1 }
|
|
|
|
|
|
|
|
| [] -> raise (MalformedMetadata "Instruction annotation refers to empty metadata node.")
|
|
|
|
|
|
|
|
| _ -> raise (MalformedMetadata ("Instruction annotation refers to metadata node " ^
|
|
|
|
|
|
|
|
"without line number as first component."))
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
(* Generate list of SIL instructions and list of local variables *)
|
|
|
|
(* Generate list of SIL instructions and list of local variables *)
|
|
|
|
let rec trans_annotated_instrs (cfg : Cfg.cfg) (procdesc : Cfg.Procdesc.t)
|
|
|
|
let rec trans_annotated_instrs
|
|
|
|
: LAst.annotated_instr list -> Sil.instr list * (Mangled.t * Sil.typ) list = function
|
|
|
|
(cfg : Cfg.cfg) (procdesc : Cfg.Procdesc.t) (metadata : LAst.metadata_map)
|
|
|
|
|
|
|
|
: LAst.annotated_instr list -> Sil.instr list * (Mangled.t * Sil.typ) list = function
|
|
|
|
| [] -> ([], [])
|
|
|
|
| [] -> ([], [])
|
|
|
|
| h :: t ->
|
|
|
|
| (instr, anno) :: t ->
|
|
|
|
let (sil_instrs, locals) = trans_annotated_instrs cfg procdesc t in
|
|
|
|
let (sil_instrs, locals) = trans_annotated_instrs cfg procdesc metadata t in
|
|
|
|
begin match fst h with
|
|
|
|
let location = location_of_annotation_option metadata anno in
|
|
|
|
| Ret None -> (sil_instrs, locals)
|
|
|
|
begin match instr with
|
|
|
|
| Ret (Some (tp, exp)) ->
|
|
|
|
| Ret None -> (sil_instrs, locals)
|
|
|
|
let procname = Cfg.Procdesc.get_proc_name procdesc in
|
|
|
|
| Ret (Some (tp, exp)) ->
|
|
|
|
let ret_var = Sil.get_ret_pvar procname in
|
|
|
|
let procname = Cfg.Procdesc.get_proc_name procdesc in
|
|
|
|
let new_sil_instr =
|
|
|
|
let ret_var = Sil.get_ret_pvar procname in
|
|
|
|
Sil.Set (Sil.Lvar ret_var, trans_typ tp, trans_operand exp, Sil.dummy_location) in
|
|
|
|
let new_sil_instr =
|
|
|
|
(new_sil_instr :: sil_instrs, locals)
|
|
|
|
Sil.Set (Sil.Lvar ret_var, trans_typ tp, trans_operand exp, location) in
|
|
|
|
| Load (var, tp, ptr) ->
|
|
|
|
(new_sil_instr :: sil_instrs, locals)
|
|
|
|
let new_sil_instr =
|
|
|
|
| Load (var, tp, ptr) ->
|
|
|
|
Sil.Letderef (ident_of_variable var, trans_variable ptr, trans_typ tp, Sil.dummy_location) in
|
|
|
|
let new_sil_instr =
|
|
|
|
(new_sil_instr :: sil_instrs, locals)
|
|
|
|
Sil.Letderef (ident_of_variable var, trans_variable ptr, trans_typ tp, location) in
|
|
|
|
| Store (op, tp, var) ->
|
|
|
|
(new_sil_instr :: sil_instrs, locals)
|
|
|
|
let new_sil_instr =
|
|
|
|
| Store (op, tp, var) ->
|
|
|
|
Sil.Set (trans_variable var, trans_typ tp, trans_operand op, Sil.dummy_location) in
|
|
|
|
let new_sil_instr =
|
|
|
|
|
|
|
|
Sil.Set (trans_variable var, trans_typ tp, trans_operand op, location) in
|
|
|
|
(new_sil_instr :: sil_instrs, locals)
|
|
|
|
(new_sil_instr :: sil_instrs, locals)
|
|
|
|
| Alloc (var, tp, num_elems) ->
|
|
|
|
| Alloc (var, tp, num_elems) ->
|
|
|
|
(* num_elems currently ignored *)
|
|
|
|
(* num_elems currently ignored *)
|
|
|
@ -68,7 +84,8 @@ let rec trans_annotated_instrs (cfg : Cfg.cfg) (procdesc : Cfg.Procdesc.t)
|
|
|
|
end
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
(* Update CFG and call graph with new function definition *)
|
|
|
|
(* Update CFG and call graph with new function definition *)
|
|
|
|
let trans_func_def (cfg : Cfg.cfg) (cg: Cg.t) : LAst.func_def -> unit = function
|
|
|
|
let trans_func_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
|
|
|
|
|
|
|
|
: LAst.func_def -> unit = function
|
|
|
|
FuncDef (func_name, ret_tp_opt, params, annotated_instrs) ->
|
|
|
|
FuncDef (func_name, ret_tp_opt, params, annotated_instrs) ->
|
|
|
|
let (proc_attrs : Sil.proc_attributes) =
|
|
|
|
let (proc_attrs : Sil.proc_attributes) =
|
|
|
|
let open Sil in
|
|
|
|
let open Sil in
|
|
|
@ -92,7 +109,7 @@ let trans_func_def (cfg : Cfg.cfg) (cg: Cg.t) : LAst.func_def -> unit = function
|
|
|
|
ret_type = (match ret_tp_opt with
|
|
|
|
ret_type = (match ret_tp_opt with
|
|
|
|
| None -> Sil.Tvoid
|
|
|
|
| None -> Sil.Tvoid
|
|
|
|
| Some ret_tp -> trans_typ ret_tp);
|
|
|
|
| Some ret_tp -> trans_typ ret_tp);
|
|
|
|
formals = List.map (fun (tp, name) -> (name, trans_typ tp)) params;
|
|
|
|
formals = Utils.list_map (fun (tp, name) -> (name, trans_typ tp)) params;
|
|
|
|
locals = []; (* TODO *)
|
|
|
|
locals = []; (* TODO *)
|
|
|
|
captured = [];
|
|
|
|
captured = [];
|
|
|
|
loc = Sil.dummy_location
|
|
|
|
loc = Sil.dummy_location
|
|
|
@ -110,7 +127,7 @@ let trans_func_def (cfg : Cfg.cfg) (cg: Cg.t) : LAst.func_def -> unit = function
|
|
|
|
(* link all nodes in a chain for now *)
|
|
|
|
(* link all nodes in a chain for now *)
|
|
|
|
| [] -> Cfg.Node.set_succs_exn start_node [exit_node] [exit_node]
|
|
|
|
| [] -> Cfg.Node.set_succs_exn start_node [exit_node] [exit_node]
|
|
|
|
| nd :: nds -> Cfg.Node.set_succs_exn start_node [nd] [exit_node]; link_nodes nd nds in
|
|
|
|
| nd :: nds -> Cfg.Node.set_succs_exn start_node [nd] [exit_node]; link_nodes nd nds in
|
|
|
|
let (sil_instrs, locals) = trans_annotated_instrs cfg procdesc annotated_instrs in
|
|
|
|
let (sil_instrs, locals) = trans_annotated_instrs cfg procdesc metadata annotated_instrs in
|
|
|
|
let nodes = Utils.list_map (node_of_sil_instr cfg procdesc) sil_instrs in
|
|
|
|
let nodes = Utils.list_map (node_of_sil_instr cfg procdesc) sil_instrs in
|
|
|
|
Cfg.Procdesc.set_start_node procdesc start_node;
|
|
|
|
Cfg.Procdesc.set_start_node procdesc start_node;
|
|
|
|
Cfg.Procdesc.set_exit_node procdesc exit_node;
|
|
|
|
Cfg.Procdesc.set_exit_node procdesc exit_node;
|
|
|
@ -119,9 +136,9 @@ let trans_func_def (cfg : Cfg.cfg) (cg: Cg.t) : LAst.func_def -> unit = function
|
|
|
|
Cg.add_node cg procname
|
|
|
|
Cg.add_node cg procname
|
|
|
|
|
|
|
|
|
|
|
|
let trans_prog : LAst.prog -> Cfg.cfg * Cg.t * Sil.tenv = function
|
|
|
|
let trans_prog : LAst.prog -> Cfg.cfg * Cg.t * Sil.tenv = function
|
|
|
|
Prog (func_defs, _) ->
|
|
|
|
Prog (func_defs, metadata) ->
|
|
|
|
let cfg = Cfg.Node.create_cfg () in
|
|
|
|
let cfg = Cfg.Node.create_cfg () in
|
|
|
|
let cg = Cg.create () in
|
|
|
|
let cg = Cg.create () in
|
|
|
|
let tenv = Sil.create_tenv () in
|
|
|
|
let tenv = Sil.create_tenv () in
|
|
|
|
List.iter (trans_func_def cfg cg) func_defs;
|
|
|
|
Utils.list_iter (trans_func_def cfg cg metadata) func_defs;
|
|
|
|
(cfg, cg, tenv)
|
|
|
|
(cfg, cg, tenv)
|
|
|
|