[threadsafety] Fix divergence due to indexing string literal in loop

Summary:
Indexing into a string literal expression would generate a fresh
variable on every application of a transformer. This violated
finiteness of the domain, and caused divergence.

Reviewed By: da319

Differential Revision: D5342951

fbshipit-source-id: e95e84e

infer/src/IR/HilExp.ml

@@ -85,11 +85,13 @@ let rec of_sil ~f_resolve_id (exp : Exp.t) typ = match exp with
               AccessPath.base_of_pvar pvar typ, of_sil ~f_resolve_id value typ)
           closure.captured_vars in
       Closure (closure.name, environment)
-  | Lindex (Const (Cstr _), index_exp) ->
+  | Lindex (Const (Cstr s), index_exp) ->
       (* indexed string literal (e.g., "foo"[1]). represent this by introducing a dummy variable
          for the string literal. if you actually need to see the value of the string literal in the
-         analysis, you should probably be using SIL *)
-      of_sil ~f_resolve_id (Exp.Lindex (Var (Ident.create_none ()), index_exp)) typ
+         analysis, you should probably be using SIL. this is unsound if the code modifies the
+         literal, e.g. using `const_cast<char*>` *)
+      of_sil ~f_resolve_id
+        (Exp.Lindex (Var (Ident.create_normal (Ident.string_to_name s) 0), index_exp)) typ
   | Lvar _ | Lfield _ | Lindex _ ->
       match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
       | Some access_path ->

infer/tests/codetoanalyze/cpp/threadsafety/string_literal.cpp

@@ -0,0 +1,19 @@
+/*
+ * Copyright (c) 2017 - 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.
+ */
+extern int nondet_int();
+extern char* nondet_string();
+
+void loop() {
+  int i = 0;
+  char* s = nondet_string();
+
+  while (nondet_int()) {
+    s[i++] = "0123456789ABCDEF"[nondet_int() % 16];
+  }
+}