Reorganise C parameter creation #767

owen-mc-diffblue · 2017-04-06T11:06:43Z

Make it match the java code more closely to prepare for (a) one day
merging them and (b) dealing with pointer parameters.

owen-mc-diffblue · 2017-04-06T11:07:36Z

Note that this patch makes one test fail: cbmc/unsigned__int128. I'll need help working out how to solve this problem. I paste below a description of the problem that I put on slack.

--

I am confused about the test cbmc/unsigned__int128. It works on master, but not with my patch. Here is my understanding of the test. The C function reduce() has two parameters. After following typedefs the second one (called in) is an array of 7 uint128_ts. It then assumes some things about the size of the elements of in and does some additions. CBMC is called with "--unsigned-overflow-check --signed-overflow-check" to check that it doesn't detect any overflow. (I'm not sure if we check that CBMC can detect overflow when there is actual overflow.)

If you look at the goto generated by CBMC on master, it sets the second argument to the function to be a null pointer, because it can't cope with pointers or arrays yet. I'm slightly surprised that it correctly checks some arithmetic involving in[0] when it thinks in is null rather than worrying about undefined behaviour, but I've confirmed that it does work: if I increase the numbers being added together then it does then decide there is integer overflow.

My patch makes CBMC generate code so it can cope with C function parameters which are pointers (or pointers to pointers, ...). I haven't explicitly done anything for arrays, but actually it thinks the array parameter is a pointer (I'm not sure how I can distinguish them), so it generates extra code for it which makes a nondet boolean and conditions on that to say that the argument is either null or it points to a temporary uint128_t variable (which it makes). Note that it creates a single uint128_t - in an ideal world it would create an array of 7 of them. Now the test fails, on all the lines involving in. I don't really understand why. It was happy to reason about integer overflow involving in[0] to in[6] when in was null, but not when in might be null or might point to a particular uint128_t.

tautschnig · 2017-04-06T12:38:24Z

I'd recommend changing the unsiged___int128 test to have unquestionable semantics:

--- a/regression/cbmc/unsigned___int128/main.c
+++ b/regression/cbmc/unsigned___int128/main.c
@@ -18,8 +18,10 @@ felem p = {0x1FFFFFFFFFFFFFF,
  * Reduce seven 128-bit coefficients to four 64-bit coefficients.
  * Requires in[i] < 2^126,
  * ensures out[0] < 2^56, out[1] < 2^56, out[2] < 2^56, out[3] <= 2^56 + 2^16 */
-void reduce(felem out, const widefelem in)
+void reduce()
 {
+    felem out;
+    const widefelem in;

     __CPROVER_assume(in[0]<(widelimb)((widelimb)1<<126));
     __CPROVER_assume(in[1]<((widelimb)1<<126));
diff --git a/regression/cbmc/unsigned___int128/test.desc b/regression/cbmc/unsigned___int128/test.desc
index 67b0294..aaeabeb 100644
--- a/regression/cbmc/unsigned___int128/test.desc
+++ b/regression/cbmc/unsigned___int128/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --unsigned-overflow-check --signed-overflow-check --function reduce
 ^EXIT=0$

Note the change to KNOWNBUG: the test actually does fail with current master when changed in this way. So there's an unrelated bug to be fixed.

tautschnig · 2017-04-06T14:06:09Z

@owen-jones-diffblue Brilliant, thank you for debugging and actually fixing the test!!!

Would you mind, however, placing this in a separate PR? I believe this should be merged ASAP (and it's really unrelated to your additional work).

owen-mc-diffblue · 2017-04-06T14:06:42Z

Yes, I'd just come to the same conclusion. I've made a separate PR. #771

tautschnig

This is a very nice piece of work, but I'd like to see some clarification on a number of questions.

tautschnig · 2017-04-06T14:08:04Z

src/ansi-c/ansi_c_entry_point.cpp

-
-    result[i]=symbol_expr;
-    i++;
+    const code_typet::parametert &p = parameters[param_number];


Nit picking: no whitespace around =

tautschnig · 2017-04-06T14:10:10Z

src/ansi-c/ansi_c_entry_point.cpp

+      init_code,
+      allow_null,
+      symbol_table,
+      p.source_location(),


This function has a large number of parameters, and seemingly at least 2 can be derived from the first one. Can this be simplified?

I was trying to keep it similar to object_factory() in src/java_bytecode/java_object_factory.cpp so that they can be easily combined in future. If it is preferable then I can instead simplify it and reduce the number of parameters.

This makes a lot of sense. I'm wondering whether the Java code should be refactored instead?

I looked into refactoring this aspect of the java code. object_factory() is used in two places in java_entry_point(): once in a loop over all the parameters of the function we are looking at, and once in a loop over all symbols in the symbol table which are static plus some other conditions, or which are string literals. Without knowing the code better it's not clear to me that I can reduce the number of parameters in a way which works in both places.

Ok, thanks for checking!

tautschnig · 2017-04-06T14:10:44Z

src/ansi-c/ansi_c_entry_point.cpp

+
+    main_arguments[param_number]=c_nondet_symbol_factory(
+      p,
+      param_number,


Why is the position of the parameter a required piece of information?

It is only used to construct a fallback base name which is used if the parameter doesn't have one. That is what the code did before I refactored it. Other options include passing in the fallback base name or trying to establish that the parameter will always have a base name.

Ok; I'm inclined to suggest that the name should be passed in (effectively as constructed in that function) as the problem can only arise at the top level, recursive calls would not suffer from that problem.

tautschnig · 2017-04-06T14:12:14Z

src/ansi-c/ansi_c_entry_point.cpp

+    input_recorder.record_input(
+      p_symbol.base_name,
+      main_arguments[param_number]);
+    input_recorder.declare_recorded_inputs(init_code);


The input recorder is passed as an argument to c_nondet_symbol_factory, but then there still is a need for an extra manual step. I think this should be simplified.

You are right. I have moved this entirely within c_nondet_symbol_factory().

tautschnig · 2017-04-06T14:12:58Z

src/ansi-c/ansi_c_entry_point.cpp

@@ -505,8 +481,11 @@ bool ansi_c_entry_point(
  else
  {
    // produce nondet arguments
-    call_main.arguments()=
-      build_function_environment(parameters, init_code, symbol_table);
+    call_main.arguments()=build_function_environment(


Nit pick: Preferably wrap lines after the = (applies elsewhere in your patch too).

I have added an argument (message_handler, to make it more like the java code), so it no longer fits into one line if I wrap after the =.

Ah, apologies for being unclear: also wrap after the = (and then indent the arguments by two additional spaces).

tautschnig · 2017-04-06T14:26:49Z

src/ansi-c/c_nondet_symbol_factory.cpp

+
+      code_ifthenelset null_check;
+      exprt null_return=
+        zero_initializer(returns_null_sym.type, loc, ns, message_handler);


You should be able to get away with from_integer(0, returns_null_sym.type), at which point you might not even need a message_handlert anymore.

tautschnig · 2017-04-06T14:29:46Z

src/ansi-c/c_nondet_symbol_factory.cpp

+    type,
+    prefix);
+
+  code_declt decl;


code declt decl(tmp_symbol.symbol_expr());

tautschnig · 2017-04-06T14:32:13Z

src/ansi-c/c_nondet_symbol_factory.cpp

+  symbol_exprt symbol_expr(identifier, type);
+
+  code_declt decl;
+  decl.symbol()=symbol_expr;


code_declt decl(symbol_expr);

tautschnig · 2017-04-06T14:33:16Z

src/ansi-c/c_nondet_symbol_factory.cpp

+      message_handler,
+      input_recorder);
+    state.gen_nondet_init(symbol_expr, loc);
+  }


Why just those to type classes?

I copied the java code. The pointer case seems to cover arrays and structs as well, though this patch doesn't properly deal with them.

tautschnig · 2017-04-06T14:35:28Z

src/ansi-c/c_nondet_symbol_factory.h

+  symbol_tablet &symbol_table,
+  const source_locationt &loc,
+  const typet &type,
+  const std::string &prefix="tmp");


The above appear to be helper functions that ought to be just marked static and not be exported via the header file either.

tautschnig

My main ask is about the high-level comment - I don't think I have yet understood the code being generated very well. It looks overly complicated to me, but I am likely missing something.

tautschnig · 2017-04-07T17:04:21Z

src/ansi-c/ansi_c_entry_point.cpp

-    i++;
+    const code_typet::parametert &p=parameters[param_number];
+
+    bool allow_null=true;


Is there a reason that this is placed in a local variable rather than passing true directly?

No, I guess it'll always be true here. I was thinking that when we add arrays and structs we'd need to have some logic to choose it, but I guess not at this level.

tautschnig · 2017-04-07T17:14:49Z

src/ansi-c/c_nondet_symbol_factory.cpp

+    if(!assume_non_null)
+    {
+      // Will generate the following code:
+      //   IF NONDET(_Bool) != FALSE THEN GOTO <set_null_label_str>


Thanks a lot for the detailed comments. Could you please add the overall code in one place to understand what's intended to happen here at high level?

I'll move them all into one place, rather than have them in one place and spread out.

tautschnig · 2017-04-07T17:16:04Z

src/ansi-c/c_nondet_symbol_factory.cpp

+    new_symbol.base_name=base_name;
+    new_symbol.type=type;
+
+    symbol_table.move(new_symbol);


Use symbol_table.add and make sure this symbol is actually new (add has a return value).

Done. I also wrote the function comments for symbol_table.add() and symbol_table.move(), which I'll put in a separate PR.

tautschnig · 2017-04-10T11:00:49Z

src/ansi-c/c_nondet_symbol_factory.cpp

+      //   <code generated by gen_nondet_init()>
+      //   GOTO <init_done_label_str>
+      //   <set_null_label_str>: <expr> = ((<pointer_type>)NULL);
+      //   <init_done_label_str>: SKIP


Thanks a lot for adding those comments! It seems the code here really mixes up two concepts (I understand that you've just copied this from the Java version): the code is being generated as if in the GOTO intermediate level, but it's being done using high-level language constructs. There does not seem to be any need for labels or gotos here. Just generate a code_ifthenelse with a then_case and an else_case. This avoids the static variable and synthetic labels, and will thus make the code much more concise.

I've done this. I had to make the auxiliary variables static, otherwise they were going out of scope at the end of the else clause, being declared dead, and CBMC didn't produce the right test suite.

owen-mc-diffblue · 2017-04-13T09:08:05Z

I haven't made any changes to the java code since the last round - I'll do it once the C code has been reviewed.

I included a commit to turn off the failing test that is fixed in #771 so that the CI can produce the correct results. This commit should be removed before this PR is merged.

Using code_ifthenelset properly makes things a lot simpler. Unfortunately it introduced issues of scope, so I've had to make all the intermediate variables have is_static_lifetime true so they don't go out of scope at the end of the else clause. This means that they aren't declared in the output of show-goto-functions, which I feel is a bit less clear, but seems to be the desired behaviour for is_static_lifetime (=global?) variables. Since the declarations are not doing anything I've removed them. Java already uses is_static_lifetime=true intermediate variables, I believe. One alternative would be to collect all the variable declarations in a separate code block and output them before all the other code for that parameter, in a similar way that we collect the INPUT() lines to the end.

I made a helper function, concatenate_code_blocks(), which I feel should be a method on code_blockt.

tautschnig · 2017-04-13T09:17:40Z

I haven't made any changes to the java code since the last round - I'll do it once the C code has been reviewed.

Cool, I'll take a look.

I included a commit to turn off the failing test that is fixed in #771 so that the CI can produce the correct results. This commit should be removed before this PR is merged.

I've taken another look at #771, and merged it to avoid further overhead. You might thus remove your commit (after rebasing).

Using code_ifthenelset properly makes things a lot simpler. Unfortunately it introduced issues of scope, so I've had to make all the intermediate variables have is_static_lifetime true so they don't go out of scope at the end of the else clause. This means that they aren't declared in the output of show-goto-functions, which I feel is a bit less clear, but seems to be the desired behaviour for is_static_lifetime (=global?) variables. Since the declarations are not doing anything I've removed them. Java already uses is_static_lifetime=true intermediate variables, I believe. One alternative would be to collect all the variable declarations in a separate code block and output them before all the other code for that parameter, in a similar way that we collect the INPUT() lines to the end.

Ok, I'll take a look. I'm pretty sure that the declarations should just be placed ahead of any if/else anyway.

I made a helper function, concatenate_code_blocks(), which I feel should be a method on code_blockt.

I fully agree.

tautschnig · 2017-04-13T09:20:17Z

src/ansi-c/c_nondet_symbol_factory.cpp

+
+\*******************************************************************/
+
+static symbolt &c_new_tmp_symbol(


I think you can return it as a const symbolt &

tautschnig · 2017-04-13T09:22:22Z

src/ansi-c/c_nondet_symbol_factory.cpp

+  {
+    target_block.add(to_code(operand));
+  }
+}


As suggested in your comment, this should really go in util/std_code.h, as a member function of code_blockt. It would then be worthwhile using reserve to do the re-allocation of memory just once.

tautschnig · 2017-04-13T09:23:47Z

src/ansi-c/c_nondet_symbol_factory.cpp

+  //   INPUT("tmp$<temporary_counter>", tmp$<temporary_counter>);
+
+  symbolt &aux_symbol=c_new_tmp_symbol(symbol_table, loc, allocate_type);
+  aux_symbol.is_static_lifetime=static_lifetime;


Maybe static lifetime should actually be a parameter to c_new_tmp_symbol? setting it in there once and that re-setting it here seems questionable.

Oops, setting it in two places was a mistake. Well, hopefully I'll stop using static lifetime tmp symbols, but if I do continue using them I'll make it an option, and definitely only do it in one place.

tautschnig · 2017-04-13T09:26:27Z

src/ansi-c/c_nondet_symbol_factory.cpp

+    else
+    {
+      // Add the following code to init_code:
+      //           IF !(NONDET(_Bool) == FALSE) THEN GOTO <label1>


This comment isn't exactly what the code now does, please update.

I'm not sure exactly what you mean. Do you mean that changing the condition of the if-then-else clause means that this line changes? I ended up having to back out that change because it wouldn't run with just --cover branch, without --show-goto-functions.

tautschnig · 2017-04-13T09:27:45Z

src/ansi-c/c_nondet_symbol_factory.cpp

+      const exprt null_return=from_integer(0, c_bool_typet(1));
+
+      code_ifthenelset null_check;
+      null_check.cond()=equal_exprt(nondet_bool, null_return);


This equality test on nondet is redundant - it's sufficient to just do null_check.cond()=c_get_nondet_bool(c_bool_typet(1));

Done. I've been thinking that the code that was being generated here was a bit clunky, but I didn't see the obvious fix.

Actually that generated an error when running without --show-goto-functions. I ran on pointer-function-parameters/main.c with the flags --function fun --cover branch and I got this output:

Passing problem to propositional reduction converting SSA ######### lhs: symbol * type: bool * identifier: goto_symex::\guard#1 * expression: symbol * type: bool * identifier: goto_symex::\guard * L2: 1 * L1_object_identifier: goto_symex::\guard * #SSA_symbol: 1 ######### rhs: typecast * type: c_bool * width: 1 0: nondet_symbol * type: bool * identifier: symex::nondet0 * #source_location: nil equality without matching types /home/owen/workspace/cbmc/src/cbmc/cbmc exited with code 10

Going back to using an equal_exprt got rid of the problem.

tautschnig · 2017-04-13T09:32:44Z

src/ansi-c/c_nondet_symbol_factory.cpp

+    // pointer to a pointer temporary variables are created in else clauses,
+    // and thus go out of scope before the function is called.
+    exprt allocated=
+      allocate_object(non_null_inst, expr, subtype, true);


If you make this call return two code blocks -- a declaration block and an assignment block, then you should be able to get away without static-lifetime objects. This would be highly preferable for the concurrency encoding.

It's a little bit more complicated than that. Because when this function recursively calls itself, even if we put the variable declaration before the if-else statement it can end up inside another else clause, and thus going out of scope before we call the entry function. I can however do it by collecting all the variable declarations separately from the other code and then putting them in the right order at the very end, a bit like what we're currently doing with input_recorder.

owen-mc-diffblue · 2017-04-15T07:11:42Z

I've updated the PR addressing all comments. I realised I could deal with putting all the variable declarations first and putting all the INPUT statements last at the same time by keeping a list of pointers to the symbols that had been created and generating all the code at the very end. That removes all the code for input_recordert, which makes the code a lot shorter.

As before, I haven't updated the java code, but I will do so once it's clear that the C code is taking the right approach.

tautschnig · 2017-04-15T08:42:02Z

src/ansi-c/c_nondet_symbol_factory.cpp

+
+      code_ifthenelset null_check;
+      null_check.cond()=
+        equal_exprt(c_get_nondet_bool(c_bool_typet(1)), false_expr);


To address the equality-without-matching-types issue you should probably just do

null_check.cond()=side_effect_expr_nondett(bool_typet());

The issue is the c_bool_typet placed in here. Apologies for not spotting that any earlier.

Make it deal with pointer parameters to C functions. We follow the java code to prepare for one day merging them. The C code doesn't yet deal with structs or arrays, which the java code does.

Following the review of the equivalent C code, these changes were made: set replaced with unordered set; helper functions declared static and not exported in header; zero_initializer() replaced with from_integer() and all uses of message_handlert removed;

tautschnig

Looks good to me! You might want to add the remaining cleanup for the Java code, if feasible.

owen-mc-diffblue · 2017-04-18T16:33:34Z

Yes, I definitely want to clean up the java, especially the simpler use of if_then_elset.

owen-mc-diffblue · 2017-04-21T13:27:26Z

I created #853 to do the final refactoring I'd intended.

owen-mc-diffblue force-pushed the feature/pointer-function-parameters branch from 338ba47 to 74f8eaa Compare April 6, 2017 11:15

owen-mc-diffblue force-pushed the feature/pointer-function-parameters branch from 8742644 to 74f8eaa Compare April 6, 2017 14:06

tautschnig requested changes Apr 6, 2017

View reviewed changes

tautschnig assigned tautschnig and owen-mc-diffblue Apr 7, 2017

owen-mc-diffblue force-pushed the feature/pointer-function-parameters branch 2 times, most recently from a8f7b4b to e4fe932 Compare April 7, 2017 16:51

tautschnig requested changes Apr 7, 2017

View reviewed changes

owen-mc-diffblue force-pushed the feature/pointer-function-parameters branch from e4fe932 to 350a7be Compare April 10, 2017 10:48

tautschnig reviewed Apr 10, 2017

View reviewed changes

tautschnig mentioned this pull request Apr 12, 2017

Test harness output #810

Merged

owen-mc-diffblue force-pushed the feature/pointer-function-parameters branch from 350a7be to 55afbae Compare April 13, 2017 08:47

tautschnig reviewed Apr 13, 2017

View reviewed changes

owen-mc-diffblue force-pushed the feature/pointer-function-parameters branch from 55afbae to 358fb48 Compare April 15, 2017 07:05

tautschnig reviewed Apr 15, 2017

View reviewed changes

Owen Jones added 3 commits April 18, 2017 09:41

Reorganise C parameter creation

5ec389d

Make it deal with pointer parameters to C functions. We follow the java code to prepare for one day merging them. The C code doesn't yet deal with structs or arrays, which the java code does.

Clean up formatting of java code

2194b31

Refactor java code

f777e29

Following the review of the equivalent C code, these changes were made: set replaced with unordered set; helper functions declared static and not exported in header; zero_initializer() replaced with from_integer() and all uses of message_handlert removed;

owen-mc-diffblue force-pushed the feature/pointer-function-parameters branch from 358fb48 to f777e29 Compare April 18, 2017 08:42

tautschnig approved these changes Apr 18, 2017

View reviewed changes

Merge branch 'master' into feature/pointer-function-parameters

db510c9

kroening merged commit 7b42a2b into diffblue:master Apr 19, 2017

owen-mc-diffblue mentioned this pull request Apr 20, 2017

Clean up code for pointer function parameters #853

Merged

tautschnig mentioned this pull request Apr 24, 2017

Factor nondet choices in object factory #863

Closed


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

		static symbolt &c_new_tmp_symbol(

Reorganise C parameter creation #767

Reorganise C parameter creation #767

Conversation

owen-mc-diffblue commented Apr 6, 2017

owen-mc-diffblue commented Apr 6, 2017 • edited Loading

tautschnig commented Apr 6, 2017

tautschnig commented Apr 6, 2017

owen-mc-diffblue commented Apr 6, 2017 • edited Loading

tautschnig 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

owen-mc-diffblue Apr 6, 2017 • edited Loading

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

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

tautschnig 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

owen-mc-diffblue commented Apr 13, 2017

tautschnig commented Apr 13, 2017

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

owen-mc-diffblue Apr 14, 2017 • edited Loading

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

owen-mc-diffblue Apr 14, 2017 • edited Loading

Choose a reason for hiding this comment

owen-mc-diffblue Apr 15, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 15, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 18, 2017

owen-mc-diffblue commented Apr 21, 2017

owen-mc-diffblue commented Apr 6, 2017 •

edited

Loading

owen-mc-diffblue commented Apr 6, 2017 •

edited

Loading

owen-mc-diffblue Apr 6, 2017 •

edited

Loading

owen-mc-diffblue Apr 14, 2017 •

edited

Loading

owen-mc-diffblue Apr 14, 2017 •

edited

Loading

owen-mc-diffblue Apr 15, 2017 •

edited

Loading