From 52ee910c128e6bbcf7299a0660511deacadb14f1 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 5 Nov 2018 09:01:03 -0800
Subject: [PATCH] API: Fix assignment operators (#2680)

The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.

Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
---
 src/api/cvc4cpp.cpp          | 27 --------------------------
 src/api/cvc4cpp.h            | 23 ----------------------
 test/unit/api/CMakeLists.txt |  1 +
 test/unit/api/term_black.h   | 37 ++++++++++++++++++++++++++++++++++++
 4 files changed, 38 insertions(+), 50 deletions(-)
 create mode 100644 test/unit/api/term_black.h

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be7c5c665..b4d3b013d 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -749,15 +749,6 @@ Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
 
 Sort::~Sort() {}
 
-Sort& Sort::operator=(const Sort& s)
-{
-  if (this != &s)
-  {
-    *d_type = *s.d_type;
-  }
-  return *this;
-}
-
 bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
 
 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
@@ -1008,15 +999,6 @@ Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
 
 Term::~Term() {}
 
-Term& Term::operator=(const Term& t)
-{
-  if (this != &t)
-  {
-    *d_expr = *t.d_expr;
-  }
-  return *this;
-}
-
 bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
@@ -1180,15 +1162,6 @@ OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
 
 OpTerm::~OpTerm() {}
 
-OpTerm& OpTerm::operator=(const OpTerm& t)
-{
-  if (this != &t)
-  {
-    *d_expr = *t.d_expr;
-  }
-  return *this;
-}
-
 bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; }
 
 bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index fc07a1cd7..aebeffb0d 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -196,13 +196,6 @@ class CVC4_PUBLIC Sort
    */
   ~Sort();
 
-  /**
-   * Assignment operator.
-   * @param s the sort to assign to this sort
-   * @return this sort after assignment
-   */
-  Sort& operator=(const Sort& s);
-
   /**
    * Comparison for structural equality.
    * @param s the sort to compare to
@@ -553,14 +546,6 @@ class CVC4_PUBLIC Term
    */
   ~Term();
 
-  /**
-   * Assignment operator, makes a copy of the given term.
-   * Both terms must belong to the same solver object.
-   * @param t the term to assign
-   * @return the reference to this term after assignment
-   */
-  Term& operator=(const Term& t);
-
   /**
    * Syntactic equality operator.
    * Return true if both terms are syntactically identical.
@@ -843,14 +828,6 @@ class CVC4_PUBLIC OpTerm
    */
   ~OpTerm();
 
-  /**
-   * Assignment operator, makes a copy of the given operator term.
-   * Both terms must belong to the same solver object.
-   * @param t the term to assign
-   * @return the reference to this operator term after assignment
-   */
-  OpTerm& operator=(const OpTerm& t);
-
   /**
    * Syntactic equality operator.
    * Return true if both operator terms are syntactically identical.
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 90d34f7c6..025575e41 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -2,3 +2,4 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(api_guards_black api)
+cvc4_add_unit_test_black(term_black api)
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
new file mode 100644
index 000000000..c2ca1cb08
--- /dev/null
+++ b/test/unit/api/term_black.h
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file term_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the Term class
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class TermBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override {}
+  void tearDown() override {}
+
+  void testTermAssignment()
+  {
+    Term t1 = d_solver.mkReal(1);
+    Term t2 = t1;
+    t2 = d_solver.mkReal(2);
+    TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+  }
+
+ private:
+  Solver d_solver;
+};
-- 
2.30.2