diff --git a/infer/src/Makefile b/infer/src/Makefile index c6f621872..47d401d9e 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -108,7 +108,7 @@ FCP_CLANG_AST_CACHE = $(addprefix $(CLANG_OCAML_ROOT)/, clang_ast_cache.ml clang #### LLVM declarations #### LLVM_SOURCES = llvm -INFERLLVM_MAIN = $(LLVM_SOURCES)/main +INFERLLVM_MAIN = $(LLVM_SOURCES)/lMain INFERLLVM_BINARY = $(BINDIR)/InferLLVM #### End of declarations #### diff --git a/infer/src/llvm/ast.ml b/infer/src/llvm/ast.ml deleted file mode 100644 index b9492f68b..000000000 --- a/infer/src/llvm/ast.ml +++ /dev/null @@ -1,23 +0,0 @@ -(* -* Copyright (c) 2015 - present Facebook, Inc. -* All rights reserved. -* -* This source code is licensed under the BSD style license found in the -* 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. - *) -type prog = Prog of func_def list -and func_def = FuncDef of string * typ option * (typ * string) list * instr list -and typ = - | Tint of int - | Tfloat (* just one type for now *) - | Tptr of typ - | Tvector of int * typ - | Tarray of int * typ -and instr = - | Ret of (typ * value) option -and value = - | True - | False - | Intlit of int - | Null diff --git a/infer/src/llvm/examples/empty.ll b/infer/src/llvm/examples/empty.ll new file mode 100644 index 000000000..e69de29bb diff --git a/infer/src/llvm/examples/empty_func.ll b/infer/src/llvm/examples/empty_func.ll new file mode 100644 index 000000000..41107c9c3 --- /dev/null +++ b/infer/src/llvm/examples/empty_func.ll @@ -0,0 +1,4 @@ +; Definition of main function +define void @main() { + ret void +} diff --git a/infer/src/llvm/examples/simple_func.ll b/infer/src/llvm/examples/simple_func.ll new file mode 100644 index 000000000..39aeede51 --- /dev/null +++ b/infer/src/llvm/examples/simple_func.ll @@ -0,0 +1,4 @@ +; Definition of main function +define i32 @main() { + ret i32 0 +} diff --git a/infer/src/llvm/lAst.ml b/infer/src/llvm/lAst.ml new file mode 100644 index 000000000..0490871cb --- /dev/null +++ b/infer/src/llvm/lAst.ml @@ -0,0 +1,43 @@ +(* +* Copyright (c) 2015 - present Facebook, Inc. +* All rights reserved. +* +* This source code is licensed under the BSD style license found in the +* 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. +*) + +(** Representation of LLVM constructs *) + +type variable = + | Global of string + | Local of string + +type constant = + | Cint of int + | Cnull + +type operand = + | Var of variable + | Const of constant + +type typ = + | Tint of int + | Tfloat (* just one type for now *) + | Tptr of typ + | Tvector of int * typ + | Tarray of int * typ + | Tlabel + | Tmetadata + +type instr = + | Ret of (typ * operand) option + | UncondBranch of variable + | CondBranch of operand * variable * variable + +type func_def = FuncDef of variable * typ option * (typ * string) list * instr list + +type prog = Prog of func_def list + +let string_of_variable : variable -> string = function + | Global str | Local str -> str diff --git a/infer/src/llvm/lexer.mll b/infer/src/llvm/lLexer.mll similarity index 94% rename from infer/src/llvm/lexer.mll rename to infer/src/llvm/lLexer.mll index 3f0f01fce..fdb49bc55 100644 --- a/infer/src/llvm/lexer.mll +++ b/infer/src/llvm/lLexer.mll @@ -5,10 +5,10 @@ * This source code is licensed under the BSD style license found in the * 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. - *) +*) { open Lexing - open Parser + open LParser exception LexingError of string } @@ -26,7 +26,7 @@ let lower = ['a'-'z'] let upper = ['A'-'Z'] let id_special_char = ['-' '$' '.' '_'] let id_char = lower | upper | id_special_char -let id = ['%' '@'] id_char (id_char | digit)* +let id = id_char (id_char | digit)* rule token = parse | space | comment { token lexbuf } @@ -52,6 +52,7 @@ rule token = parse (* TYPES *) | "void" { VOID } + | "i1" { BIT (* INT 1 *) } | 'i' (pos_int as width) { INT (int_of_string width) } | "half" { HALF } | "float" { FLOAT } @@ -65,9 +66,9 @@ rule token = parse | pos_int as size { SIZE (int_of_string size) } (* CONSTANTS *) - | "true" { TRUE } - | "false" { FALSE } - | intlit as i { INTLIT (int_of_string i) } + | "true" { CONSTINT 1 } + | "false" { CONSTINT 0 } + | intlit as i { CONSTINT (int_of_string i) } (* floating point constants *) | "null" { NULL } @@ -150,6 +151,8 @@ rule token = parse | "landingpad" { LANDINGPAD } (* identifiers - make this complete *) + | '@' { AT } + | '%' { PERCENT } | id as str { IDENT str } | eof { EOF } diff --git a/infer/src/llvm/main.ml b/infer/src/llvm/lMain.ml similarity index 83% rename from infer/src/llvm/main.ml rename to infer/src/llvm/lMain.ml index 7eaf47fac..30c752ece 100644 --- a/infer/src/llvm/main.ml +++ b/infer/src/llvm/lMain.ml @@ -5,7 +5,7 @@ * This source code is licensed under the BSD style license found in the * 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. - *) +*) open Lexing open Printf @@ -17,8 +17,8 @@ let () = try else let filename = Sys.argv.(1) in let lexbuf = Lexing.from_channel (open_in filename) in - let prog = Parser.prog Lexer.token lexbuf in - let pretty = Pretty.pretty_prog prog in - print_string pretty + let prog = LParser.prog LLexer.token lexbuf in + let pretty = LPretty.pretty_prog prog in + LTrans.gen_prog prog; () with | UsageError msg -> print_string ("Usage error: " ^ msg ^ "\n") diff --git a/infer/src/llvm/parser.mly b/infer/src/llvm/lParser.mly similarity index 80% rename from infer/src/llvm/parser.mly rename to infer/src/llvm/lParser.mly index 906bdf595..601cf9f70 100644 --- a/infer/src/llvm/parser.mly +++ b/infer/src/llvm/lParser.mly @@ -5,9 +5,9 @@ * This source code is licensed under the BSD style license found in the * 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. - *) +*) %{ - open Ast + open LAst %} (* keywords *) @@ -27,9 +27,12 @@ %token EQUALS %token STAR %token X +%token AT +%token PERCENT (* TYPES *) %token VOID +%token BIT (* i1 *) %token INT %token HALF %token FLOAT @@ -43,9 +46,7 @@ %token SIZE (* CONSTANTS *) -%token TRUE -%token FALSE -%token INTLIT +%token CONSTINT %token NULL (* INSTRUCTIONS *) @@ -131,10 +132,10 @@ %token EOF %start prog -%type prog -%type func_def -%type ret_typ -%type typ +%type prog +%type func_def +%type ret_typ +%type typ %% @@ -142,7 +143,7 @@ prog: | defs=list(func_def) EOF { Prog defs } func_def: - | DEFINE ret_tp=ret_typ name=IDENT LPAREN params=separated_list(COMMA, pair(typ, IDENT)) RPAREN instrs=block { + | DEFINE ret_tp=ret_typ name=variable LPAREN params=separated_list(COMMA, pair(typ, IDENT)) RPAREN instrs=block { FuncDef (name, ret_tp, params, instrs) } ret_typ: @@ -154,8 +155,8 @@ typ: (*| X86_MMX { () }*) | tp=vector_typ { tp } | LSQBRACK sz=SIZE X tp=element_typ RSQBRACK { Tarray (sz, tp) } (* array type *) - (*| LABEL { () } - | METADATA { () }*) + | LABEL { Tlabel } + | METADATA { Tmetadata } (* TODO structs *) vector_typ: @@ -182,11 +183,13 @@ block: instr: | term=terminator { term } - | IDENT EQUALS binop { Ret None } + | variable EQUALS binop { Ret None } (* TODO *) terminator: - | RET tp=typ v=value { Ret (Some (tp, v)) } + | RET tp=typ op=operand { Ret (Some (tp, op)) } | RET VOID { Ret None } + | BR LABEL lbl=variable { UncondBranch lbl } + | BR BIT op=operand COMMA LABEL lbl1=variable COMMA LABEL lbl2=variable { CondBranch (op, lbl1, lbl2) } (* | switch | indirectbr @@ -216,8 +219,8 @@ binop: | OR binop_args { () } | XOR binop_args { () } (* vector *) - | EXTRACTELEMENT vector_typ value COMMA typ IDENT { () } - | INSERTELEMENT vector_typ value COMMA typ element COMMA typ IDENT { () } + | EXTRACTELEMENT vector_typ operand COMMA typ operand { () } + | INSERTELEMENT vector_typ operand COMMA typ operand COMMA typ operand { () } arith_options: | option(NUW) option(NSW) { () } @@ -231,14 +234,13 @@ binop_args: (* below is fuzzy *) operand: - (* variable *) - | v=value { v } + | var=variable { Var var } + | const=constant { Const const } -element: - | v=value { v } +variable: + | AT id=IDENT { Global id } + | PERCENT id=IDENT { Local id } -value: - | TRUE { True } - | FALSE { False } - | i=INTLIT { Intlit i } - | NULL { Null } +constant: + | i=CONSTINT { Cint i } + | NULL { Cnull } diff --git a/infer/src/llvm/lPretty.ml b/infer/src/llvm/lPretty.ml new file mode 100644 index 000000000..6df2302de --- /dev/null +++ b/infer/src/llvm/lPretty.ml @@ -0,0 +1,56 @@ +(* +* Copyright (c) 2015 - present Facebook, Inc. +* All rights reserved. +* +* This source code is licensed under the BSD style license found in the +* 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. +*) +open LAst + +let concatmap (sep : string) (f : 'a -> string) (l : 'a list) : string = + String.concat sep (List.map f l) + +let pretty_variable : variable -> string = function + | Global id -> "@" ^ id + | Local id -> "%" ^ id + +let pretty_constant : constant -> string = function + | Cint i -> string_of_int i + | Cnull -> "null" + +let pretty_operand : operand -> string = function + | Var var -> pretty_variable var + | Const const -> pretty_constant const + +let rec pretty_typ : typ -> string = function + | Tint width -> "i" ^ string_of_int width + | Tfloat (* just one type for now *) -> "float" + | Tptr tp -> pretty_typ tp ^ "*" + | Tvector (sz, tp) -> "<" ^ string_of_int sz ^ " x " ^ pretty_typ tp ^ ">" + | Tlabel -> "label" + | Tmetadata -> "metadata" + | Tarray (sz, tp) -> "[" ^ string_of_int sz ^ " x " ^ pretty_typ tp ^ "]" + +let pretty_ret_typ : typ option -> string = function + | None -> "void" + | Some tp -> pretty_typ tp + +let pretty_instr : instr -> string = function + | Ret None -> "ret void" + | Ret (Some (tp, op)) -> "ret " ^ pretty_typ tp ^ " " ^ pretty_operand op + | UncondBranch label -> "br label " ^ pretty_variable label + | CondBranch (op, label1, label2) -> + "br i1 " ^ pretty_operand op ^ ", label " ^ pretty_variable label1 ^ + ", label " ^ pretty_variable label2 + +let pretty_instr_ln (i : instr) : string = pretty_instr i ^ "\n" + +let pretty_func_def : func_def -> string = function + FuncDef (name, ret_tp, params, instrs) -> + "define " ^ pretty_ret_typ ret_tp ^ " " ^ pretty_variable name ^ "(" ^ + concatmap ", " (fun (tp, id) -> pretty_typ tp ^ " " ^ id) params ^ ") {\n" ^ + concatmap "" pretty_instr_ln instrs ^ "}\n" + +let pretty_prog : prog -> string = function + Prog defs -> concatmap "" pretty_func_def defs diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml new file mode 100644 index 000000000..5268e91e5 --- /dev/null +++ b/infer/src/llvm/lTrans.ml @@ -0,0 +1,77 @@ +(* +* Copyright (c) 2015 - Facebook. +* All rights reserved. +*) +open LAst + +exception ImproperTypeError of string +exception Unimplemented of string + +let gen_variable : variable -> Sil.exp = function (* HACK *) + | Global id -> Sil.Var (Ident.create_normal (Ident.string_to_name id) 0) + | Local id -> Sil.Var (Ident.create_normal (Ident.string_to_name id) 0) + +let gen_constant : constant -> Sil.exp = function + | Cint i -> Sil.Const (Sil.Cint (Sil.Int.of_int i)) + | Cnull -> Sil.exp_null + +let gen_operand : operand -> Sil.exp = function + | Var var -> gen_variable var + | Const const -> gen_constant const + +let rec gen_typ : typ -> Sil.typ = function + | Tint i -> Sil.Tint IInt (* need to actually check what size int is needed here *) + | Tfloat -> Sil.Tfloat FFloat + | Tptr tp -> Tptr (gen_typ tp, Pk_pointer) + | Tvector (i, tp) + | Tarray (i, tp) -> Sil.Tarray (gen_typ tp, Sil.Const (Sil.Cint (Sil.Int.of_int i))) + | Tlabel -> raise (ImproperTypeError "Tried to generate Sil type from LLVM label type.") + | Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.") + +let gen_instr (cfg : Cfg.cfg) (pdesc : Cfg.Procdesc.t) : instr -> Sil.instr list = function + | Ret None -> [] + | Ret (Some (tp, exp)) -> + let ret_var = Sil.get_ret_pvar (Cfg.Procdesc.get_proc_name pdesc) in + [Sil.Set (Sil.Lvar ret_var, gen_typ tp, gen_operand exp, Sil.dummy_location)] + | _ -> raise (Unimplemented "Need to translate instruction to SIL.") + +(* Modify the cfg in place *) +let gen_func_def (old_cfg : Cfg.cfg) : func_def -> unit = function + FuncDef (func_name, ret_tp_opt, params, instrs) -> + let (proc_attrs : Sil.proc_attributes) = + { access = Sil.Default; + exceptions = []; + is_abstract = false; + is_bridge_method = false; + is_objc_instance_method = false; + is_synthetic_method = false; + language = Sil.C_CPP; + func_attributes = []; + method_annotation = Sil.method_annotation_empty + } in + let (pdesc_builder : Cfg.Procdesc.proc_desc_builder) = + { cfg = old_cfg; + name = Procname.from_string (string_of_variable func_name); + is_defined = true; (** is defined and not just declared *) + proc_attributes = proc_attrs; + ret_type = (match ret_tp_opt with + | None -> Sil.Tvoid + | Some ret_tp -> gen_typ ret_tp); + formals = List.map (fun (tp, name) -> (name, gen_typ tp)) params; + locals = []; (* TODO *) + captured = []; + loc = Sil.dummy_location + } in + let nodekind_of_instr : instr -> Cfg.Node.nodekind = function + | Ret _ -> Cfg.Node.Stmt_node "method_body" + | _ -> raise (Unimplemented "Need to get node type for instruction.") in + let add_instr (cfg : Cfg.cfg) (pdesc : Cfg.Procdesc.t) (ins : instr) : unit = + Cfg.Node.create cfg Sil.dummy_location (nodekind_of_instr ins) + (gen_instr cfg pdesc ins) pdesc []; () in + let pdesc = Cfg.Procdesc.create pdesc_builder in + List.iter (fun ins -> add_instr old_cfg pdesc ins) instrs + +let gen_prog : prog -> Cfg.cfg = function + Prog fds -> + let cfg = Cfg.Node.create_cfg () in + List.iter (gen_func_def cfg) fds; cfg diff --git a/infer/src/llvm/pretty.ml b/infer/src/llvm/pretty.ml deleted file mode 100644 index dec28f346..000000000 --- a/infer/src/llvm/pretty.ml +++ /dev/null @@ -1,43 +0,0 @@ -(* -* Copyright (c) 2015 - present Facebook, Inc. -* All rights reserved. -* -* This source code is licensed under the BSD style license found in the -* 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. - *) -open Ast - -let concatmap (sep : string) (f : 'a -> string) (l : 'a list) : string = String.concat sep (List.map f l) - -let rec pretty_prog : prog -> string = function - Prog defs -> concatmap "" pretty_func_def defs - -and pretty_func_def : func_def -> string = function - FuncDef (name, ret_tp, params, instrs) -> - "define " ^ pretty_ret_typ ret_tp ^ " " ^ name ^ "(" ^ - concatmap ", " (fun (tp, id) -> pretty_typ tp ^ " " ^ id) params ^ ") {\n" ^ - concatmap "" pretty_instr_ln instrs ^ "}\n" - -and pretty_ret_typ : typ option -> string = function - | None -> "void" - | Some tp -> pretty_typ tp - -and pretty_typ : typ -> string = function - | Tint width -> "i" ^ string_of_int width - | Tfloat (* just one type for now *) -> "float" - | Tptr tp -> pretty_typ tp ^ "*" - | Tvector (sz, tp) -> "<" ^ string_of_int sz ^ " x " ^ pretty_typ tp ^ ">" - | Tarray (sz, tp) -> "[" ^ string_of_int sz ^ " x " ^ pretty_typ tp ^ "]" - -and pretty_instr_ln (i : instr) : string = pretty_instr i ^ "\n" - -and pretty_instr : instr -> string = function - | Ret None -> "ret void" - | Ret (Some (tp, v)) -> "ret " ^ pretty_typ tp ^ " " ^ pretty_value v - -and pretty_value : value -> string = function - | True -> "true" - | False -> "false" - | Intlit i -> string_of_int i - | Null -> "null"