[infer] Translate VAArgExpr to the builtin function

Reviewed By: mbouaziz

Differential Revision: D14206463

fbshipit-source-id: 821983012

infer/src/biabduction/BuiltinDefn.ml

@@ -18,7 +18,7 @@ type t = Builtin.registered
 let execute___builtin_va_arg {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} :
     Builtin.ret_typ =
   match args with
-  | [_; _; (lexp3, typ3)] ->
+  | [(lexp3, typ3)] ->
       let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in
       SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton instr') [(prop_, path)]
   | _ ->

infer/src/clang/cTrans.ml

@@ -1072,6 +1072,27 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
           ~return:res_trans_call.return all_res_trans
 
 
+  and va_arg_trans trans_state si stmt expr_info =
+    let context = trans_state.context in
+    let fn_type_no_ref = CType_decl.get_type_from_expr_info expr_info context.CContext.tenv in
+    let function_type = add_reference_if_glvalue fn_type_no_ref expr_info in
+    let sil_loc =
+      CLocation.location_of_stmt_info context.translation_unit_context.source_file si
+    in
+    let trans_state_pri = PriorityNode.try_claim_priority_node trans_state si in
+    let sil_fe = Exp.Const (Const.Cfun BuiltinDecl.__builtin_va_arg) in
+    let trans_state_param = {trans_state_pri with succ_nodes= []; var_exp_typ= None} in
+    let result_trans_param = exec_with_glvalue_as_reference instruction trans_state_param stmt in
+    let res_trans_call =
+      create_call_instr trans_state function_type sil_fe [result_trans_param.return] sil_loc
+        CallFlags.default ~is_objc_method:false ~is_inherited_ctor:false
+    in
+    let node_name = Procdesc.Node.Call (Exp.to_string sil_fe) in
+    let all_res_trans = [result_trans_param; res_trans_call] in
+    PriorityNode.compute_results_to_parent trans_state_pri sil_loc ~node_name si
+      ~return:res_trans_call.return all_res_trans
+
+
   and cxx_method_construct_call_trans trans_state_pri result_trans_callee params_stmt si
       function_type is_cpp_call_virtual extra_res_trans ~is_inherited_ctor =
     let context = trans_state_pri.context in
@@ -3447,8 +3468,10 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
         booleanValue_trans trans_state expr_info type_trait_info.Clang_ast_t.xtti_value
     | CXXNoexceptExpr (_, _, expr_info, cxx_noexcept_expr_info) ->
         booleanValue_trans trans_state expr_info cxx_noexcept_expr_info.Clang_ast_t.xnee_value
-    | OffsetOfExpr (_, _, expr_info) | VAArgExpr (_, _, expr_info) ->
+    | OffsetOfExpr (_, _, expr_info) | VAArgExpr (_, [], expr_info) ->
         undefined_expr trans_state expr_info
+    | VAArgExpr (stmt_info, stmt :: _, ei) ->
+        va_arg_trans trans_state stmt_info stmt ei
     | ArrayInitIndexExpr _ | ArrayInitLoopExpr _ ->
         no_op_trans trans_state.succ_nodes
     (* vector instructions for OpenCL etc. we basically ignore these for now; just translate the

infer/tests/codetoanalyze/c/bufferoverrun/function_call.c

@@ -8,6 +8,7 @@
  */
 
 #include <stdlib.h>
+#include <stdarg.h>
 
 struct S {
   int field;
@@ -141,3 +142,21 @@ void call_call_access_index_4_on_S3_Bad() {
   s.ptr = malloc(sizeof(int) * 4);
   call_access_index_4_on_S3(&s);
 }
+
+void va_arg_int(int* a, ...) {
+  va_list args;
+  va_start(args, a);
+  int i = va_arg(args, int);
+  a[i] = 0;
+  va_end(args);
+}
+
+void call_va_arg_int_Good_FP() {
+  int a[10];
+  va_arg_int(a, 5);
+}
+
+void call_va_arg_int_Bad() {
+  int a[10];
+  va_arg_int(a, 10);
+}

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -115,6 +115,8 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_call_access_index_4_on_S3_Ba
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/function_call.c, call_va_arg_int_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Unknown value from: __builtin_va_arg,Assignment,<Length trace>,Parameter `*a`,Array access: Offset: [-oo, +oo] Size: 10 by call to `va_arg_int` ]
+codetoanalyze/c/bufferoverrun/function_call.c, call_va_arg_int_Good_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Unknown value from: __builtin_va_arg,Assignment,<Length trace>,Parameter `*a`,Array access: Offset: [-oo, +oo] Size: 10 by call to `va_arg_int` ]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `x->field`,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot

@@ -40,7 +40,7 @@ digraph cfg {
 	
 
 	 "vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_10" -> "vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_5" ;
-"vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_11" [label="11:  DeclStmt \n   n$5=_fun___variable_initialization(&i:int) assign_last [line 13, column 3]\n  *&i:int=n$4 [line 13, column 3]\n  EXIT_SCOPE(n$4,n$5); [line 13, column 3]\n " shape="box"]
+"vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_11" [label="11:  DeclStmt \n   n$5=_fun___variable_initialization(&i:int) assign_last [line 13, column 3]\n  n$4=_fun___builtin_va_arg(&valist:void*) [line 13, column 11]\n  *&i:int=n$4 [line 13, column 3]\n  EXIT_SCOPE(n$4,n$5); [line 13, column 3]\n " shape="box"]
 	
 
 	 "vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_11" -> "vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_6" ;