diff --git a/infer/src/llvm/lAst.ml b/infer/src/llvm/lAst.ml index ca5cbe64f..f78f71acf 100644 --- a/infer/src/llvm/lAst.ml +++ b/infer/src/llvm/lAst.ml @@ -46,6 +46,12 @@ and metadata_component = | TypOperand of typ option * operand | MetadataVal of metadata_value +type metadata_location = { line : int; col : int; scope : metadata_value } + +type metadata_aggregate = + | Components of metadata_component list + | Location of metadata_location + type instruction = | Ret of (typ * operand) option | UncondBranch of variable @@ -62,7 +68,7 @@ type annotated_instruction = instruction * annotation option type function_def = FunctionDef of variable * typ option * (typ * string) list * annotated_instruction list -type metadata_map = metadata_component list MetadataMap.t +type metadata_map = metadata_aggregate MetadataMap.t type program = Program of function_def list * metadata_map diff --git a/infer/src/llvm/lLexer.mll b/infer/src/llvm/lLexer.mll index f56012463..4db738a0f 100644 --- a/infer/src/llvm/lLexer.mll +++ b/infer/src/llvm/lLexer.mll @@ -55,6 +55,7 @@ rule token = parse | '>' { RANGLE } | '[' { LSQBRACK } | ']' { RSQBRACK } + | ':' { COLON } (* symbols *) | '=' { EQUALS } | '*' { STAR } @@ -171,6 +172,7 @@ rule token = parse (* METADATA *) | "!dbg" { DEBUG_ANNOTATION } + | "!MDLocation" { METADATA_LOCATION } | '!' (id as str) { NAMED_METADATA str } | '!' (nonneg_int as i) { NUMBERED_METADATA (int_of_string i) } | '!' '"' ([^ '"']* as str) '"' { METADATA_STRING str } diff --git a/infer/src/llvm/lParser.mly b/infer/src/llvm/lParser.mly index fb39f9b26..2ebd5e074 100644 --- a/infer/src/llvm/lParser.mly +++ b/infer/src/llvm/lParser.mly @@ -27,6 +27,7 @@ %token RANGLE %token LSQBRACK %token RSQBRACK +%token COLON (* symbols *) %token EQUALS %token STAR @@ -141,6 +142,7 @@ %token NUMBERED_METADATA %token METADATA_STRING %token METADATA_NODE_BEGIN +%token METADATA_LOCATION %token ATTRIBUTE_GROUP @@ -157,7 +159,7 @@ program: | targets func_defs = function_def* opt_mappings = metadata_def* EOF { let mappings = list_flatten_options opt_mappings in - let add_mapping map (metadata_id, components) = MetadataMap.add metadata_id components map in + let add_mapping map (metadata_id, aggregate) = MetadataMap.add metadata_id aggregate map in let metadata_map = list_fold_left add_mapping MetadataMap.empty mappings in Program (func_defs, metadata_map) } @@ -176,16 +178,27 @@ target_triple: metadata_def: | NAMED_METADATA EQUALS numbered_metadata_node { None } - | metadata_id = NUMBERED_METADATA EQUALS components = metadata_node { Some (metadata_id, components) } + | metadata_id = NUMBERED_METADATA EQUALS aggregate = metadata_aggregate { Some + (metadata_id, aggregate) } numbered_metadata_node: | METADATA_NODE_BEGIN metadata_ids = separated_list(COMMA, NUMBERED_METADATA) RBRACE { metadata_ids } +metadata_aggregate: + | components = metadata_node { Components components } + | location = metadata_location { Location location } + +metadata_location: + | METADATA_LOCATION LPAREN IDENT COLON line_num = CONSTANT_INT COMMA + IDENT COLON col_num = CONSTANT_INT COMMA + IDENT COLON i = NUMBERED_METADATA RPAREN + { { line = line_num; col = col_num; scope = MetadataVar i} } + metadata_node: | METADATA? METADATA_NODE_BEGIN components = separated_list(COMMA, metadata_component) RBRACE { components } metadata_component: - | tp = typ? op = operand { TypOperand (tp, op) } + | METADATA? tp = typ? op = operand { TypOperand (tp, op) } | METADATA? value = metadata_value { MetadataVal value } metadata_value: diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 83906752c..7caa6fab8 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -39,17 +39,21 @@ let rec trans_typ : LAst.typ -> Sil.typ = function let get_source_filename (metadata : LAst.metadata_map) : DB.source_file = match MetadataMap.find 1 metadata with - | MetadataVal (MetadataString file_str) :: _ -> DB.source_file_from_string file_str - | _ -> raise (MalformedMetadata "Source file name was expected at head of metadata variable !1.") + | Components (MetadataVal (MetadataString file_str) :: _) -> + DB.source_file_from_string file_str + | _ -> raise (MalformedMetadata "Source file name was expected in first component of metadata variable !1.") 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 + | Components (TypOperand (_, Const (Cint line_num)) :: _) -> + let open Sil in { line = line_num; col = -1; file = get_source_filename metadata; nLOC = -1 } - | [] -> raise (MalformedMetadata "Instruction annotation refers to empty metadata node.") + | Location loc -> + let open Sil in + { line = loc.line; col = loc.col; file = get_source_filename metadata; nLOC = -1 } | _ -> raise (MalformedMetadata ("Instruction annotation refers to metadata node " ^ "without line number as first component.")) end diff --git a/infer/tests/codetoanalyze/llvm/null_deref.ll b/infer/tests/codetoanalyze/llvm/null_deref.ll index 625006fca..905a4d2a4 100644 --- a/infer/tests/codetoanalyze/llvm/null_deref.ll +++ b/infer/tests/codetoanalyze/llvm/null_deref.ll @@ -12,38 +12,40 @@ target triple = "x86_64-apple-macosx10.10.0" ; Function Attrs: nounwind ssp uwtable define void @foo() #0 { %p = alloca i32*, align 8 - call void @llvm.dbg.declare(metadata !{i32** %p}, metadata !11), !dbg !14 - store i32* null, i32** %p, align 8, !dbg !15 - %1 = load i32** %p, align 8, !dbg !16 - store i32 42, i32* %1, align 4, !dbg !16 - ret void, !dbg !17 + call void @llvm.dbg.declare(metadata i32** %p, metadata !12, metadata !15), !dbg !16 + store i32* null, i32** %p, align 8, !dbg !16 + %1 = load i32** %p, align 8, !dbg !17 + store i32 42, i32* %1, align 4, !dbg !18 + ret void, !dbg !19 } ; Function Attrs: nounwind readnone -declare void @llvm.dbg.declare(metadata, metadata) #1 +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 attributes #0 = { nounwind ssp uwtable "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" } attributes #1 = { nounwind readnone } !llvm.dbg.cu = !{!0} -!llvm.module.flags = !{!8, !9} -!llvm.ident = !{!10} +!llvm.module.flags = !{!8, !9, !10} +!llvm.ident = !{!11} -!0 = metadata !{i32 786449, metadata !1, i32 12, metadata !"Apple LLVM version 6.1.0 (clang-602.0.53) (based on LLVM 3.6.0svn)", i1 false, metadata !"", i32 0, metadata !2, metadata !2, metadata !3, metadata !2, metadata !2, metadata !"", i32 1} ; [ DW_TAG_compile_unit ] [/Users/rohanjr/infer/infer/tests/codetoanalyze/llvm/null_deref.c] [DW_LANG_C99] -!1 = metadata !{metadata !"null_deref.c", metadata !"/Users/rohanjr/infer/infer/tests/codetoanalyze/llvm"} -!2 = metadata !{} -!3 = metadata !{metadata !4} -!4 = metadata !{i32 786478, metadata !1, metadata !5, metadata !"foo", metadata !"foo", metadata !"", i32 10, metadata !6, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 false, void ()* @foo, null, null, metadata !2, i32 10} ; [ DW_TAG_subprogram ] [line 10] [def] [foo] -!5 = metadata !{i32 786473, metadata !1} ; [ DW_TAG_file_type ] [/Users/rohanjr/infer/infer/tests/codetoanalyze/llvm/null_deref.c] -!6 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !7, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] -!7 = metadata !{null} -!8 = metadata !{i32 2, metadata !"Dwarf Version", i32 2} -!9 = metadata !{i32 2, metadata !"Debug Info Version", i32 602053001} -!10 = metadata !{metadata !"Apple LLVM version 6.1.0 (clang-602.0.53) (based on LLVM 3.6.0svn)"} -!11 = metadata !{i32 786688, metadata !4, metadata !"p", metadata !5, i32 11, metadata !12, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [p] [line 11] -!12 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, metadata !13} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from int] -!13 = metadata !{i32 786468, null, null, metadata !"int", i32 0, i64 32, i64 32, i64 0, i32 0, i32 5} ; [ DW_TAG_base_type ] [int] [line 0, size 32, align 32, offset 0, enc DW_ATE_signed] -!14 = metadata !{i32 11, i32 9, metadata !4, null} ; [ DW_TAG_lexical_block ] [/] -!15 = metadata !{i32 11, i32 4, metadata !4, null} ; [ DW_TAG_lexical_block ] [/] -!16 = metadata !{i32 12, i32 4, metadata !4, null} -!17 = metadata !{i32 13, i32 1, metadata !4, null} +!0 = !{!"0x11\0012\00clang version 3.6.1 (tags/RELEASE_361/final)\000\00\000\00\001", !1, !2, !2, !3, !2, !2} ; [ DW_TAG_compile_unit ] [/Users/rohanjr/infer/infer/tests/codetoanalyze/llvm/null_deref.c] [DW_LANG_C99] +!1 = !{!"null_deref.c", !"/Users/rohanjr/infer/infer/tests/codetoanalyze/llvm"} +!2 = !{} +!3 = !{!4} +!4 = !{!"0x2e\00foo\00foo\00\0010\000\001\000\000\00256\000\0010", !1, !5, !6, null, void ()* @foo, null, null, !2} ; [ DW_TAG_subprogram ] [line 10] [def] [foo] +!5 = !{!"0x29", !1} ; [ DW_TAG_file_type ] [/Users/rohanjr/infer/infer/tests/codetoanalyze/llvm/null_deref.c] +!6 = !{!"0x15\00\000\000\000\000\000\000", null, null, null, !7, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ] +!7 = !{null} +!8 = !{i32 2, !"Dwarf Version", i32 2} +!9 = !{i32 2, !"Debug Info Version", i32 2} +!10 = !{i32 1, !"PIC Level", i32 2} +!11 = !{!"clang version 3.6.1 (tags/RELEASE_361/final)"} +!12 = !{!"0x100\00p\0011\000", !4, !5, !13} ; [ DW_TAG_auto_variable ] [p] [line 11] +!13 = !{!"0xf\00\000\0064\0064\000\000", null, null, !14} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from int] +!14 = !{!"0x24\00int\000\0032\0032\000\000\005", null, null} ; [ DW_TAG_base_type ] [int] [line 0, size 32, align 32, offset 0, enc DW_ATE_signed] +!15 = !{!"0x102"} ; [ DW_TAG_expression ] +!16 = !MDLocation(line: 11, column: 9, scope: !4) +!17 = !MDLocation(line: 12, column: 5, scope: !4) +!18 = !MDLocation(line: 12, column: 4, scope: !4) +!19 = !MDLocation(line: 13, column: 1, scope: !4)