smt2_solver: implement (echo "string") #3463

kroening · 2018-11-25T12:37:42Z

Test to be added.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 0fdf8ee).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92466982

peterschrammel · 2018-11-25T14:25:17Z

I assume a test will come...

tautschnig · 2018-11-28T14:10:22Z

src/solvers/smt2/smt2_solver.cpp

@@ -185,8 +208,6 @@ void smt2_solvert::command(const std::string &c)
    | ( define-fun-rec hfunction_def i )
    | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
    | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
-    | ( echo hstringi )
-    | ( exit )


Why is exit deleted here?

Unrelated cleanup

tautschnig · 2018-11-28T14:11:36Z

src/solvers/smt2/smt2_solver.cpp

@@ -162,6 +178,13 @@ void smt2_solvert::command(const std::string &c)
        std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'


Hmm, just noticed this one: we already have smt2_format by now.

Well, yes, as of #3461. Will tweak.

tautschnig · 2018-11-28T14:12:22Z

src/solvers/smt2/smt2_solver.cpp

+      if(next_token() != STRING_LITERAL)
+        std::cout << "expected string literal" << '\n';
+      else
+        std::cout << smt2_string_literal(buffer) << '\n';


It seems errors and desired output are indistinguishable?

Needs #3441

tautschnig · 2018-11-28T14:14:40Z

src/solvers/smt2/smt2_solver.cpp

+    if(c == '"')
+      result += "\"\"";
+    else
+      result += c;


How about replace_all from string_utils.{h,cpp}?

Uh, actually, that's implemented in a really inefficient way when the string gets longer. Let's say separate PR.

I find it quite brave that a character-by-character operator+= on a string is used in an argument about efficiency. Also I wonder whether anyone uses echo with long strings.

The loop in smt2_string_literal is quasi linear (assuming a standard allocation strategy), despite the +=.
The one in replace_all is quadratic.

When you say "standard allocation strategy" what is it that you are assuming? Growing by some factor > 1? That at least does not seem to be the case with the STL implementation shipped with GCC 8, which just increases the allocation by the size of the string being appended.

No, this refers to the ability of the allocator to avoid fragmentation; the threat is that this becomes quadratic if there's a non-trivial number of re-allocations.

I was wrong in my previous comment, _M_create actually does exponential growth of the allocation. So we should just fix replace_all.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: a1fe6d4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92910569

kroening · 2018-11-29T11:06:50Z

Now with test!

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f59fc6e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92992375

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 97980ec).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92994410
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

kroening added the work in progress label Nov 25, 2018

kroening requested review from martin-cs, peterschrammel and tautschnig as code owners November 25, 2018 12:37

allredj reviewed Nov 25, 2018

View reviewed changes

peterschrammel approved these changes Nov 25, 2018

View reviewed changes

tautschnig reviewed Nov 28, 2018

View reviewed changes

kroening force-pushed the smt2_solver_echo branch from 0fdf8ee to a1fe6d4 Compare November 28, 2018 19:41

allredj reviewed Nov 28, 2018

View reviewed changes

tautschnig mentioned this pull request Nov 29, 2018

add replace_all documentation #3478

Merged

3 tasks

smt2_solver: implement (echo "string")

f59fc6e

kroening force-pushed the smt2_solver_echo branch from a1fe6d4 to f59fc6e Compare November 29, 2018 11:06

kroening removed the work in progress label Nov 29, 2018

kroening requested review from pkesseli and smowton as code owners November 29, 2018 11:28

kroening force-pushed the smt2_solver_echo branch from 97980ec to f59fc6e Compare November 29, 2018 11:28

allredj reviewed Nov 29, 2018

View reviewed changes

kroening merged commit 6293c53 into develop Nov 29, 2018

kroening deleted the smt2_solver_echo branch November 29, 2018 18:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

smt2_solver: implement (echo "string") #3463

smt2_solver: implement (echo "string") #3463

kroening commented Nov 25, 2018 •

edited

Loading

allredj left a comment

peterschrammel commented Nov 25, 2018

tautschnig Nov 28, 2018

kroening Nov 28, 2018

tautschnig Nov 28, 2018

kroening Nov 28, 2018

tautschnig Nov 28, 2018

kroening Nov 28, 2018

tautschnig Nov 28, 2018

kroening Nov 28, 2018

tautschnig Nov 28, 2018

kroening Nov 29, 2018

tautschnig Nov 29, 2018

kroening Nov 29, 2018

tautschnig Nov 29, 2018

allredj left a comment

kroening commented Nov 29, 2018

allredj left a comment

allredj left a comment

		@@ -162,6 +178,13 @@ void smt2_solvert::command(const std::string &c)
		std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'

smt2_solver: implement (echo "string") #3463

smt2_solver: implement (echo "string") #3463

Conversation

kroening commented Nov 25, 2018 • edited Loading

allredj left a comment

Choose a reason for hiding this comment

peterschrammel commented Nov 25, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

kroening commented Nov 29, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

kroening commented Nov 25, 2018 •

edited

Loading