diff --git a/src/goto-instrument/README.md b/src/goto-instrument/README.md index 5be917235ba..e2fcf92734c 100644 --- a/src/goto-instrument/README.md +++ b/src/goto-instrument/README.md @@ -26,3 +26,158 @@ developers are advised to copy the directory, remove all files apart from `main.*`, `parseoptions.*` and the `Makefile` and use these as the skeleton of their application. The `doit()` method in `parseoptions.cpp` is the preferred location for the top level control for the program. + +### Main usage ### + +For most of the transformations, `goto-instrument` takes one or two +arguments and any number of options. The two file arguments are +a goto-binary that it uses +as an input for the transformation, and then *another goto binary* that +it uses to write the result of the transformation. This is important +because many times, if you don't supply a second filename for the +goto-binary to be written to, you get the equivalent of the `--help` +option output, with no indication of what has gone wrong. Some of the options +can work with just an input file and not output file. For more specific +examples, take a look at the demonstrations below: + +### Function pointer removal ### + +As an example of a transformation pass being run, imagine you have a file +called `function_pointers.c` with the following content: + + int f1(void); + int f2(void); + int f3(void); + int f4(void); + + int (* const fptbl1[][2])(void) = { + { f1, f2 }, + { f3, f4 }, + }; + + int g1(void); + int g2(void); + + int (* const fptbl2[])(void) = { + g1, g2 + }; + + int func(int id1, int id2) + { + int t; + t = fptbl1[id1][id2](); + t = fptbl2[id1](); + return t; + } + +Then, assuming you have compiled it to a goto-binary with `goto-cc`, called +`function_pointers.goto`, you could see the output of the +`--show-goto-functions` flag on the unmodified program: + + Reading GOTO program from `function_pointers.goto' + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + func /* func */ + // 0 file function_pointer.c line 20 function func + signed int t; + // 1 file function_pointer.c line 21 function func + t=fptbl1[(signed long int)id1][(signed long int)id2](); + // 2 file function_pointer.c line 22 function func + t=fptbl2[(signed long int)id1](); + // 3 file function_pointer.c line 23 function func + return t; + // 4 file function_pointer.c line 23 function func + dead t; + // 5 file function_pointer.c line 23 function func + GOTO 1 + // 6 file function_pointer.c line 24 function func + 1: END_FUNCTION + + +Then, you can run a transformation pass with `goto-instrument --remove-function-pointers function_pointers.goto function_pointers_modified.goto`, +and then ask to show the result of the transformation through +showing the goto-functions again: + + Reading GOTO program from `function_pointers_modified.goto' + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + func /* func */ + // 0 file function_pointer.c line 20 function func + signed int t; + // 1 file function_pointer.c line 21 function func + fptbl1[(signed long int)id1][(signed long int)id2]; + // 2 file function_pointer.c line 21 function func + IF fptbl1[(signed long int)id1][(signed long int)id2] == f3 THEN GOTO 1 + // 3 file function_pointer.c line 21 function func + IF fptbl1[(signed long int)id1][(signed long int)id2] == f2 THEN GOTO 2 + // 4 file function_pointer.c line 21 function func + IF fptbl1[(signed long int)id1][(signed long int)id2] == f1 THEN GOTO 3 + // 5 file function_pointer.c line 21 function func + IF fptbl1[(signed long int)id1][(signed long int)id2] == f4 THEN GOTO 4 + // 6 file function_pointer.c line 21 function func + IF fptbl1[(signed long int)id1][(signed long int)id2] == g1 THEN GOTO 5 + // 7 file function_pointer.c line 21 function func + IF fptbl1[(signed long int)id1][(signed long int)id2] == g2 THEN GOTO 6 + // 8 file function_pointer.c line 21 function func + 1: t=f3(); + // 9 file function_pointer.c line 21 function func + GOTO 7 + // 10 file function_pointer.c line 21 function func + 2: t=f2(); + // 11 file function_pointer.c line 21 function func + GOTO 7 + // 12 file function_pointer.c line 21 function func + 3: t=f1(); + // 13 file function_pointer.c line 21 function func + GOTO 7 + // 14 file function_pointer.c line 21 function func + 4: t=f4(); + // 15 file function_pointer.c line 21 function func + GOTO 7 + // 16 file function_pointer.c line 21 function func + 5: t=g1(); + // 17 file function_pointer.c line 21 function func + GOTO 7 + // 18 file function_pointer.c line 21 function func + 6: t=g2(); + // 19 file function_pointer.c line 22 function func + 7: fptbl2[(signed long int)id1]; + // 20 file function_pointer.c line 22 function func + IF fptbl2[(signed long int)id1] == g1 THEN GOTO 8 + // 21 file function_pointer.c line 22 function func + IF fptbl2[(signed long int)id1] == g2 THEN GOTO 9 + // 22 file function_pointer.c line 22 function func + 8: t=g1(); + // 23 file function_pointer.c line 22 function func + GOTO 10 + // 24 file function_pointer.c line 22 function func + 9: t=g2(); + // 25 file function_pointer.c line 23 function func + 10: return t; + // 26 file function_pointer.c line 23 function func + dead t; + // 27 file function_pointer.c line 24 function func + END_FUNCTION + +You can now see that the function pointer (indirect) call (resulting from +the array indexing of the array containing the function pointers) +has now been substituted by direct, conditional calls. + +### Call Graph ### + +This is an example of a command line flag that requires only one argument, +specifying the input file. + +You can see the call graph of a particular goto-binary by issuing `goto-instrument --call-graph `. This gives a result similar to this: + + Reading GOTO program from `a.out' + Function Pointer Removal + Virtual function removal + Cleaning inline assembler statements + main -> fun + __CPROVER__start -> __CPROVER_initialize + __CPROVER__start -> main + fun -> malloc + +The interesting part of the output in the above text is the last four lines, +that show that `main` is calling `fun`, `__CPROVER__start` is calling `__CPROVER_initialize` and `main` and that `fun` is calling `malloc`.