From: Tim King <taking@cs.nyu.edu>
Date: Tue, 19 Sep 2017 22:51:50 +0000 (-0700)
Subject: Fixing a null pointer dereference in the cvc3 compatibility layer. (#1089)
X-Git-Tag: cvc5-1.0.0~5627
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76926d9278970aa393248715dc5ca06b3b337c7c;p=cvc5.git

Fixing a null pointer dereference in the cvc3 compatibility layer. (#1089)
---

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker.java b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
index 1b38a4c95..9289a8ae7 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker.java
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
@@ -160,23 +160,23 @@ public class ValidityChecker extends Embedded {
     private static native Object
 	jniCreateOp2(Object ValidityChecker, String name, Object Type, Object ExprDef) throws Cvc3Exception;
     private static native Object
-	jniEqOp() throws Cvc3Exception;
+	jniEqOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniLtOp() throws Cvc3Exception;
+	jniLtOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniLeOp() throws Cvc3Exception;
+	jniLeOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniGtOp() throws Cvc3Exception;
+	jniGtOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniGeOp() throws Cvc3Exception;
+	jniGeOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniPlusOp() throws Cvc3Exception;
+	jniPlusOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniMinusOp() throws Cvc3Exception;
+	jniMinusOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniMultOp() throws Cvc3Exception;
+	jniMultOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniDivideOp() throws Cvc3Exception;
+	jniDivideOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
 	jniFunExpr1(Object ValidityChecker, Object Op, Object Expr) throws Cvc3Exception;
     private static native Object
@@ -919,47 +919,47 @@ public class ValidityChecker extends Embedded {
 
     // '='
     public OpMut eqOp() throws Cvc3Exception {
-	return new OpMut(jniEqOp(), embeddedManager());
+	return new OpMut(jniEqOp(embedded()), embeddedManager());
     }
 
     // '<'
     public OpMut ltOp() throws Cvc3Exception {
-	return new OpMut(jniLtOp(), embeddedManager());
+	return new OpMut(jniLtOp(embedded()), embeddedManager());
     }
 
     // '<='
     public OpMut leOp() throws Cvc3Exception {
-	return new OpMut(jniLeOp(), embeddedManager());
+	return new OpMut(jniLeOp(embedded()), embeddedManager());
     }
 
     // '>'
     public OpMut gtOp() throws Cvc3Exception {
-	return new OpMut(jniGtOp(), embeddedManager());
+	return new OpMut(jniGtOp(embedded()), embeddedManager());
     }
 
     // '>='
     public OpMut geOp() throws Cvc3Exception {
-	return new OpMut(jniGeOp(), embeddedManager());
+	return new OpMut(jniGeOp(embedded()), embeddedManager());
     }
 
     // '+'
     public OpMut plusOp() throws Cvc3Exception {
-	return new OpMut(jniPlusOp(), embeddedManager());
+	return new OpMut(jniPlusOp(embedded()), embeddedManager());
     }
 
     // '-'
     public OpMut minusOp() throws Cvc3Exception {
-	return new OpMut(jniMinusOp(), embeddedManager());
+	return new OpMut(jniMinusOp(embedded()), embeddedManager());
     }
 
     // '*'
     public OpMut multOp() throws Cvc3Exception {
-	return new OpMut(jniMultOp(), embeddedManager());
+	return new OpMut(jniMultOp(embedded()), embeddedManager());
     }
 
     // '/' for rationals
     public OpMut divideOp() throws Cvc3Exception {
-	return new OpMut(jniDivideOp(), embeddedManager());
+	return new OpMut(jniDivideOp(embedded()), embeddedManager());
     }
 
     public ExprMut funExpr(Op op, Expr expr1) throws Cvc3Exception {
diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index cfda940d8..6c6a9f8cb 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -300,40 +300,40 @@ jobject m ValidityChecker vc n string name c Type type c Expr expr
 return embed_copy(env, vc->createOp(name, *type, *expr));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniEqOp
-jobject
-return embed_copy<Op>(env, Op(EQ));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), EQ));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniLtOp
-jobject
-return embed_copy<Op>(env, Op(LT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), LT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniLeOp
-jobject
-return embed_copy<Op>(env, Op(LE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), LE));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniGtOp
-jobject
-return embed_copy<Op>(env, Op(GT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), GT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniGeOp
-jobject
-return embed_copy<Op>(env, Op(GE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), GE));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniPlusOp
-jobject
-return embed_copy<Op>(env, Op(PLUS));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), PLUS));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniMinusOp
-jobject
-return embed_copy<Op>(env, Op(MINUS));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), MINUS));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniMultOp
-jobject
-return embed_copy<Op>(env, Op(MULT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), MULT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniDivideOp
-jobject
-return embed_copy<Op>(env, Op(DIVIDE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), DIVIDE));
 
 
 DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr1
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 169b49faa..df7257d3f 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -252,8 +252,8 @@ Expr::Expr(const Expr& e) : CVC4::Expr(e) {
 Expr::Expr(const CVC4::Expr& e) : CVC4::Expr(e) {
 }
 
-Expr::Expr(const CVC4::Kind k) : CVC4::Expr() {
-  *this = getEM()->operatorOf(k);
+Expr::Expr(ExprManager* em, const CVC4::Kind k) : CVC4::Expr() {
+  *this = em->operatorOf(k);
 }
 
 Expr Expr::eqExpr(const Expr& right) const {
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 25e3ae32f..daac466d5 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -321,7 +321,7 @@ public:
   Expr();
   Expr(const Expr& e);
   Expr(const CVC4::Expr& e);
-  Expr(CVC4::Kind k);
+  Expr(ExprManager* em, CVC4::Kind k);
 
   // Compound expression constructors
   Expr eqExpr(const Expr& right) const;