String refine preprocessing #378

romainbrenguier · 2016-12-31T12:33:41Z

Preprocessing of goto-programs for the string refinement.
This pull request includes the changes from ~~#374~~ ~~#549~~(merged) which should be merged before.

smowton

Broadly looks good, three main flavours of change to make:

(1) Some possible factoring in preprocess to consider
(2) Run cpplint.py to find code style problems
(3) Add commentary / function block comments to explain the reasoning behind some of the less-obvious code.

Regarding (3), cpplint.py will demand that you include a full docblock for every one of axioms_for_concat and axioms_for_substring and .... However I suspect if you consult with @forejtv / @peterschrammel they might be willing to accept a docblock for the /family/ of functions rather than lots of tedious repetition.

smowton · 2017-01-16T11:12:26Z

src/goto-programs/string_refine_preprocess.cpp

+#include <util/prefix.h>
+#include <solvers/refinement/string_expr.h>
+
+symbol_exprt string_refine_preprocesst::new_tmp_symbol


Unify this with java_bytecode/java_bytecode_convert_method.cpp::tmp_variable

smowton · 2017-01-16T11:17:27Z

src/goto-programs/string_refine_preprocess.cpp

+  i_it->code=assignment;
+}
+
+void string_refine_preprocesst::make_string_function_side_effect


Can you factor these three nearly-identical functions?

smowton · 2017-01-16T11:18:00Z

src/goto-programs/string_refine_preprocess.cpp

+    debug() << "string_refine_preprocesst::make_to_char_array_function"
+            << "got nil object_size" << eom;
+
+  auto location = function_call.source_location();


Code style -- use cpplint.py

smowton · 2017-01-16T11:19:37Z

src/goto-programs/string_refine_preprocess.cpp

+  side_effect_exprt data_cpp_new_expr(ID_cpp_new_array, data.type());
+  data_cpp_new_expr.set(ID_size, length);
+  symbol_exprt tmp_data=
+    new_tmp_symbol("tmp_data", struct_type.components()[2].type());


To help people reading generated VCCs, give this a more descriptive name

smowton · 2017-01-16T11:20:34Z

src/goto-programs/string_refine_preprocess.cpp

+
+  // tmp_assign = MALLOC(struct java::array[reference],sizeof(s))
+  symbol_exprt tmp_assign =
+    new_tmp_symbol("tmp_assign", pointer_typet(object_type));


Again, descriptive name would be good

smowton · 2017-01-16T11:58:40Z

src/solvers/refinement/string_refinement.cpp

+}
+
+
+exprt string_refinementt::sum_of_map(std::map<exprt, int> & m, bool negated)


Comment on what this function does / what it's purpose is, and consider a more descriptive name

smowton · 2017-01-16T11:59:09Z

src/solvers/refinement/string_refinement.cpp

+  return plus_exprt(sum, index_const);
+}
+
+exprt string_refinementt::simplify_sum(const exprt &f)


Comment on what sort of simplification this can do

smowton · 2017-01-16T12:00:35Z

src/solvers/refinement/string_refinement.cpp

+  return sum_of_map(map);
+}
+
+exprt string_refinementt::compute_subst


What does this do? Subst...itution, I guess? But from what, to what? Looking below, I guess this could be renamed "instantiate_quanfitier" or "substitute_quantifier" or similar? What is f for?

smowton · 2017-01-16T12:01:17Z

src/solvers/refinement/string_refinement.cpp

+(const exprt &qvar, const exprt &val, const exprt &f)
+{
+  exprt positive, negative;
+  // number of time the element should be added (can be negative)


This comment should make sense in context of a block comment up top, to tell us what 'the element' is, and what it's being added to, and so on

smowton · 2017-01-16T12:05:47Z

src/solvers/refinement/string_refinement.cpp

+      }
+      else
+      {
+        // otherwise we add k-1


Explain, here or somewhere else, what's happening here-- will this be called repeatedly to decrement the quantifier towards its lower bound, or is this a one-shot instantiate-with-upper-bound-minus-one?

peterschrammel

I've only looked over the first part of it. My comments apply to the whole PR, though. I'll review again once it has been rebased and cleaned up.

peterschrammel · 2017-02-05T13:42:26Z

src/goto-programs/string_refine_preprocess.cpp

+  const std::string &name, const typet &type)
+{
+  auxiliary_symbolt tmp_symbol;
+  // TODO: add a prefix to the name to avoid clashing with other


Please do that.

peterschrammel · 2017-02-05T13:45:11Z

src/goto-programs/string_refine_preprocess.cpp

+  goto_functions.function_map[function_name];
+}
+
+static bool is_java_string_type(const typet& type)


