From 8ce531b3de3fdf0eb0e4a51b24f360cfd2956715 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 30 Jun 2017 05:39:51 -0700
Subject: [PATCH] [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                        |  8 +++++---
 .../cpp/threadsafety/string_literal.cpp       | 19 +++++++++++++++++++
 2 files changed, 24 insertions(+), 3 deletions(-)
 create mode 100644 infer/tests/codetoanalyze/cpp/threadsafety/string_literal.cpp

diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml
index d1cff7c44..d9df51b5a 100644
--- a/infer/src/IR/HilExp.ml
+++ b/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 ->
diff --git a/infer/tests/codetoanalyze/cpp/threadsafety/string_literal.cpp b/infer/tests/codetoanalyze/cpp/threadsafety/string_literal.cpp
new file mode 100644
index 000000000..c4538c565
--- /dev/null
+++ b/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];
+  }
+}