From 3ab2d2a44195f6ae0ad70e13c2664908721ee75a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Jan 2014 10:15:00 -0800
Subject: [PATCH] fix(frontends/lean/parser): memory leak due to g++ bug

g++ implementation of std::initializer_list has bug.
http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html

This commit memory leaks triggered by this bug.
It also adds minimal tests to expose three different instances of the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser_expr.cpp | 9 ++++++---
 tests/lean/leak1.lean              | 1 +
 tests/lean/leak1.lean.expected.out | 3 +++
 tests/lean/leak2.lean              | 1 +
 tests/lean/leak2.lean.expected.out | 3 +++
 tests/lean/leak3.lean              | 1 +
 tests/lean/leak3.lean.expected.out | 3 +++
 7 files changed, 18 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/leak1.lean
 create mode 100644 tests/lean/leak1.lean.expected.out
 create mode 100644 tests/lean/leak2.lean
 create mode 100644 tests/lean/leak2.lean.expected.out
 create mode 100644 tests/lean/leak3.lean
 create mode 100644 tests/lean/leak3.lean.expected.out

diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp
index a79b5fc60..7d0f25efe 100644
--- a/src/frontends/lean/parser_expr.cpp
+++ b/src/frontends/lean/parser_expr.cpp
@@ -152,17 +152,20 @@ expr parser_imp::parse_postfix(expr const & left, operator_info const & op, pos_
 
 /** \brief Parse a user defined infix operator. */
 expr parser_imp::parse_infix(expr const & left, operator_info const & op, pos_info const & op_pos) {
-    return mk_application(op, op_pos, {left, parse_expr(op.get_precedence()+1)});
+    expr right = parse_expr(op.get_precedence()+1);
+    return mk_application(op, op_pos, {left, right});
 }
 
 /** \brief Parse a user defined infix-left operator. */
 expr parser_imp::parse_infixl(expr const & left, operator_info const & op, pos_info const & op_pos) {
-    return mk_application(op, op_pos, {left, parse_expr(op.get_precedence())});
+    expr right = parse_expr(op.get_precedence());
+    return mk_application(op, op_pos, {left, right});
 }
 
 /** \brief Parse a user defined infix-right operator. */
 expr parser_imp::parse_infixr(expr const & left, operator_info const & op, pos_info const & op_pos) {
-    return mk_application(op, op_pos, {left, parse_expr(op.get_precedence()-1)});
+    expr right = parse_expr(op.get_precedence()-1);
+    return mk_application(op, op_pos, {left, right});
 }
 
 /**
diff --git a/tests/lean/leak1.lean b/tests/lean/leak1.lean
new file mode 100644
index 000000000..32e929928
--- /dev/null
+++ b/tests/lean/leak1.lean
@@ -0,0 +1 @@
+print 2 * a
\ No newline at end of file
diff --git a/tests/lean/leak1.lean.expected.out b/tests/lean/leak1.lean.expected.out
new file mode 100644
index 000000000..93446efe4
--- /dev/null
+++ b/tests/lean/leak1.lean.expected.out
@@ -0,0 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
+leak1.lean:1:11: error: unknown identifier 'a'
diff --git a/tests/lean/leak2.lean b/tests/lean/leak2.lean
new file mode 100644
index 000000000..160778679
--- /dev/null
+++ b/tests/lean/leak2.lean
@@ -0,0 +1 @@
+print true /\ a
\ No newline at end of file
diff --git a/tests/lean/leak2.lean.expected.out b/tests/lean/leak2.lean.expected.out
new file mode 100644
index 000000000..4010e4317
--- /dev/null
+++ b/tests/lean/leak2.lean.expected.out
@@ -0,0 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
+leak2.lean:1:15: error: unknown identifier 'a'
diff --git a/tests/lean/leak3.lean b/tests/lean/leak3.lean
new file mode 100644
index 000000000..e67141864
--- /dev/null
+++ b/tests/lean/leak3.lean
@@ -0,0 +1 @@
+print true = a
\ No newline at end of file
diff --git a/tests/lean/leak3.lean.expected.out b/tests/lean/leak3.lean.expected.out
new file mode 100644
index 000000000..02d0fe1b4
--- /dev/null
+++ b/tests/lean/leak3.lean.expected.out
@@ -0,0 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
+leak3.lean:1:14: error: unknown identifier 'a'