From 6fe86ffefd8dc38ff6365ba9cf37f2c2581a5545 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Sep 2013 13:50:35 -0700
Subject: [PATCH] Fix initialized memory error reported by Valgrind. Disable 2
 tests that produce memory leaks due to a bug in g++.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/lean_pp.cpp | 22 ++++++++++++++++++++--
 src/tests/kernel/arith.cpp     |  5 +++++
 src/tests/util/thread.cpp      |  7 ++++++-
 3 files changed, 31 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp
index e7cd99f401..b43b0471f3 100644
--- a/src/frontends/lean/lean_pp.cpp
+++ b/src/frontends/lean/lean_pp.cpp
@@ -514,7 +514,24 @@ class pp_fn {
             if (m_implicit_args) {
                 unsigned r = 0;
                 for (unsigned i = 0; i < num_args(m_app) - 1; i++) {
-                    if (!(*m_implicit_args)[i])
+                    // Remark: we need the test i >= m_implicit_args because the application
+                    // m_app may contain more arguments than the declaration of m_f.
+                    // Example:
+                    // m_f was declared as
+                    //     Pi {A : Type} (a : A) : A
+                    // Thus m_implicit_args has size 2, and contains {true, false}
+                    // indicating that the first argument is implicit.
+                    // Then, the actuall application is:
+                    //    f (Int -> Int) g 10
+                    // Assuming g has type Int -> Int.
+                    // This application is fine and has type Int.
+                    // We should not print the argument (Int -> Int) since it is
+                    // implicit.
+                    // We should view the application above as:
+                    //   (f (Int -> Int) g) 10
+                    // So, the arguments at position >= m_implicit_args->size()
+                    // are explicit by default.
+                    if (i >= m_implicit_args->size() || !(*m_implicit_args)[i])
                         r++;
                 }
                 return r;
@@ -528,7 +545,8 @@ class pp_fn {
             if (m_implicit_args) {
                 unsigned n = num_args(m_app);
                 for (unsigned j = 1; j < n; j++) {
-                    if (!(*m_implicit_args)[j-1]) {
+                    // See comment in get_num_args()
+                    if (j - 1 >= m_implicit_args->size() || !(*m_implicit_args)[j-1]) {
                         // explicit argument found
                         if (i == 0)
                             return arg(m_app, j);
diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp
index ef22ec8292..ba06706e9e 100644
--- a/src/tests/kernel/arith.cpp
+++ b/src/tests/kernel/arith.cpp
@@ -82,6 +82,10 @@ static void tst5() {
 }
 
 static void tst6() {
+#if 0
+    // Disabling test to avoid memory leak error message produced by Valgrind.
+    // The memory leak is due to a bug in the g++ compiler.
+    // Soonho reported the problem. Gcc team said this a known problem, and will be fixed
     std::cout << "tst6\n";
     std::cout << mk_int_add_fn().raw() << "\n";
     std::cout << mk_int_add_fn().raw() << "\n";
@@ -93,6 +97,7 @@ static void tst6() {
     t2.join();
     #endif
     std::cout << mk_int_add_fn().raw() << "\n";
+#endif
 }
 
 int main() {
diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp
index 8fe2ac9cf7..7a538c61de 100644
--- a/src/tests/util/thread.cpp
+++ b/src/tests/util/thread.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include <mutex>
 #include <vector>
 
-static void foo() {
+void foo() {
     static thread_local std::vector<int> v(1024);
     if (v.size() != 1024) {
         std::cerr << "Error\n";
@@ -19,11 +19,16 @@ static void foo() {
 }
 
 static void tst1() {
+#if 0
+    // Disabling test to avoid memory leak error message produced by Valgrind.
+    // The memory leak is due to a bug in the g++ compiler.
+    // Soonho reported the problem. Gcc team said this a known problem, and will be fixed
     unsigned n = 5;
     for (unsigned i = 0; i < n; i++) {
         std::thread t([](){ foo(); });
         t.join();
     }
+#endif
 }
 
 int main() {