Make it a static class member.
These are candidates to go into a util class at some point.

Actually it is already declared here https://github.com/diffblue/cbmc/blob/master/src/solvers/refinement/refined_string_type.h#L64 so I'm going to use this one for now, but yes it could be moved

peterschrammel · 2017-02-05T14:05:33Z

src/goto-programs/string_refine_preprocess.cpp

+  // variables of the program
+  std::ostringstream buf;
+  buf << prefix << "_" << (next_symbol_id++);
+  std::string name = buf.str();


peterschrammel · 2017-02-05T14:06:02Z

src/goto-programs/string_refine_preprocess.cpp

+    return false;
+}
+
+static bool is_java_string_pointer_type(const typet& type)


function comment block missing

peterschrammel · 2017-02-05T14:06:43Z

src/goto-programs/string_refine_preprocess.cpp

+      symbol_exprt("java::java.lang.String", string_typet());
+    // TODO: we should use a function which is not currently in the code base
+    // to get the class identifier in this way:
+    // get_class_identifier_field(in, symbol_typet("java::java.lang.Object"), ns);


Is here:
https://github.com/diffblue/cbmc/blob/master/src/goto-programs/class_identifier.h

changed this here 918d97a

peterschrammel · 2017-02-05T14:30:19Z

src/goto-programs/string_refine_preprocess.cpp

+  assert(ns.follow(object_type).id() == ID_struct);
+  const struct_typet &struct_type=to_struct_type(object_type);
+  typet length_type, data_type;
+  for(unsigned i=0; i < struct_type.components().size(); i++)


use a ranged for

peterschrammel · 2017-02-05T14:31:05Z

src/goto-programs/string_refine_preprocess.cpp

+    else if(struct_type.components()[i].get_name() == "data")
+      data_type=struct_type.components()[i].type();
+
+  std::string fnamel=std::string(function_name.c_str()) + "_length";


use id2string

peterschrammel · 2017-02-05T14:33:08Z

src/goto-programs/string_refine_preprocess.cpp

+  // TODO: there should be a way defined in refined_string_type to access
+  // the array element
+  exprt rhs_data=member_exprt(arg, "content", data_type.subtype());
+  //exprt rhs_data=member_exprt(arg, "data", data_type.subtype());


code commented out? Fix, remove or use #if 0 and explain why

peterschrammel · 2017-02-05T14:33:42Z

src/goto-programs/string_refine_preprocess.cpp

+  if(lhs.id()==ID_typecast)
+    lhs=to_typecast_expr(lhs).op();
+
+#if 0


why is this code commented out?

peterschrammel · 2017-02-05T14:35:28Z

src/goto-programs/string_refine_preprocess.cpp

+
+ Purpose: at the given position replace `r = some_function(arr,...)` by
+          `r = function_name(arr.length, arr.data, ...)`
+          TODO: document what exactly do the two options


Please do so

peterschrammel · 2017-02-10T22:45:38Z

src/goto-programs/string_refine_preprocess.cpp

+#include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+#include <goto-programs/class_identifier.h>
+#include <solvers/refinement/string_expr.h>


Strictly speaking, this is forbidden. This would introduce a dependency of goto-programs on solvers. So, the immediate guess is that string_expr.h should go into util/. However, this contains dependencies to solvers and java_bytecode, which I don't understand why they are needed. In my opinion. string_expr.h should be language-independent and be moved into util/: for this to happen, the includes bv_refinement.h (seems obsolete) and refined_string_type.h must be removed. The function to_refined_string_type should be defined in refined_string_type.h in the style of similar functions in std_expr.h.

Note: Investigating all these unwanted dependencies, I noticed that solvers depends on ansi-c (in qbf and flattening) and also on java_bytecode (in the string solver), which is not "clean". Also, goto-programs has dependencies on ansi-c, which should not be the case if we take the view of a goto-program being language-independent. All this is related to our multi-language facilities requiring some refactoring.

@peterschrammel would you mind opening an issue to track those (undesirable) dependencies? I'm aware of some of them, but as you have done a proper investigation it would be great if you could note down the details of your findings so that we can all work on them. Thanks!!

