topl can't handle functions from pointers

[qequ]

Please make sure your issue is not addressed in the FAQ.

Please include the following information:

• [x] The version of infer from infer --version.

• [x] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc.

• [x] Which command you ran, for example infer -- make.

• [x] The full output in a paste, for instance a gist.

• [x] If possible, a minimal example to reproduce your problem (for instance, some code where infer reports incorrectly, together with the way you run infer to reproduce the incorrect report).

• infer version Infer version v1.1.0

• OS; Ubuntu 20.04.5 LTS

Having a C program like this

#include <stdio.h>

void hello(int x)

{
    printf("%d\n", x);
    (void)x;
}

void world(int x)

{
    printf("%d\n", x);
    (void)x;
}

void callfunctions(void (*f)(int), void (*g)(int))

{

    (*f)(1);

    (*g)(2); // Error in topl: argument should be the same as that passed to hello()
}

int main(void)

{

    callfunctions(&hello, &world);

    return 0;
}

and topl file like this

property RepeatArgument
  prefix "repeat"
  start -> start: *
  start -> trackingParams: callfunctions(Arg1, Arg2, VoidRet) => func1 := Arg1; func2:= Arg2
  trackingParams -> trackHello: func1(Arg3, VoidRet) => x := Arg3
  trackHello -> error: func2(Arg4, VoidRet) when x != Arg4

calling infer with the command infer --topl --topl-properties test_ptr.topl -- gcc test_rep_arg_ptr.c

infer doesn't catch the error in the code and generates this output

Capturing in make/cc mode...
Found 1 source file to analyze in /home/alvaro/infer_testing/infer-out
1/1 [################################################################################] 100% 36.851ms

  No issues found  

with different variants of topl file looking directly for the functions like

property RepeatArgument
  prefix "repeat"
  start -> start: *
  start -> trackingHello: "(*f)"(Arg1, VoidRet) => x := Arg1
  trackingHello -> error: "(*g)"(Arg2, VoidRet) when x != Arg2

property RepeatArgument
  prefix "repeat"
  start -> start: *
  start -> trackingHello: "(*hello)"(Arg1, VoidRet) => x := Arg1
  trackingHello -> error: "(*world)"(Arg2, VoidRet) when x != Arg2

property RepeatArgument
  prefix "repeat"
  start -> start: *
  start -> trackingHello: hello(Arg1, VoidRet) => x := Arg1
  trackingHello -> error: world(Arg2, VoidRet) when x != Arg2

no issue has been found

CC: @dgutson

[dgutson]

ping? @jvillard ?

[jvillard]

The function names in the TOPL transitions are interpreted as regexes over the name of the function being called so func1 will match a function called func1, not the variable you set in the other transition. Similarly for (*f) and (*hello).

But, good news! The last config does in fact seem to work but requires to enable --function-pointer-specialization. I'll see if we can make it enabled by default.

$ cat topl_fptr.topl
property RepeatArgument
  prefix "repeat"
  start -> start: *
  start -> trackingHello: hello(Arg1, VoidRet) => x := Arg1
  trackingHello -> error: world(Arg2, VoidRet) when x != Arg2
$ infer --topl-only --topl-properties topl_fptr.topl --function-pointer-specialization -- clang -c topl_fptr.c
topl_fptr.c:17: error: Topl Error
  property RepeatArgument fails.
  15. }
  16. 
  17. void callfunctions(void (*f)(int), void (*g)(int))
      ^
  18. 
  19. {

Found 1 issue
  Issue Type(ISSUED_TYPE_ID): #
      Topl Error(TOPL_ERROR): 1