Skip to content

Commit 0a8499b

Browse files
DavidGalllobDavidGalllob
committed
- fixed some intense bugs
1 parent d72a024 commit 0a8499b

File tree

8 files changed

+145
-54
lines changed

8 files changed

+145
-54
lines changed

‎src/org/sosy_lab/java_smt/basicimpl/FloatingPointGenerator.java‎

Lines changed: 37 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -52,15 +52,24 @@ protected static void logMakeFloatingPointFromBigInteger(
5252
List<Object> inputParams = new ArrayList<>();
5353
// SIGN BIT
5454
String output = "(fp ";
55-
if (sign) output += "#b1 ";
56-
else output += "#b0 ";
55+
if (sign) {
56+
output += "#b1 ";
57+
} else {
58+
output += "#b0 ";
59+
}
5760
// EXPONENT
58-
if (exponent.toString().length() == type.getExponentSize()) output += "#b";
59-
else output += "#x";
61+
if (exponent.toString().length() == type.getExponentSize()) {
62+
output += "#b";
63+
} else {
64+
output += "#x";
65+
}
6066
output += exponent + " ";
6167
// MANTISSA
62-
if (mantissa.toString().length() == type.getMantissaSize()) output += "#b";
63-
else output += "#x";
68+
if (mantissa.toString().length() == type.getMantissaSize()) {
69+
output += "#b";
70+
} else {
71+
output += "#x";
72+
}
6473
output += mantissa + ")";
6574
inputParams.add(output);
6675
Function<List<Object>, String> functionToString = createString -> (String) createString.get(0);
@@ -159,8 +168,13 @@ public static String convertToSMTLibBinaryForInteger(int value, FloatingPointTyp
159168
}
160169

161170
// Return the SMT-LIB formatted string
162-
return "(fp #b" + signBit + " #b" + String.format("%" + exponentSize + "s", Integer.toBinaryString(biasedExponent))
163-
.replace(' ', '0') + " #b" + mantissaBits
171+
return "(fp #b"
172+
+ signBit
173+
+ " #b"
174+
+ String.format("%" + exponentSize + "s", Integer.toBinaryString(biasedExponent))
175+
.replace(' ', '0')
176+
+ " #b"
177+
+ mantissaBits
164178
+ ")";
165179
}
166180