string_expr.h could be moved to util but we need refined_string_type.h (this is the type of string_exprt, and maybe these should be renamed to make that obvious). To avoid dependencies on java_bytecode and such, some static of methods of refined_string_type should be moved out of this class to more appropriate places.

@peterschrammel do you prefer to have these changes (on string_expr and refined_string_type) in this pull request or should it be a new one?

peterschrammel · 2017-02-10T22:52:35Z

src/goto-programs/string_refine_preprocess.cpp

+symbol_exprt string_refine_preprocesst::new_tmp_symbol(
+  const std::string &prefix, const typet &type)
+{
+  auxiliary_symbolt tmp_symbol;


Consider using #523 (once it has been merged) for adding fresh variables.

peterschrammel · 2017-02-10T22:53:15Z

src/goto-programs/string_refine_preprocess.cpp

+  assert(ns.follow(object_type).id() == ID_struct);
+  const struct_typet &struct_type=to_struct_type(object_type);
+  for(unsigned i=0; i<struct_type.components().size(); i++)
+    if(struct_type.components()[i].get_name() == "length")


cpplint (check whole file)

I didn't get any error from cpplint on this file

peterschrammel · 2017-02-10T22:53:42Z

src/goto-programs/string_refine_preprocess.cpp

+
+/*******************************************************************\
+
+Function: string_refine_preprocesst::insert_assignements


assignments (check whole file)

peterschrammel · 2017-02-10T22:53:58Z

src/goto-programs/string_refine_preprocess.cpp

+  typet length_type, data_type;
+  get_data_and_length_type_of_string(deref, data_type, length_type);
+
+  std::string fnamel=id2string(function_name) + "_length";


peterschrammel · 2017-02-10T22:55:38Z

src/goto-programs/string_refine_preprocess.cpp

+{
+  exprt::operandst new_arguments;
+
+  for(unsigned i=0; i<arguments.size(); i++)


std::size_t

peterschrammel · 2017-02-10T22:56:01Z

src/goto-programs/string_refine_preprocess.cpp

+  const irep_idt &function_id)
+{
+  auto it=signatures.find(function_id);
+  if(it != signatures.end())


peterschrammel · 2017-02-10T23:09:59Z

Looks much cleaner now. Please squash the commits when finalising.

tautschnig · 2017-02-11T07:14:17Z

src/goto-programs/string_refine_preprocess.cpp

+
+\*******************************************************************/
+
+#include "string_refine_preprocess.h"


Nit picking: most files place the include of the class-specific header as the last #include (I can't argue this is good or bad).

tautschnig · 2017-02-11T07:14:22Z

src/goto-programs/string_refine_preprocess.cpp

+\*******************************************************************/
+
+symbol_exprt string_refine_preprocesst::new_tmp_symbol(
+  const std::string &prefix, const typet &type)


I would suggest to use the facilities from #523 (which implies that #523 should get merged asap).

I added a TODO note there, in case this PR is merged before

It seems some poking and pushing on #523 is required...

tautschnig · 2017-02-11T07:14:26Z

src/goto-programs/string_refine_preprocess.cpp

+{
+  symbolt tmp_symbol;
+  std::ostringstream buf;
+  buf << "string_preprocess" << (next_symbol_id++) << "#" << prefix;


The use of #' as separator may be dangerous as it is used in the SSA encoding. Code shouldn't be doing this, but may be relying only a single #' to exist...

I used $ instead (8196d90), it seems that's what #523 uses

tautschnig · 2017-02-11T07:14:30Z

src/goto-programs/string_refine_preprocess.cpp

+  tmp_symbol.name=name;
+  tmp_symbol.type=type;
+  symbol_table.add(tmp_symbol);
+  return symbol_exprt(name, type);


return tmp_symbol.symbol_expr();

tautschnig · 2017-02-11T07:14:33Z

src/goto-programs/string_refine_preprocess.cpp

+  auxiliary_symbolt func_symbol;
+  func_symbol.base_name=function_name;
+  func_symbol.is_static_lifetime=false;
+  func_symbol.mode=ID_java;


Hardcoding ID_java looks scary to me. Why does that work? (Though, in fact, it might as well just not matter.)

As mentioned in the next comment, this preprocessing functions are only for Java, so that's why there shouldn't be any problem there.

If this is Java only, shouldn't all the files go in the java_bytecode folder? Language-specific parts should be as clearly separated from generic ones as possible.

From the point of view of dependencies, we need goto-programs but not anything from java_bytecode. If code in java_bytecode is allowed to use things from goto-programs then yes we could move it there, but I'm not sure it's the case. Maybe @peterschrammel has an opinion on this?

How is this code being invoked, i.e., where is the call that says "now let's do string preprocessing"? That might help to understand where it fits best.

Invocation of the preprocessing is not part of this pull request but of this one: #429 (in particular here: https://github.com/diffblue/cbmc/pull/429/files#diff-41db988013f70caad45ce489749c7df6R921)
This is because the original pull request was too big and thus was split into several parts.

Thanks a lot for the pointer (I was aware it had been split out, but couldn't find it on the spot)! This certainly suggests that goto-programs is the right place, and that one should rather think about how to make this extensible to other languages? (Which does not imply any request to do so right away, but just bringing up the thought and possibly placing some TODO notes.)

tautschnig · 2017-02-11T07:15:38Z

src/goto-programs/string_refine_preprocess.cpp

+void string_refine_preprocesst::initialize_string_function_table()
+{
+  string_functions
+    [irep_idt("java::java.lang.String.codePointAt:(I)I")]=


The explicit use of irep_idt should not be necessary.

tautschnig · 2017-02-11T07:16:28Z

src/goto-programs/string_refine_preprocess.cpp

+{
+  string_functions
+    [irep_idt("java::java.lang.String.codePointAt:(I)I")]=
+    ID_cprover_string_code_point_at_func;


With C++11 you should be able to initialize that map using { { id, value}, {id, value} , ... } as a more concise syntax.

It seems like it works for maps but not unordered maps

tautschnig · 2017-02-11T07:16:38Z

src/goto-programs/string_refine_preprocess.h

+
+  // String builders maps the different names of a same StringBuilder object
+  // to a unique expression.
+  std::map<exprt, exprt> string_builders;


Shouldn't that be a std::unordered_map?

tautschnig · 2017-02-11T07:16:43Z

src/goto-programs/string_refine_preprocess.h

+  std::map<irep_idt, irep_idt> string_function_calls;
+  std::map<irep_idt, irep_idt> string_of_char_array_functions;
+  std::map<irep_idt, irep_idt> string_of_char_array_function_calls;
+  std::map<irep_idt, irep_idt> side_effect_char_array_functions;


Likely these should be std::unordered_map as well

tautschnig · 2017-02-11T07:16:45Z

src/goto-programs/string_refine_preprocess.h

+
+  std::map<irep_idt, std::string> signatures;
+  std::map<exprt, exprt> hidden_strings;
+  std::map<exprt, exprt> java_to_cprover_strings;


As above: std::unordered_map

romainbrenguier · 2017-02-15T14:49:55Z

I squashed the commits, but this now depends on #549 which moves string_exprt to util

peterschrammel · 2017-03-09T18:59:32Z

src/goto-programs/string_refine_preprocess.cpp

+  const std::string &signature)
+{
+  if(function_name==ID_cprover_string_copy_func)
+    make_string_copy(goto_program, i_it, lhs, arguments[0], location);


are sure there is an argument?

peterschrammel · 2017-03-09T19:00:46Z

src/goto-programs/string_refine_preprocess.cpp

+  goto_programt::targett &i_it,
+  const std::list<code_assignt> &va)
+{
+  auto i=va.begin();


are you sure the list is not empty?

tautschnig · 2017-03-10T19:05:16Z

src/goto-programs/string_refine_preprocess.cpp

+\*******************************************************************/
+
+symbol_exprt string_refine_preprocesst::new_tmp_symbol(
+  const std::string &prefix, const typet &type)


It seems some poking and pushing on #523 is required...

tautschnig · 2017-03-10T19:05:24Z

src/goto-programs/string_refine_preprocess.cpp

+  auxiliary_symbolt func_symbol;
+  func_symbol.base_name=function_name;
+  func_symbol.is_static_lifetime=false;
+  func_symbol.mode=ID_java;


If this is Java only, shouldn't all the files go in the java_bytecode folder? Language-specific parts should be as clearly separated from generic ones as possible.

tautschnig · 2017-03-10T19:05:48Z

src/goto-programs/string_refine_preprocess.cpp

+    if(i_it->is_function_call())
+    {
+      code_function_callt &function_call=to_code_function_call(i_it->code);
+      for(auto arg : function_call.arguments())


const auto &arg

this particular one cannot be made const as we modify it

Oh, I'm sorry, but not knowing the precise rules for auto just yet: are you sure you end up with a reference and not with a copy? In the latter case you can obviously modify it, but it won't have much of an effect... I'd suggest auto &arg to be on the safe side.

tautschnig · 2017-03-10T19:05:54Z

src/goto-programs/string_refine_preprocess.cpp

+  assert(is_java_string_type(expr.type()) ||
+         is_java_string_builder_type(expr.type()));
+  typet object_type=ns.follow(expr.type());
+  assert(object_type.id()==ID_struct);


This assertion is covered by the subsequent to_struct_type

tautschnig · 2017-03-10T19:05:56Z

src/goto-programs/string_refine_preprocess.cpp

+  typet object_type=ns.follow(expr.type());
+  assert(object_type.id()==ID_struct);
+  const struct_typet &struct_type=to_struct_type(object_type);
+  for(auto component : struct_type.components())


const auto &component

tautschnig · 2017-03-10T19:06:00Z

src/goto-programs/string_refine_preprocess.cpp

+
+exprt string_refine_preprocesst::make_cprover_string_assign(
+  goto_programt &goto_program,
+  goto_programt::targett &i_it,


Would it be possible to find a more descriptive name for this parameter?

tautschnig · 2017-03-10T19:06:02Z

src/goto-programs/string_refine_preprocess.cpp

+  i_it->code=*i;
+  for(i++; i!=va.end(); i++)
+  {
+    i_it=goto_program.insert_after(i_it);


neither source_location nor function is properly set for these newly inserted instructions

tautschnig · 2017-03-10T19:06:04Z

src/goto-programs/string_refine_preprocess.cpp

+
+  if(object_size.is_nil())
+    debug() << "string_refine_preprocesst::make_string_assign "
+            << "got nil object_size" << eom;


Is it nevertheless ok to continue?

tautschnig · 2017-03-14T15:18:59Z

From my point of view #523 is the main blocker here. (Actually, the only one, for me.)

romainbrenguier · 2017-03-15T16:51:26Z

Now that #523 is merged, I rebased and used this function to declare fresh array and strings. See the commit f14f165

tautschnig · 2017-03-15T17:20:00Z

src/util/std_expr.h

+
+  function_application_exprt(
+    const symbol_exprt &_function, const typet &_type):
+      function_application_exprt(_type)


Please add // NOLINT(runtime/explicit) to this line to silence the linter on this invocation of the constructor from the two-parameter one.

peterschrammel

This looks ready to go after some minor polishing

peterschrammel · 2017-03-16T08:12:13Z

src/goto-programs/string_refine_preprocess.cpp

+{
+  if(function_name==ID_cprover_string_copy_func)
+  {
+    assert(arguments.size()>0);


peterschrammel · 2017-03-16T08:13:14Z

src/goto-programs/string_refine_preprocess.cpp

+  function_application_exprt rhs;
+  std::vector<exprt> args;
+  if(assign_first_arg)
+    rhs.type()=function_call.arguments()[0].type();


assert !arguments().empty()

peterschrammel · 2017-03-16T08:14:01Z

src/goto-programs/string_refine_preprocess.cpp

+
+  exprt lhs;
+  if(assign_first_arg)
+    lhs=function_call.arguments()[0];


assert !arguments().empty()

peterschrammel · 2017-03-16T08:14:11Z

src/goto-programs/string_refine_preprocess.cpp

+  const std::string &signature)
+{
+  const code_function_callt function_call=to_code_function_call(target->code);
+  string_builders[function_call.lhs()]=function_call.arguments()[0];


assert !arguments().empty()

peterschrammel · 2017-03-16T08:17:03Z

src/goto-programs/string_refine_preprocess.cpp

+{
+  const code_function_callt &function_call=to_code_function_call(target->code);
+
+  assert(function_call.arguments().size()>=1);


peterschrammel · 2017-03-16T08:17:36Z

src/goto-programs/string_refine_preprocess.cpp

+  make_char_array_function(
+    goto_program, target, function_name, signature, 1, true, false);
+  code_function_callt &function_call=to_code_function_call(target->code);
+  string_builders[function_call.lhs()]=function_call.arguments()[0];


assert !arguments().empty()

peterschrammel · 2017-03-16T08:19:21Z

src/goto-programs/string_refine_preprocess.cpp

+  auto it=signatures.find(function_id);
+  if(it!=signatures.end())
+    return it->second;
+  else return "";


return on next line

peterschrammel · 2017-03-16T08:20:52Z

src/goto-programs/string_refine_preprocess.cpp

+    const typet &subtype=pt.subtype();
+    if(subtype.id()==ID_struct)
+    {
+      irep_idt tag=to_struct_type(subtype).get_tag();


could use const & here

peterschrammel · 2017-03-16T08:21:19Z

src/goto-programs/string_refine_preprocess.cpp

+  }
+  else if(type.id()==ID_struct)
+  {
+    irep_idt tag=to_struct_type(type).get_tag();


could use const & here

peterschrammel · 2017-03-16T08:21:30Z

src/goto-programs/string_refine_preprocess.cpp

+{
+  if(type.id()==ID_symbol)
+  {
+    irep_idt tag=to_symbol_type(type).get_identifier();


could use const & here

This avoid dependencies between goto-programs and solver. We also removed function is_unrefined_string_type which should not be needed in the string solver. Removed also mention of java string types and unrefined types in the solver. These mentions should not be necessary, since we are not supposed to do anything java specific. The solver should only have to deal with refined string types and possibly char arrays.

This is a more appropriate location for this module since it's used both in the preprocessing of goto-programs and the string solver.

Refined string type should be used instead as we are trying to be language independent.

peterschrammel

Looks good to me now.

kroening · 2017-04-04T12:23:54Z

Why did refined_string_type.h move into util/?

romainbrenguier · 2017-04-06T14:33:38Z

@kroening the refined_string_typet class is used both in the preprocessing of goto-program and the string-solver when the --refine-strings option is activated. Moving it to util avoids dependencies between goto-programs and solvers

romainbrenguier · 2017-06-28T16:53:31Z

I'm closing this PR which is obsolete compared to what is in the test-gen-support branch

67c80fc Merge pull request diffblue#394 from diffblue/jeannie/LinkedHashMapIterators 6667484 Tests that the iteration order is correct. 38301ea Tests other methods and constructor in LinkedHashMap f795b3d Models other methods in LinkedHashMap. 25773a6 Tests entrySet(), keySet() and values() in LinkedHashMap ee8cfad Models keySet(), entrySet() and values() in LinkedHashMap. 02c8271 Merge pull request diffblue#393 from diffblue/jeannie/UpdateReadMeForSpec 81460d3 Update readme.md to include new style for specs 9efcce3 Merge pull request diffblue#396 from diffblue/antonia/clean-up-for-TG-1081 c902c03 Merge pull request diffblue#397 from diffblue/jeannie/ForgotAppendObjectDocs 772a977 Merge pull request diffblue#390 from diffblue/antonia/enable-fixed-tests 5bef2ff Merge pull request diffblue#398 from diffblue/antonia/ticket-references-bugfix ed1dca2 Merge pull request diffblue#395 from diffblue/allredj/disable-tests-failing-on-tg2717 c07841d Add more tests for String.getBytes(Charset) d568e47 Fix array index bug in String.getBytesUTF_16 2218407 Model String.getBytes(Charset) 9c3a8bc Clarify difference of String.getBytes from JDK cf1c23b Merge the two active scenarios in String.spec dd5d2d9 Remove support_v1 tag from String specs 5f9a7e1 Split String tests into Level 0 and Level 1+ f2877b9 Enable Class test that was blocked by TG-1081 034f3e0 Remove reference to TG-1081 from File model 43afde7 Force static initialiser for File model d95ff9e Remove reference to fixed bug from Date model 0807806 Remove references to fixed bugs from Arrays model cde4085 Remove references to fixed bugs from HashMap model d85fe5b Update RaceTimes references to TG-1404 and TG-1523 0e925e5 Update ticket number in HashMap.spec 03a5186 Enable TG-1404 tests fa051dd Delete ArrayList CustomType test file b0e853b Enable HashMap test previously blocked by TG-1877 44bfe0a Merge pull request diffblue#392 from diffblue/lajw/TG-2389-enable-tests 595dd5d Changes CProver helped methods in HashMap to protected. c52771c Merge pull request diffblue#385 from diffblue/jeannie/UpdateTestRunner de0abdc Enable tests fixed by recent test-gen fixes b64357a Remove ticket numbers from resolved bugfix tests 53eca00 Documents StringBuilder and StringBuffer append(Object) baec23f Merge pull request diffblue#389 from diffblue/antonia/enable-TG-2666-test b2f0258 Enable LinkedList test that was blocked by TG-2666 57e79e5 Add knownbug tests for TG-2717 80fa433 Merge pull request diffblue#387 from diffblue/forejtv/unsupportedcharsetexception 990129c Merge pull request diffblue#391 from diffblue/allredj/disable-html-report 97f32f6 Don't write to the Html report 4cb5996 Merge pull request diffblue#382 from diffblue/antonia/address-ArrayList-todos 6749702 Merge pull request diffblue#386 from diffblue/antonia/gauge-telemetry-off 546dfdc Move legacy style tests into main Gauge step 5be886f Mark UnsupportedCharsetException as untested 1c17838 Add regression test for side effects 8c836ab Add tests for ArrayLists w. (non-default) capacity 34a141d Address bugfix TODOs in ArrayList 563b631 Correct bug description in comment 3e7603d Merge pull request diffblue#383 from diffblue/antonia/reformat-HashSet-tests 5d4e013 [TG-2751] Added UnsupportedCharsetException 11b28fb Reformat HashSet.spec f77c3c4 Rename HashSet_L2.spec to HashSet_L0.spec a16a1e7 Move all HashSet Maven tests into HashSet.spec f21a2da Merge pull request diffblue#376 from diffblue/jeannie/LinkedHashMap 820c5f7 Merge pull request diffblue#380 from diffblue/jeannie/AppendObject af65f4d Tests java.lang.StringBuffer append(Object) a554517 Reformat tests in java.util.StringBuilder dd6d3f6 Models append(Object) for StringBuilder and StringBuffer. 8920399 Tests toString() methods on existing models where possible 647f4fe Tests toString() methods on existing models where possible 978273b Documents and implements toString() methods in existing models. 78020ee Documents java.util.LinkedHashMap fb0cf92 Tests java.util.LinkedHashMap 7a9df4e Models java.util.LinkedHashMap 5a8af60 Marks all methods as notModelled() for java.util.LinkedHashMap 8d6b149 Initial commit for java.util.LinkedHashMap 34b7c54 Merge pull request diffblue#359 from diffblue/forejtv/throwable-no-static e2230de Cleanup of unused (mostly static) variables 255013e Merge pull request diffblue#384 from diffblue/jeannie/DisableBoundedGenericHashMap f374d5f Merge pull request diffblue#381 from diffblue/justin/TG2600-Correction ce6328b Turn off Gauge telemetry on Travis 6ab2864 Updates TestRunner.java to mimic platform parameters. 8ee75a4 Disables a HashMap test that depends on bounded generic type. 3677c3a [TG-2600] correct a mistake in the L1RemoveLast test 4511813 Merge pull request diffblue#378 from diffblue/antonia/LinkedList-first-model 6bda7ea Add tests for LinkedList b5d4cbe Model LinkedList methods specified in TG-2600 aa6e90a Empty models for new classes 3c25555 Copy LinkedList and related classes from jdk 5e4d410 Merge pull request diffblue#373 from diffblue/romain/tests/activate-arrays-hashset-test#TG-1404 a0d9289 Activate some Arrays test 27d06b4 Activate tests for Hashset fixed by TG-1404 224962a Merge pull request diffblue#371 from diffblue/romain/tests/activate-after-fix-1404 ed26b28 Activate level 2 tests fixed by TG-1404 b59c1e9 Relabel known-bug for Level2 HashMap test 5c0041b Activate tests for HashMap.values fixed by TG-1404 2777872 Activate tests for HashMap.entrySet 50d3f2c Activate tests for HashMap.keySet fixed by TG-1404 6146215 Activate ArrayList test fixed by TG-1404 bc09fd7 Merge pull request diffblue#365 from diffblue/jeannie/getTimeZone 29cf7e0 Merge pull request diffblue#372 from diffblue/forejtv/bump-up-gauge-v bdd500a Change Gauge Java Maven Plugin to 0.6.6 190aa18 Tests java.util.TimeZone 170a992 Documents java.util.TimeZone in javadocs 9e52664 Models java.util.TimeZone constructor, getID, setID and getTimeZone. eac578e Tests sun.util.calendar.ZoneInfo b4be728 Documents sun.util.calendar.ZoneInfo in javadocs e5ffa98 Models the sun.util.calendar.ZoneInfo constructor and getTimeZone() 6d704ad Marks methods as notModelled() for sun.util.calendar.ZoneInfo d249adb Marks methods as notModelled() for java.util.TimeZone 7f71d8d Initial commit for sun.util.calendar.ZoneInfo. b53d9c1 Initial commit for java.util.TimeZone 056aad2 Merge pull request diffblue#368 from diffblue/allredj/fix-hashtable-spec 8848414 Merge pull request diffblue#370 from diffblue/allredj/stringbuffer-spec-small-correction 1d947e5 Small correction to StringBuffer spec file 42f1a93 Fix typo in hashtable spec file git-subtree-dir: benchmarks/LIBRARIES/models git-subtree-split: 67c80fcdcf82418b5e7099ae63dec3360b153f90

…resco-readme Update readme for installing Alfresco

romainbrenguier mentioned this pull request Dec 31, 2016

String solver #341

Closed

peterschrammel requested a review from smowton January 12, 2017 12:39

romainbrenguier mentioned this pull request Jan 12, 2017

String refine option #429

Closed

smowton suggested changes Jan 16, 2017

View reviewed changes

romainbrenguier force-pushed the string-refine-preprocessing branch 2 times, most recently from 9b1e639 to f5a6cfd Compare January 17, 2017 10:52

romainbrenguier force-pushed the string-refine-preprocessing branch 6 times, most recently from 0625ef1 to b69129b Compare February 2, 2017 10:34

romainbrenguier force-pushed the string-refine-preprocessing branch from b69129b to ff66780 Compare February 2, 2017 15:18

peterschrammel added the String solver label Feb 2, 2017

romainbrenguier force-pushed the string-refine-preprocessing branch from 4c26c59 to 2cd801d Compare February 3, 2017 09:09

peterschrammel requested changes Feb 5, 2017

View reviewed changes

romainbrenguier force-pushed the string-refine-preprocessing branch 6 times, most recently from 334ac5f to 3fd299a Compare February 10, 2017 12:51

peterschrammel reviewed Feb 10, 2017

View reviewed changes

tautschnig requested changes Feb 11, 2017

View reviewed changes

tautschnig assigned romainbrenguier Feb 13, 2017

romainbrenguier force-pushed the string-refine-preprocessing branch 3 times, most recently from 3af4fb8 to d35d9ca Compare February 15, 2017 14:48

forejtv unassigned romainbrenguier Mar 6, 2017

peterschrammel reviewed Mar 9, 2017

View reviewed changes

tautschnig reviewed Mar 10, 2017

View reviewed changes

romainbrenguier force-pushed the string-refine-preprocessing branch from 7aea419 to f14f165 Compare March 15, 2017 16:44

tautschnig requested changes Mar 15, 2017

View reviewed changes

peterschrammel requested changes Mar 16, 2017

View reviewed changes

allredj mentioned this pull request Mar 16, 2017

Corrections to the string solver - 2 #646

Closed

romainbrenguier force-pushed the string-refine-preprocessing branch from c404cd1 to ff69281 Compare March 17, 2017 17:26

romainbrenguier added 5 commits March 17, 2017 22:37

Preprocessing of goto programs for string refinement

1aede78

Moving refined_string_type to util

70af9ce

This is a more appropriate location for this module since it's used both in the preprocessing of goto-programs and the string solver.

Removed distinction between c string type and refined string type

2929d7f

Removed mention of c string type

5cb0e5e

Refined string type should be used instead as we are trying to be language independent.

romainbrenguier force-pushed the string-refine-preprocessing branch from ff69281 to 5cb0e5e Compare March 17, 2017 22:41

peterschrammel approved these changes Mar 18, 2017

View reviewed changes

peterschrammel assigned kroening and unassigned peterschrammel Mar 18, 2017

tautschnig approved these changes Mar 20, 2017

View reviewed changes

tautschnig removed their assignment Mar 20, 2017

peterschrammel mentioned this pull request Mar 21, 2017

String refine preprocessing #669

Merged

romainbrenguier added the do not merge label Jun 20, 2017

peterschrammel unassigned kroening Jun 25, 2017

romainbrenguier closed this Jun 28, 2017

smowton pushed a commit to smowton/cbmc that referenced this pull request May 9, 2018

Merge pull request diffblue#378 from diffblue/owen-jones-diffblue/alf…

65d0409

…resco-readme Update readme for installing Alfresco

		}


		exprt string_refinementt::sum_of_map(std::map<exprt, int> & m, bool negated)


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

		Function: string_refine_preprocesst::insert_assignements


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

		#include "string_refine_preprocess.h"

String refine preprocessing #378

String refine preprocessing #378

Uh oh!

Conversation

romainbrenguier commented Dec 31, 2016 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel commented Feb 10, 2017

romainbrenguier commented Dec 31, 2016 •

edited

Loading