Skip to content

Remove z3 string theory from String wrapper #1050

New issue

Have a question about this project? No Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “No Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? No Sign in to your account

Merged
merged 6 commits into from
Oct 16, 2022

Conversation

dtim
Copy link
Collaborator

@dtim dtim commented Oct 1, 2022

Description

This PR removes the code that depends on Z3 string theory, and replaces missing components with the overridden Java implementation.

Fixes #1058
Fixes #131

Type of Change

  • Breaking change (fix or feature that would cause existing functionality to not work as expected)

Symbolic analysis of strings may behave differently. Extra executions may be found, or executions may be missed.

How Has This Been Tested?

Automated Testing

All existing unit tests should pass.

Manual Scenario

There should be no regressions on string operations. Operations that were not supported before are not expected to work.

Sample code that I checked (correct tests are generated both with and without concrete execution).

package strings;

import org.jetbrains.annotations.NotNull;

public class StringExamples {
    public String returnArgumentOrEmptyString(String arg) {
        if (arg == null || arg.isEmpty())
            return "";
        return arg;
    }

    public boolean checkIfContainsCharacter(@NotNull String arg, char c) {
        return arg.indexOf(c) >= 0;
    }

    public boolean checkIfContainsSubstring(@NotNull String arg, @NotNull String pattern) {
        return arg.contains(pattern);
    }

    public boolean checkIfContainsProperSubstring(@NotNull String arg, @NotNull String pattern) {
        if (arg.equals(pattern))
            return false;
        return arg.contains(pattern);
    }

    public String sumToString(int a, int b) {
        int sum = a + b;
        return Integer.valueOf(sum).toString();
    }

    public String concatenate1(@NotNull String first, @NotNull String second) {
        if (first.isEmpty())
            return second;
        if (second.isEmpty())
            return first;
        return first.concat(second);
    }

    public String concatenate2(@NotNull String first, @NotNull String second) {
        if (first.isEmpty())
            return second;
        if (second.isEmpty())
            return first;
        return first + second;
    }

    public String concatenate3(@NotNull String first, @NotNull String second) {
        if (first.isEmpty())
            return second;
        if (second.isEmpty())
            return first;
        StringBuilder sb = new StringBuilder();
        sb.append(first);
        sb.append(second);
        return sb.toString();
    }

    public char[] checkToCharArray1() {
        String source = "hello";
        char[] target = source.toCharArray();
        return target;
    }

    public char[] checkToCharArray2(@NotNull String source) {
        if (source.length() < 3) {
            return new char[0];
        }
        return source.toCharArray();
    }

    public String myConcat(@NotNull String first, @NotNull String second) {
        if (first.isEmpty())
            return second;
        if (second.isEmpty())
            return first;

        final char[] firstArray = first.toCharArray();
        final char[] secondArray = second.toCharArray();
        final int fl = firstArray.length;
        final int sl = secondArray.length;
        char[] result = new char[fl + sl];
        System.arraycopy(firstArray, 0, result, 0, fl);
        System.arraycopy(secondArray, 0, result, fl, sl);
        return new String(result);
    }
}

Checklist (remove irrelevant options):

This is the author self-check list

  • The change followed the style guidelines of the UTBot project
  • Self-review of the code is passed
  • The change contains enough commentaries, particularly in hard-to-understand areas
  • New documentation is provided or existed one is altered
  • No new warnings
  • New tests have been added
  • All tests pass locally with my changes

@dtim dtim force-pushed the dtim/remove_z3_string_theory branch 7 times, most recently from 4736b35 to ef4919e Compare October 5, 2022 10:52
@dtim dtim marked this pull request as ready for review October 5, 2022 10:52
@dtim dtim requested review from CaelmBleidd and Damtev October 5, 2022 10:52
Copy link
Member

@Damtev Damtev left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall, LGTM, just some minor issues

@dtim dtim force-pushed the dtim/remove_z3_string_theory branch 2 times, most recently from 74afce3 to fee46dc Compare October 10, 2022 12:40
Copy link
Member

@Damtev Damtev left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, perhaps @CaelmBleidd has some functional issues

@dtim dtim force-pushed the dtim/remove_z3_string_theory branch 2 times, most recently from 2c3e058 to e97aee4 Compare October 13, 2022 08:15
int offset = 0;
while (value > 0) {
reversed[offset] = (char) ('0' + (value % 10));
value /= value;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why? Shouldn't it be value /= 10?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure. It seems I was too distracted when I fixed the previous comment. I should have noticed it myself.

int offset = 0;
while (value > 0) {
reversed[offset] = (char) ('0' + (value % 10));
value /= value;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same about a division

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, same "copy-paste" type error.

return "0";
}

assume(i <= 0x7FFFFFFF); // java.lang.Integer.MAX_VALUE
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we have <=, but for Byte we have just less?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For Byte, the comparison was with "max byte + 1". Replaced it with < 127 to have the same comparison in all cases.

Comment on lines 84 to 85
assume(i > 0x80000000); // java.lang.Integer.MIN_VALUE
assume(i != 0);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are redundant assumes, aren't they?

Comment on lines 49 to 56
if (s == -32768)
return "-32768";
if (s == 0)
return "0";

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please, add brackets or write it in one line

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed, thank you.

dtim added 6 commits October 15, 2022 23:54
  * Removed `UtNativeString`, `NativeStringWrapper`, string-related
    `UtExpression` subclasses
  * Implemented `toString` methods for numeric wrappers in Java
  * Restored temporarily disabled `testByteToString` test

  Complex `GenericExamples` string tests are disabled until symbolic
  part of the wrapper is enabled.
  + updated string tests w.r.t. running without concrete execution
@dtim dtim force-pushed the dtim/remove_z3_string_theory branch from 9e1952e to bfbc69c Compare October 15, 2022 19:54
@CaelmBleidd CaelmBleidd merged commit 9453e11 into main Oct 16, 2022
@CaelmBleidd CaelmBleidd deleted the dtim/remove_z3_string_theory branch October 16, 2022 05:55
No Sign up for free to join this conversation on GitHub. Already have an account? No Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Get rid of Z3 string theory in the String wrapper byteToString works for hours sometimes
3 participants