@@ -376,9 +390,9 @@ public static String convertToSMTLibBinary(Rational value, FloatingPointType typ
376390
final int exponentSize = type.getExponentSize();
377391
final int mantissaSize = type.getMantissaSize();
378392
final int bias = (1 << (exponentSize - 1)) - 1;
379-
final Rational TWO = Rational.ofLong(2);
380-
final Rational ONE = Rational.ofLong(1);
381-
final Rational HALF = Rational.ofLongs(1, 2);
393+
final Rational two = Rational.ofLong(2);
394+
final Rational one = Rational.ofLong(1);
395+
final Rational half = Rational.ofLongs(1, 2);
382396

383397
// Handle zero
384398
if (value.equals(Rational.ZERO)) {
@@ -392,14 +406,14 @@ public static String convertToSMTLibBinary(Rational value, FloatingPointType typ
392406

393407
// Calculate exponent
394408
int exponent = 0;
395-
if (absValue.compareTo(ONE) >= 0) {
396-
while (absValue.compareTo(TWO) >= 0) {
397-
absValue = absValue.divides(TWO);
409+
if (absValue.compareTo(one) >= 0) {
410+
while (absValue.compareTo(two) >= 0) {
411+
absValue = absValue.divides(two);
398412
exponent++;
399413
}
400414
} else {
401-
while (absValue.compareTo(ONE) < 0) {
402-
absValue = absValue.times(TWO);
415+
while (absValue.compareTo(one) < 0) {
416+
absValue = absValue.times(two);
403417
exponent--;
404418
}
405419
}
@@ -421,21 +435,21 @@ public static String convertToSMTLibBinary(Rational value, FloatingPointType typ
421435

422436
// Calculate mantissa bits
423437
StringBuilder mantissaBits = new StringBuilder(mantissaSize);
424-
Rational remainder = absValue.minus(ONE);
438+
Rational remainder = absValue.minus(one);
425439

426440
for (int i = 0; i < mantissaSize; i++) {
427-
remainder = remainder.times(TWO);
428-
if (remainder.compareTo(ONE) >= 0) {
441+
remainder = remainder.times(two);
442+
if (remainder.compareTo(one) >= 0) {
429443
mantissaBits.append('1');
430-
remainder = remainder.minus(ONE);
444+
remainder = remainder.minus(one);
431445
} else {
432446
mantissaBits.append('0');
433447
}
434448
}
435449

436450
// Rounding - round to nearest, ties to even
437-
if (remainder.compareTo(HALF) > 0
438-
|| (remainder.equals(HALF) && mantissaBits.charAt(mantissaSize - 1) == '1')) {
451+
if (remainder.compareTo(half) > 0
452+
|| (remainder.equals(half) && mantissaBits.charAt(mantissaSize - 1) == '1')) {
439453
// Need to round up
440454
boolean carry = true;
441455
for (int i = mantissaSize - 1; i >= 0 && carry; i--) {
@@ -640,7 +654,7 @@ protected static void logFPRound(
640654

641655
protected static void logFPAssignment(
642656
BooleanFormula result, FloatingPointFormula num1, FloatingPointFormula num2) {
643-
logBinaryOp(result, "fp.assign", num1, num2);
657+
logBinaryOp(result, "=", num1, num2);
644658
}
645659

646660
protected static void logFPCastTo(

‎src/org/sosy_lab/java_smt/basicimpl/StringGenerator.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ protected static void logRegexClosure(RegexFormula result, RegexFormula regex) {
112112

113113
protected static void logRegexComplement(RegexFormula result, RegexFormula regex) {
114114
List<Object> inputParams = ImmutableList.of(regex);
115-
logOperation(result, inputParams, "(re.complement %s)", Keyword.SKIP);
115+
logOperation(result, inputParams, "(re.comp %s)", Keyword.SKIP);
116116
}
117117

118118
protected static void logRegexDifference(
@@ -150,7 +150,7 @@ protected static void logReplaceAll(
150150
logOperation(result, inputParams, "(str.replaceall %s %s %s)", Keyword.SKIP);
151151
}
152152

153-
protected static void logMakeRegex(RegexFormula result, String value) {
153+
protected static void logMakeRegex(Object result, String value) {
154154
String unquotedValue = value.replace("\"", "");
155155
List<Object> inputParams = ImmutableList.of(unquotedValue);
156156
logOperation(result, inputParams, "(str.to_re \"%s\")", Keyword.SKIP);

‎src/org/sosy_lab/java_smt/basicimpl/UFGenerator.java‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,11 @@ protected static String checkUFInputType(ImmutableList<FormulaType<?>> args) {
4747
return "String";
4848
} else if (arg.isFloatingPointType()) {
4949
FloatingPointType type = (FloatingPointType) arg;
50-
return "(_ FloatingPoint " + type.getExponentSize() + " " + type.getExponentSize() + ")";
50+
return "(_ FloatingPoint "
51+
+ type.getExponentSize()
52+
+ " "
53+
+ (type.getMantissaSize() + 1)
54+
+ ")";
5155
} else {
5256
throw new GeneratorException(arg + " is not a known sort. ");
5357
}
@@ -76,7 +80,11 @@ protected static String checkUFOutputType(FormulaType<?> out) {
7680
return "String";
7781
} else if (out.isFloatingPointType()) {
7882
FloatingPointType type = (FloatingPointType) out;
79-
return "(_ FloatingPoint " + type.getExponentSize() + " " + type.getExponentSize() + ")";
83+
return "(_ FloatingPoint "
84+
+ type.getExponentSize()
85+
+ " "
86+
+ (type.getMantissaSize() + 1)
87+
+ ")";
8088
} else {
8189
throw new GeneratorException(out + " is not a known sort. ");
8290
}

‎src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -391,6 +391,9 @@ public FormulaType<?> visitSort_id(Sort_idContext ctx) {
391391
if (isABitVecInSMT2(type)) {
392392
return parseToBitVecFormulaTypeIfMatching(type);
393393
}
394+
if (isAFloatingPointInSMT2(type)) {
395+
return parseToFPOnlyNumeral(type);
396+
}
394397

395398
switch (type) {
396399
case "Int":
@@ -1716,7 +1719,7 @@ && isInteger(operators.get(1))) {
17161719
}
17171720
String value = operands.get(0).toString();
17181721
value = value.replace("\"", "");
1719-
return Objects.requireNonNull(smgr).makeRegex(value);
1722+
return Objects.requireNonNull(smgr).makeRegex(Pattern.quote(value));
17201723
case "str.is_digit":
17211724
throw new UnsupportedOperationException("str.is_digit is not supported in JavaSMT");
17221725
case "str.in_re":
@@ -1836,7 +1839,7 @@ && isInteger(operators.get(1))) {
18361839
return result;
18371840
} else if (operands.stream().anyMatch(c -> c instanceof FloatingPointFormula)) {
18381841
return Objects.requireNonNull(fpmgr)
1839-
.equalWithFPSemantics(
1842+
.assignment(
18401843
(FloatingPointFormula) operands.get(0),
18411844
(FloatingPointFormula) operands.get(1));
18421845
} else if (operands.stream().anyMatch(c -> c instanceof StringFormula)) {

‎src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessFloatingPointFormulaManager.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -177,7 +177,7 @@ protected SMTLIB2Formula remainder(SMTLIB2Formula pParam1, SMTLIB2Formula pParam
177177

178178
@Override
179179
protected SMTLIB2Formula assignment(SMTLIB2Formula pParam1, SMTLIB2Formula pParam2) {
180-
return new SMTLIB2Formula(pParam1.getExponent(), pParam1.getMantissa());
180+
return new SMTLIB2Formula(new DummyType(DummyType.Type.BOOLEAN));
181181
}
182182

183183
@Override

‎src/org/sosy_lab/java_smt/test/SMTLIB2FloatingPointTest.java‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@
2424
import org.sosy_lab.java_smt.api.FloatingPointFormula;
2525
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
2626
import org.sosy_lab.java_smt.api.FormulaType;
27+
import org.sosy_lab.java_smt.api.ProverEnvironment;
2728
import org.sosy_lab.java_smt.api.SolverException;
2829
import org.sosy_lab.java_smt.basicimpl.Generator;
2930

@@ -315,6 +316,41 @@ public void testDeclareFloatingPointsWithBits()
315316
assertThat(actualResult).isEqualTo(expectedResult);
316317
}
317318

319+
@Test
320+
public void testComplexFP()
321+
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
322+
requireFloats();
323+
assume().that(solverToUse()).isNotEqualTo(Solvers.BITWUZLA);
324+
assume()
325+
.withMessage("For some reason very slow here")
326+
.that(solverToUse())
327+
.isNotEqualTo(Solvers.MATHSAT5);
328+
String x =
329+
"(declare-fun |c::main::$tmp::return_value_nondet_double$1@1!0&0#1|\n"
330+
+ " ()\n"
331+
+ " (_ FloatingPoint 11 53))\n"
332+
+ "(declare-fun |nondet$symex::nondet0| () (_ FloatingPoint 11 53))\n"
333+
+ "(declare-fun |c::main::main::1::x@1!0&0#1| () (_ FloatingPoint 11 53))\n"
334+
+ "(declare-fun |execution_statet::guard_exec@0!0| () Bool)\n"
335+
+ "(assert (= |nondet$symex::nondet0|\n"
336+
+ " |c::main::$tmp::return_value_nondet_double$1@1!0&0#1|))\n"
337+
+ "(assert (= |c::main::$tmp::return_value_nondet_double$1@1!0&0#1|\n"
338+
+ " |c::main::main::1::x@1!0&0#1|))\n"
339+
+ "(assert (let ((a!1 (not (=> true\n"
340+
+ " (=> |execution_statet::guard_exec@0!0|\n"
341+
+ " (fp.eq |c::main::main::1::x@1!0&0#1|\n"
342+
+ " |c::main::main::1::x@1!0&0#1|))))))\n"
343+
+ " a!1))";
344+
345+
BooleanFormula parsed = mgr.universalParseFromString(x);
346+
Generator.assembleConstraint(parsed);
347+
System.out.println(parsed + "\n-----------\n");
348+
System.out.println(Generator.getSMTLIB2String());
349+
ProverEnvironment proverEnvironment = context.newProverEnvironment();
350+
proverEnvironment.addConstraint(parsed);
351+
assertThat(proverEnvironment.isUnsat()).isFalse();
352+
}
353+
318354
@Test
319355
public void testDeclareFloatingPointsWithBitVectors()
320356
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {

‎src/org/sosy_lab/java_smt/test/SMTLIB2StringTest.java‎

Lines changed: 52 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
import org.sosy_lab.java_smt.api.FormulaType;
1919
import org.sosy_lab.java_smt.api.FunctionDeclaration;
2020
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
21+
import org.sosy_lab.java_smt.api.ProverEnvironment;
2122
import org.sosy_lab.java_smt.api.RegexFormula;
2223
import org.sosy_lab.java_smt.api.SolverException;
2324
import org.sosy_lab.java_smt.api.StringFormula;
@@ -421,6 +422,34 @@ public void testRegexRange()
421422
assertThat(actualResult).isEqualTo(regexMatch);
422423
}
423424

425+
@Test
426+
public void testComplexRegex()
427+
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
428+
requireStrings();
429+
String x =
430+
"(declare-const X String)\n"
431+
+ "(assert (not (str.in_re X (str.to_re"
432+
+ " \"HXLogOnlyDaemonactivityIterenetFrom:Class\\u{a}\"))))\n"
433+
+ "(assert (not (str.in_re X (re.union (re.++ (str.to_re \"\\u{22}\") (re.* (re.comp"
434+
+ " (str.to_re \"\\u{22}\"))) (str.to_re \"\\u{22}\")) (re.++ (re.opt (str.to_re"
435+
+ " \"\\u{d}\\u{a}\")) (str.to_re \"\\u{a}'\") (re.* (re.comp (str.to_re"
436+
+ " \"\\u{d}\"))))))))\n"
437+
+ "(assert (not (str.in_re X (re.++ (str.to_re \"Download\") (re.+ (re.range \"0\""
438+
+ " \"9\")) (str.to_re \"ocllceclbhs/gth\\u{a}\")))))\n"
439+
+ "(assert (str.in_re X (str.to_re"
440+
+ " \"User-Agent:Host:TeomaBarHost:HoursHost:\\u{a}\")))\n"
441+
+ "(assert (not (str.in_re X (re.++ (str.to_re \"$\") (re.opt (re.* (re.range \"0\""
442+
+ " \"9\"))) (re.opt (str.to_re \",\")) (re.opt (re.* (re.range \"0\" \"9\"))) (re.opt"
443+
+ " (str.to_re \",\")) (re.* (re.range \"0\" \"9\")) (str.to_re \".\") (re.* (re.range"
444+
+ " \"0\" \"9\")) (str.to_re \"\\u{a}\")))))\n"
445+
+ "(check-sat)";
446+
447+
BooleanFormula parsed = mgr.universalParseFromString(x);
448+
ProverEnvironment proverEnvironment = context.newProverEnvironment();
449+
proverEnvironment.addConstraint(parsed);
450+
assertThat(proverEnvironment.isUnsat()).isFalse();
451+
}
452+
424453
@Test
425454
public void testDeclareUFString()
426455
throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
@@ -429,47 +458,47 @@ public void testDeclareUFString()
429458
+ "(set-info :category \"random\")\n"
430459
+ "(set-info :status sat)\n"
431460
+ "\n"
432-
+ "(declare-fun I () String)\n"
433-
+ "(declare-fun B () String)\n"
434-
+ "(declare-fun G () String)\n"
435-
+ "(declare-fun F () String)\n"
436-
+ "(assert (= (str.++ \"cefcdf\" B \"bgcdfedb\" G \"fgafb\" G \"gefdgcbadf\") (str.++"
437-
+ " G \"ef\" I \"dcbbf\" G \"f\" G \"bbg\" F \"gefdg\" G \"badf\") ))\n"
461+
+ "(declare-fun i () String)\n"
462+
+ "(declare-fun b () String)\n"
463+
+ "(declare-fun g () String)\n"
464+
+ "(declare-fun f () String)\n"
465+
+ "(assert (= (str.++ \"cefcdf\" b \"bgcdfedb\" g \"fgafb\" g \"gefdgcbadf\") (str.++"
466+
+ " g \"ef\" i \"dcbbf\" g \"f\" g \"bbg\" f \"gefdg\" g \"badf\") ))\n"
438467
+ "(check-sat)\n"
439468
+ "\n"
440469
+ "(exit)";
441470

442471
BooleanFormula actualResult = mgr.universalParseFromString(x);
443-
FunctionDeclaration<StringFormula> I =
444-
mgr.getUFManager().declareUF("I", FormulaType.StringType);
445-
FunctionDeclaration<StringFormula> B =
446-
mgr.getUFManager().declareUF("B", FormulaType.StringType);
447-
FunctionDeclaration<StringFormula> G =
448-
mgr.getUFManager().declareUF("G", FormulaType.StringType);
449-
FunctionDeclaration<StringFormula> F =
450-
mgr.getUFManager().declareUF("F", FormulaType.StringType);
472+
FunctionDeclaration<StringFormula> i =
473+
mgr.getUFManager().declareUF("i", FormulaType.StringType);
474+
FunctionDeclaration<StringFormula> b =
475+
mgr.getUFManager().declareUF("b", FormulaType.StringType);
476+
FunctionDeclaration<StringFormula> g =
477+
mgr.getUFManager().declareUF("g", FormulaType.StringType);
478+
FunctionDeclaration<StringFormula> f =
479+
mgr.getUFManager().declareUF("f", FormulaType.StringType);
451480
BooleanFormula constraint =
452481
smgr.equal(
453482
smgr.concat(
454483
smgr.makeString("cefcdf"),
455-
fmgr.callUF(B),
484+
fmgr.callUF(b),
456485
smgr.makeString("bgcdfedb"),
457-
fmgr.callUF(G),
486+
fmgr.callUF(g),
458487
smgr.makeString("fgafb"),
459-
fmgr.callUF(G),
488+
fmgr.callUF(g),
460489
smgr.makeString("gefdgcbadf")),
461490
smgr.concat(
462-
fmgr.callUF(G),
491+
fmgr.callUF(g),
463492
smgr.makeString("ef"),
464-
fmgr.callUF(I),
493+
fmgr.callUF(i),
465494
smgr.makeString("dcbbf"),
466-
fmgr.callUF(G),
495+
fmgr.callUF(g),
467496
smgr.makeString("f"),
468-
fmgr.callUF(G),
497+
fmgr.callUF(g),
469498
smgr.makeString("bbg"),
470-
fmgr.callUF(F),
499+
fmgr.callUF(f),
471500
smgr.makeString("gefdg"),
472-
fmgr.callUF(G),
501+
fmgr.callUF(g),
473502
smgr.makeString("badf")));
474503

475504
Generator.assembleConstraint(actualResult);

‎src/org/sosy_lab/java_smt/utils/ParseGenerateAndReparse.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,9 @@
44
// SPDX-License-Identifier: Apache-2.0
55
package org.sosy_lab.java_smt.utils;
66

7-
import com.microsoft.z3.*;
87
import com.microsoft.z3.Context;
8+
import com.microsoft.z3.Solver;
9+
import com.microsoft.z3.Status;
910
import java.io.IOException;
1011
import java.nio.charset.Charset;
1112
import java.nio.file.Files;

0 commit comments

Comments
 (0)