Optimisations in generated code with function pointers

[thk123]

This is a proof of concept - there are still some structural improvements to be made (and function headers for all the functions) - so don't merge just yet.

Previously if a variable was a function pointer - we would branch in the goto program on all functions that had the right signature. This was causing problems in cases that uses dispatch tables as in reality it would be a very small number of functions that could actually be used.

The approach taken here is to handle these specific cases more intelligently. Basically, if we can work out either exactly what the function pointer is pointing to (because it is constant) or work out which array the function will come from (because it is pointing to an index inside an array), then we only generate code to handle these functions.

The main area of feedback I would appreciate is to do with resolving indirect access. For example, if the pointer is pointing to a symbolt then we need to look up the symbol in the symbol table and find what that is pointing to. Although I think below handles most cases (And should fail back to the old naive approach of all matching functions in the cases it can't), but I suspect there is some general code I should be using here to resolve this but I couldn't find any.

[thk123]

Some tests that should be added:

• Non const array
• Non const variable
• Check the & before function name doesn't change the goto program
• Arbitrarily nested symbols (particularly variable->variable->array)
• Array of constant function pointers except one

[thk123]

These no-body if statements aren't very clean. I shall have a think about a better way to structure this code.

[thk123]

Perhaps something like:

bool matched=false;
matched=matched||try_get_precise_call(...)
matched=matched||try_get_from_address_of(...)

[thk123]

This happens if we can't convert one of the operands in the array - I suppose this could happen if most of the values are constant but one is not. In this case I suppose we have to fall back to the worst cast - should add a test for this.

[thk123]

In the to_integer part of the code base, the general rule seems to be return false (i.e. 0 I guess) for errors, but this seems backward to me in general. Should I invert my functions to return false if everything went well?

[tautschnig]

So overall the Boolean return value signals whether an error occurred, i.e., it's "true" whenever something bad happened. Whether this is good or bad is a different question.

[thk123]

Confusingly, I managed to my comment exactly 50% wrong, it should have read:

return false (i.e. 0 I guess) for no errors, but this seems backward to me in general. Should I invert my functions to return false if everything went well.

To which I think your answer means return true for errors, else return true/false if the function clearly implies a truthy value.

I couldn't find a lot of try_ methods, but path_searcht::try_await for example returns true for no errors, so I suppose try suggests a truthy value of true meaning we tried and succeeded. So I will leave as it is.

[thk123]

I don't really know what ID_typecast is doing here, but it shows up when accessing the array by index - it is straightforward to resolve but feels a bit hard coded...

[thk123]

@tautschnig This feels like something you might know?

[thk123]

Perhaps simplify_expr would be useful here.

[tautschnig]

I may have answered this question in the other comments: in order to follow a symbol to its value, you'd need all the definitions, and thus a def-use analysis.

[thk123]

Sorry I'm not sure I fully understand - am I not already following the symbols to their values? I'm currently (recursively) when I find a ID_symbol, look at its ID_identifier, look that up in the symbol_table and look at the symbols value.

I was hoping this logic for recursively resolving the symbols (and ideally dealing with other things like casting) would exist in the simplify_expr but it doesn't seem to be working as I had hoped.

[thk123]

This falls apart as soon as the array is modified as it incorrectly assumes it is not. For example this code:

#include <stdio.h>

void f1 (void) { printf("%i", 1); }
...
void f9 (void) { printf("%i", 9); }

typedef void(*void_fp)(void);

void_fp fp_tbl[] = {f2, f3, f4};
void_fp fp_tbl2[] = {f1, f2, f3, f4, f5 ,f6, f7, f8, f9};

void func(void_fp fp, int i){
  fp_tbl[2] = fp;
  void_fp fp2 = fp_tbl[2];
  fp2();
}

void main(){
   for(int i=0;i<3;i++){
     func(fp_tbl2[i+3], i);
   }
}

produces 456 as its output, but the goto code for func is (under this PR):

// 44 file main.c line 22 function func
fp_tbl[(signed long int)2] = fp;
// 45 file main.c line 23 function func
void (*fp2)(void);
// 46 file main.c line 23 function func
fp2 = fp_tbl[(signed long int)2];
// 47 file main.c line 24 function func
f4();
// 48 file main.c line 25 function func
dead fp2;
// 49 file main.c line 25 function func
END_FUNCTION

i.e. would produce 444.

To resolve this we need to either detect the array being modified or only apply this optimisation on arrays that are declared constant at compile time.

I imagine the second is easier (maybe just calling is_constant()?) but, for example, wouldn't fix the original code where the array was not declared const, is supporting this required @danpoe @martin-cs ? Is there perhaps already logic to deal with the idea of variables changing value?

[danpoe]

I'm not sure whether supporting non-const arrays is required.

As far as I know there does not exist code yet to simply check whether an array is ever written to. I think looping through all assignments in the code and gathering all left-hand side symbols and afterwards checking if the array symbol is contained in there would be fine. Additionally we would need to check that the address of the array is never taken as otherwise it could be modified through a pointer. This can be done via dirtyt in analyses/dirty.{h, cpp}.

[tautschnig]

@peterschrammel Do we have any code (possibly in 2LS?) that turns a goto program into SSA form? No loop unwinding or precise phi nodes. Otherwise we could resort to the existing def-use analysis to identify whether any arrays have been written to.

[tautschnig]

Nit picking: newlines after each ","

[thk123]

I think this changed as I thought it would require that but @peterschrammel has told me that if it fits on one line, then that's OK, see this:

put each argument on a separate line if they do not fit after one line break

https://github.com/diffblue/cbmc/blob/master/CODING_STANDARD#L12

[tautschnig]

Missing return value?

[thk123]

Fixed.

[tautschnig]

const address_of_exprt &...

[tautschnig]

I had thought about the precision problems we have function pointer handling some time ago, and it wasn't entirely clear to me why we would not want to run a full data-flow analysis (via ait)? (My todo item says: "remove-function-pointers should use concurrency-aware static analysis if entry point is known") This pull request effectively does this, under the constraint that the function pointers are set exactly once, as constants. Note that function pointers lend themselves to a much more lightweight analysis that general pointers (in C): there is no arithmetic on them, or dynamic allocation.

Thoughts?

[tautschnig]

See discussion on what I think needs to be done here.

[peterschrammel]

@tautschnig, the def-use analysis for 2ls is https://github.com/diffblue/2ls/blob/master/src/ssa/ssa_domain.h

[danpoe]

@tautschnig Do you mean first running the existing remove_function_pointers, then running a function pointer analysis on that program, and then using the computed information to produce again a program with function pointers removed (but more precise case distinctions)?

The issue we're having is that remove_function_pointers runs out of memory because of the large number of type-compatible functions (see diffblue/cbmc-toyota#12) and hence huge case distinctions, thus we'd want to avoid to run the plain remove_function_pointers first.

The most precise way would probably be to integrate a function pointer analysis with the ait framework fixpoint computation.

[thk123]

@thk123 Should also add some tests for the case when the array is represented as a pointer. I'm not sure exactly how goto handles this.

[thk123]

I've added checking the const-ness of the array which seems to work. I'll quickly address the other feedback requests.

@danpoe I think for this simple version we don't need to check pointer reassignment as assigning a const array to a non-const pointer and then modifying that pointer is UB I think? And as such, I think @martin-cs said if there is UB we don't care.

I don't know if I should be looking in to the more complex solutions suggested above, for the specific case we are trying to fix, providing they can mark the function pointer arrays as const then this is smart enough. I guess this is a question for you @martin-cs?

TODO:

• simplify_expr if applicable
• smarter approach to non-const arrays if we are doing that
• add these tests Optimisations in generated code with function pointers #434 (comment)

[thk123]

The following lines could be replaced by a return false on the last line of the function, do people think it is clearer like this or collapsed down.
Clearer like it is - can see all the ways the method can fail explicitly
Clearer other way - hard to keep track of which if the else corresponds to.

[tautschnig]

For a full solution it might indeed be necessary to have an analysis that runs a fixed point over both def-use (whether implemented via SSA or otherwise), and pointers (including function pointers). This may be way more elaborate than what's intended here, in which case the simple approach for const symbols/arrays would do.

[thk123]

Add check for function pointer inside a struct. Sanity check the variable works iff const. Travis compile errors related to #467 Add a test to check that the UB of loosing const is in fact picked up by goto-cc and also check C standard to check it is in fact UB.

[tautschnig]

Noting on here as well that #467 is fixed. Rebase to re-run the tests?

[thk123]

Definitely UB to assign const to non-const, 6.7.3.6:

If an attempt is made to modify an object defined with a const-qualified type through use
of an lvalue with non-const-qualified type, the behavior is undefined.

[thk123]

Like with const arrays, we need to apply the same const check to values, otherwise for example this code behaves incorrectly:

void func()
{
  void_fp fp = f2;
  fp = f3;
  fp();
}

This bug exists in the master branch, this gets incorrectly optimised to calling f2() I will fix as part of this PR, should I create an issue for it anyway? My mistake, hadn't built.

[thk123]

@tautschnig This looks to still be failing with these errors having rebased, are these still related to you or is something else going on? https://travis-ci.org/diffblue/cbmc/jobs/194806576#L2013

../ansi-c/library/jsa.h:929:7: error: unused label '__CPROVER_jsa_pred_opcode_3'
[-Werror,-Wunused-label]
__CPROVER_jsa_pred_opcode_3: __CPROVER_jsa_execute_pred_result=__C...

[tautschnig]

@thk123 This will only be solved once #451 is merged. More to be said about this, but not in public.

[thk123]

The only thing missing from this PR (I believe) is the implementation for handling structs containing function pointers and pointers to function pointers. I've added KNOWNBUG regressions demonstrating this limitation, I'll either implement it and replace the "temp checkin" with the implementation or I will replace the "temp implementation" with just the failing tests and create corresponding issues.

[tautschnig]

Could we at least have a fall-back for all cases that the new code can't handle? I don't think we should end up in a situation where we gain precision on the one hand, but also fail in cases we previously wouldn't.

[martin-cs]

This looks awesome but is it under the wrong issue? Cheers, - Martin

[martin-cs]

Could we at least have a fall-back for all cases that the new code can't handle?

Yes; we should definitely have this.

[tautschnig]

Apologies for putting a surprising hard stop on this one: I just learned there is src/musketeer/propagate_const_function_pointers.cpp - could you please see to what extent we have overlap and/or can get rid of it?

[danpoe]

As far as I remember the purpose of src/musketeer/propagate_const_function_pointers.cpp is to propagate function pointers through the arguments/parameters of functions. The intention was to resolve the function pointers in code like the following:

void *thread(void *arg) {}

void create_worker(void *(*fp)(void)) {
  pthread_create(..., fp, ...); // we want to resolve fp here
}

int main()
{
  create_worker(thread); // function name is used here
}

[thk123]

Bit of a brain dump, feel free to ignore, just assesing what the propogate_const_function_pointers does and how it coule be combined with my changes in this PR.

TL;DR:

• They don't do the same things (though there may be some overlap in their results).
• They could be combined to be more precise, though this would be some work.
• There isn't a lot of obvious overlap in the code as they are working out what they work out in quite different ways.
• It isn't obvious to me whether the musketeer code would scale

So even if the parameter to create_worker were marked as const, my improvement still can't figure it out since it doesn't know where the function was called from.

The code in musketeer appears to start at the entry point and track each call site for each function and tracks the function pointers. It then replaces them when it can in the actual function call.

I'm not sure, but I don't think this is a comprehensive super-set of my changes since I don't think it would deal with arrays of FPs. It also seems to me (though this could be completely wrong) that this won't scale to large applications as it basically walks through a complete CFG tracking all ways a function can be called?

To combine them you would want to run this one first and this will introduce constant FPs that the second step can resolve. You could also extend this to apply the same logic to arrays of FPs in cases where they were passed in to a function.

[tautschnig]

@danpoe, @thk123 thanks a lot for the comments/review. It's good to have this documented (even though the source might ultimately be the place to do so).

[thk123]

I think some of the failing tests have some incorrect code (discovered whilst looking at some logging for missed edge cases). This shouldn't be merged until I've pushed some improvements to these tests to make their failure more precise.

[thk123]

Martin has also found some bugs and limitations with this which I will be addressing this week, so can probably hold off merging until those are complete and have been reviewed.

[martin-cs]

May I suggest the following: 1. The function pointer removal code in: goto-function/remove_function_pointers.cpp should remain 'stateless', so that it only uses the expression and definitions / types of any symbols used in it. 2. We should get the abstract interpreter to tolerate and eventually track function pointers. This will allow stateful analysis. We need this for other reasons. 3. Then --simplify --context-dependent --constant --function-pointer-sensitivity=set (or whatever) should be able to perform the simplification that is used in Musketeer.

[tautschnig]

Apologies for the on/off on this one. As first step we should have the additional tests added to see more clearly where the problems are. I feel that we are somewhat back to my first comments on this PR, saying that it would actually need a full data-flow analysis.

[thk123]

@tautschnig Sorry if I've not understood, but isn't what Martin is saying is the remove-function-pointers will be a very simple first pass that remains stateless (i.e. without a data flow analysis).

I am going to quickly get a messy branch sorted for Martin so he can verify it fixes all the problems and then I shall clean it up for this PR (it will have more tests covering different cases that it does and doesn't handle).

A TODO list for my reference:

• Fix function-pointer2 test and add separate failing test (atm this test passes but really shouldn't!)
• Add tests for direct access to array, pointer and struct member as it subtly changes the first expression that must be unpacked by remove-function-pointers
• Handle function pointers accessed through a const function pointer symbol
• Clean Martin's fix for structs
• Clean Martin's fix for arrays containing null pointers
• Clean Martin's fix for casts inside arrays
• Ensure arrays of structs work
• Ensure pointers to structs work

This should be done by Thursday. Then I will fix up this PR with these changes and clearer testing.

[martin-cs]

Yes to all of the above. Give me / @tautschnig a shout if you want back-up / to discuss the best way of handling some of these.

[tautschnig]

I think the key problem is that we need to figure out which ones can genuinely be handled in a stateless fashion: that's those where a const symbol holds all the possible values, and that symbol is genuinely never written to after initialisation. I think the existing code will be ok for the first part of that sentence (with some extensions as noted in your task list), but I think we are missing a check that the symbol (despite being declared const) is really never written to. I think I can put up a pull request for a helper analysis that will take care of that latter part.

[martin-cs]

On Wed, 2017-02-01 at 06:43 -0800, Michael Tautschnig wrote: I think we are missing a check that the symbol (despite being declared const) is really never written to.

This is part of a larger issue in abstract interpretation - you have to assume that undefined behaviour doesn't occur / things are type safe unless explictly noted otherwise because otherwise the first write to an array in which you can't bound the parameters of the index will set everything to top. The exact rules / assumptions are not entirely clear to me but I think they are worth working out and documenting as this does not seem to be an issue that is widely discussed in the academic literature but has huge inpact on things like the use of AI for security work. For example, exploit location with AI is much harder than you'd think.

I think I can put up a pull request for a helper analysis that will take care of that latter part.

That would be awesome. Cheers, - Martin

[tautschnig]

As first step we'd want the basic check that 1) there is no write to a symbol deemed const and 2) that it's address is never taken. Surely undefined behaviour causes additional trouble, but then at least we've got a first "check" step in place that can possibly be extended.

[tautschnig]

Ok, I was a bit confused - really what I was thinking of was @danpoe's work in 2df6785 that locates unused symbols. The other related work is #449. Both of which lay the grounds (in slightly different ways) for locating unused objects. #449 is probably closer in that it already uses read/write sets.

[thk123]

Progress update on this:

I have a reasonable version that deals with most cases correctly (not far advanced from what I sent you at the close of play on Thursday @martin-cs). This afternoon I fixed the structs containing const FP members but themselves are mutable. I have also started an audit on the very large number of regression tests to check I've covered all cases, there aren't any duplicates and to give them better names for a proper PR. In doing so, I have found a bug with pointers to function pointers, specifically, we don't require them to be const but should. I will complete this audit tomorrow and share it on here in case there are other cases I've not covered. Then I will fix the bug(s).

Once that is done, the only missing feature should be array indices who are constant but a non-trivial expression (i.e. arr[const_var & 2] for example). This can either be fixed or ignored. Then to get this PR prepared I will need to:

• Comment functions
• Couple of cleaning tasks (like breaking a couple fo large functions up)
• Git maintenance to get only relevant changes and files]
• Renaming regression tests

Will confirm after discussion with @martin-cs tomorrow when this will get done.

[thk123]

Finished the audit of the tests, can see a full list here: https://docs.google.com/spreadsheets/d/115b60q89eMAVAQAUPfyYLTwGEE80Pw5UX-nUjYdhH0E/edit?usp=sharing

In doing this I found some problems and some missing cases which I will address next:

• Verify 33 covers what it should it didn't (and shouldn't have)
• [Precise] 37 - Const FP assigned to a const FP component in an array of structs
• [No match] 37 - Const FP assigned to a non const FP component of a non const struct
• [No match] 38 - Const FP assigned to a dereference of a non const pointer to a const FP assgined to a function
• 6 should at least be using a const
• 8 should at least be using const
• 9 is a dupe of 8 (the only difference we are ignoring which is the specific value is not being changed)
• What's the difference between 19 and 20 the difference is one is a valid cast and one is not, can keep both for now
• [No match] 39 - Const FP assigned to a non const pointer to an array of const FPs indexed via a literal
• [No match] 40 - Const FP parameter
• [No match] 41 - Const FP assigned to a const array of const FPs that are picked at run time (look at 6)

I also ran a line coverage on the relevant class. Most of the lines are hit. Most of the ones that are not hit are return false lines where we have failed to unpack the expression which are obviously difficult to create test cases for as if knew how to hit them, could probably support them! There is one major part not covered despite having a test that I think should, so I will investigate that as well (it should be covered by 33)

[thk123]

Based on @martin-cs failures, the cases left to do

• Consistency assert where returning true but no functions
• Missing case: ptt_StsDat->pt_ExeTbl[s4t_i](ptt_MemAdr); (I think this is regression 32)
• return_value_9=ptt_EctStmDat->pt_NpfTbl[s4t_StsNow - (signed long int)2][(signed long int)0](u1t_ExeID, ptt_MemAdr);
• Deal with array indices that are constant calculations
• Apply Martins debugging patch
• Move into fresh branch
• Rename regressions
• Ensure coverage for final return false as missing these is what caused the inconsistent returns - this may be impossible but should have another go.

[thk123]

It has also occurred to me that we don't deal with unions, this shouldn't be hard to add, though unlike structs we would require either every component to be const, or the union as a whole to be const.

[thk123]

@martin-cs Update: found a big bug, I must have misunderstood what you meant by mutable structs with const function pointers, the following code can't be optimised since we can write over the whole struct.

#include <stdio.h>

void f1 (void) { printf("%i", 1); }
void f2 (void) { printf("%i", 2); }
void f3 (void) { printf("%i", 3); }
void f4 (void) { printf("%i", 4); }
void f5 (void) { printf("%i", 5); }
void f6 (void) { printf("%i", 6); }
void f7 (void) { printf("%i", 7); }
void f8 (void) { printf("%i", 8); }
void f9 (void) { printf("%i", 9); }

typedef void(*void_fp)(void);

struct state
{
  int x; // Mutable!
  const void_fp go;
};
struct state thing = {0, &f2};

struct state other_thing = {0, &f4};

// There is a basic check that excludes all functions that aren't used anywhere
// This ensures that check can't work in this example
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};

void func(int i){
  // overwrite the whole of thing including the FP!
  thing = other_thing;
  const void_fp fp = thing.go;
  fp();
}

void main(){
   for(int i=0;i<3;i++){
     func(i);
   }
}

As such I've modified it to require the whole variable is const (and we don't care about the const-ness of individual components). Therefore I'm not sure if it is going to work with your mutable struct, but if it doesn't it shouldn't, as the structs value can be legally changed... See this commit for full details: thk123@c88c1af

[thk123]

Tomorrow will move this into a clean branch to make a PR and close this one out. The only thing to investigate is the logging and behaviour of regression 11 looks a little odd (note for myself).

[thk123]

As promised - clean version of this PR #519 so closing this now. I don't think there is anything outstanding from this PR thread that needs action in the new one.