Extract string dependencies into its own files #4695

allredj · 2019-05-22T16:05:47Z

Based on #4692.
Only review last 2 commits.

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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj · 2019-05-23T08:50:29Z

rebased onto develop

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 15f36b6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112897202
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

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

romainbrenguier · 2019-05-23T09:59:54Z

src/solvers/strings/string_dependencies.h

+
+#include "string_builtin_function.h"
+#include "string_constraint.h"
+#include "string_constraint_generator.h"


I think this include is not necessary if you forward declare string_constraint_generatort

romainbrenguier · 2019-05-23T10:00:41Z

src/solvers/strings/string_dependencies.h

+#include <memory>
+
+#include "string_builtin_function.h"
+#include "string_constraint.h"


I don't think this include is used

antlechner · 2019-05-23T11:15:48Z

src/solvers/strings/string_refinement.cpp

@@ -31,6 +31,7 @@ Author: Alberto Griggio, [email protected]

 #include "equation_symbol_mapping.h"
 #include "string_constraint_instantiation.h"
+#include "string_dependencies.h"


This is already included in the header file so it's not needed here.

antlechner · 2019-05-23T13:33:01Z

src/solvers/strings/string_dependencies.cpp

+  return *node.data;
+}
+
+static void for_each_atomic_string(


❓ Is this function related only to dependencies?

Probably not, but it's not used anywhere else yet.

antlechner · 2019-05-23T13:35:42Z

src/solvers/strings/string_dependencies.h

+
+/// Keep track of dependencies between strings.
+/// Each string points to the builtin_function calls on which it depends.
+/// Each builtin_function points to the strings on which the result depends.


💡 I think this documentation should answer the question "What do we mean by dependency and how do we use dependencies?". An example, or reference to markdown files about the string solver with examples, would be helpful here. I don't know much about the string solver so I'm mostly guessing what any of this might mean. 🙂

antlechner · 2019-05-23T13:55:59Z

src/solvers/strings/string_dependencies.cpp

+#include <iostream>
+#include <numeric>
+#include <unordered_set>
+#include <util/arith_tools.h>


💡 I've seen empty lines in other files between STL includes and includes of files from the same project. The coding standard doesn't say anything about this other than the first dependency being the header file for this .cpp file though...
⚒️ It looks like the only necessary includes here are

#include "string_dependencies.h" #include <unordered_set> #include <util/expr_iterator.h> #include <util/graph.h> #include <util/make_unique.h> #include <util/ssa_expr.h>

antlechner · 2019-05-23T14:36:00Z

src/solvers/strings/string_refinement.h

@@ -27,6 +27,7 @@ Author: Alberto Griggio, [email protected]

 #include "string_constraint.h"
 #include "string_constraint_generator.h"
+#include "string_dependencies.h"


⛏️ Could forward declare string_dependenciest instead of including this file.

allredj · 2019-05-24T12:53:00Z

@antlechner @romainbrenguier I cleaned up the imports.

allredj

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

peterschrammel · 2019-05-24T15:05:24Z

src/solvers/strings/string_dependencies.h

+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H


doxygen \file is missing.

@peterschrammel Is that really useful? The class is already documented.

I would only repeat the description.

@allredj, please check whether it generates an entry next to the file here: http://cprover.diffblue.com/files.html

Indeed there's no description on the file view. I added a file documentation for this file.

tautschnig · 2019-05-30T08:11:03Z

@allredj Please rebase now that #4729 is in to make CI happy.

Because we can.

allredj

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

allredj added the cleanup label May 22, 2019

allredj requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, romainbrenguier, smowton and tautschnig as code owners May 22, 2019 16:05

allredj force-pushed the clean-up/extract-string-dependencies branch from 2b709f6 to 2096197 Compare May 22, 2019 16:13

allredj requested a review from antlechner May 22, 2019 16:21

allredj force-pushed the clean-up/extract-string-dependencies branch 3 times, most recently from 15f36b6 to 2fdc6f3 Compare May 23, 2019 08:50

allredj commented May 23, 2019

View reviewed changes

romainbrenguier approved these changes May 23, 2019

View reviewed changes

antlechner approved these changes May 23, 2019

View reviewed changes

antlechner reviewed May 23, 2019

View reviewed changes

allredj force-pushed the clean-up/extract-string-dependencies branch from 2fdc6f3 to 9e0b64f Compare May 24, 2019 12:44

allredj commented May 24, 2019

View reviewed changes

peterschrammel approved these changes May 24, 2019

View reviewed changes

peterschrammel assigned allredj May 24, 2019

allredj force-pushed the clean-up/extract-string-dependencies branch from 9e0b64f to 9b48bc5 Compare May 28, 2019 16:00

tautschnig added the Needs rebase label May 30, 2019

Joel Allred added 2 commits May 30, 2019 09:15

Extract string_dependencies into its own files

d376254

Because we can.

Remove now redundant import

b2bdda5

allredj force-pushed the clean-up/extract-string-dependencies branch from 9b48bc5 to b2bdda5 Compare May 30, 2019 08:16

tautschnig removed the Needs rebase label May 30, 2019

allredj commented May 30, 2019

View reviewed changes

allredj merged commit 3f9d063 into diffblue:develop May 30, 2019

allredj deleted the clean-up/extract-string-dependencies branch May 30, 2019 12:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Extract string dependencies into its own files #4695

Extract string dependencies into its own files #4695

allredj commented May 22, 2019

allredj commented May 23, 2019

allredj left a comment

allredj left a comment

romainbrenguier May 23, 2019

romainbrenguier May 23, 2019

antlechner May 23, 2019

antlechner May 23, 2019

allredj May 24, 2019

antlechner May 23, 2019

antlechner May 23, 2019

antlechner May 23, 2019

allredj commented May 24, 2019

allredj left a comment

peterschrammel May 24, 2019

allredj May 24, 2019

allredj May 24, 2019

peterschrammel May 28, 2019

allredj May 28, 2019

tautschnig commented May 30, 2019

allredj left a comment


		\*******************************************************************/

		#ifndef CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H

Extract string dependencies into its own files #4695

Extract string dependencies into its own files #4695

Conversation

allredj commented May 22, 2019

allredj commented May 23, 2019

allredj left a comment

Choose a reason for hiding this comment

allredj left a 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 commented May 24, 2019

allredj left a 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

tautschnig commented May 30, 2019

allredj left a comment

Choose a reason for hiding this comment