How does SVF handle external functions without entities during memory analysis?

[Ehu1]

trafficstars

define dso_local i32 @main() #0 {
entry:
  %retval = alloca i32, align 4
  %a = alloca i32, align 4
  %b = alloca i32, align 4
  %c = alloca i32*, align 8
  %d = alloca i32*, align 8
  store i32 0, i32* %retval, align 4
  store i32 0, i32* %a, align 4
  store i32 0, i32* %b, align 4
  store i32* %a, i32** %c, align 8
  store i32* %a, i32** %d, align 8
  %0 = load i32*, i32** %c, align 8
  call void @r(i32* noundef %0)
  %1 = load i32*, i32** %d, align 8
  call void @r(i32* noundef %1)
  ret i32 0
}

declare dso_local void @r(i32* noundef) #1

This is the C code corresponding to this IR.

void r(int *x);
int main() {
  int a = 0, b = 0;
  int *c = &a;
  int *d = &a;
    r(c);

    r(d);

  return 0;
}

I cannot discover through traversing the nodes or edges on SVFG that these two functions may operate on the same memory. I believe that even if a function has no entity, there should be a FormalIn node.

[Ehu1]

__Nodes__
SVFGNodeID: 22 >= FormalINSVFGNode >= MVER: {FormalINSVFGNode ID: 22 {fun: main}10V_1 = ENCHI(MR_10V_1)
pts{17 }

MRVERID: 9 MemRegion: pts{17 } MRVERSION: 1 MSSADef: 3, pts{17 }} >= ICFGNodeID: 1
SVFGNodeID: 23 >= FormalINSVFGNode >= MVER: {FormalINSVFGNode ID: 23 {fun: main}8V_1 = ENCHI(MR_8V_1)
pts{15 }

MRVERID: 7 MemRegion: pts{15 } MRVERSION: 1 MSSADef: 3, pts{15 }} >= ICFGNodeID: 1
SVFGNodeID: 24 >= FormalINSVFGNode >= MVER: {FormalINSVFGNode ID: 24 {fun: main}6V_1 = ENCHI(MR_6V_1)
pts{13 }

MRVERID: 5 MemRegion: pts{13 } MRVERSION: 1 MSSADef: 3, pts{13 }} >= ICFGNodeID: 1
SVFGNodeID: 25 >= FormalINSVFGNode >= MVER: {FormalINSVFGNode ID: 25 {fun: main}4V_1 = ENCHI(MR_4V_1)
pts{11 }

MRVERID: 3 MemRegion: pts{11 } MRVERSION: 1 MSSADef: 3, pts{11 }} >= ICFGNodeID: 1
SVFGNodeID: 26 >= FormalINSVFGNode >= MVER: {FormalINSVFGNode ID: 26 {fun: main}2V_1 = ENCHI(MR_2V_1)
pts{8 }

MRVERID: 1 MemRegion: pts{8 } MRVERSION: 1 MSSADef: 3, pts{8 }} >= ICFGNodeID: 1
FormalOUTSVFGNode ID: 27 {fun: main}RETMU(8V_2)
pts{15 }

SVFGNodeID: 27 >= FormalOUTSVFGNode >= MVER: {MRVERID: 13 MemRegion: pts{15 } MRVERSION: 2 MSSADef: 1, pts{15 }} >= ICFGNodeID: 21
FormalOUTSVFGNode ID: 28 {fun: main}RETMU(10V_2)
pts{17 }

SVFGNodeID: 28 >= FormalOUTSVFGNode >= MVER: {MRVERID: 14 MemRegion: pts{17 } MRVERSION: 2 MSSADef: 1, pts{17 }} >= ICFGNodeID: 21
FormalOUTSVFGNode ID: 29 {fun: main}RETMU(6V_2)
pts{13 }

SVFGNodeID: 29 >= FormalOUTSVFGNode >= MVER: {MRVERID: 12 MemRegion: pts{13 } MRVERSION: 2 MSSADef: 1, pts{13 }} >= ICFGNodeID: 21
FormalOUTSVFGNode ID: 30 {fun: main}RETMU(4V_2)
pts{11 }

SVFGNodeID: 30 >= FormalOUTSVFGNode >= MVER: {MRVERID: 11 MemRegion: pts{11 } MRVERSION: 2 MSSADef: 1, pts{11 }} >= ICFGNodeID: 21
FormalOUTSVFGNode ID: 31 {fun: main}RETMU(2V_2)
pts{8 }

SVFGNodeID: 31 >= FormalOUTSVFGNode >= MVER: {MRVERID: 10 MemRegion: pts{8 } MRVERSION: 2 MSSADef: 1, pts{8 }} >= ICFGNodeID: 21


__Edges__
   %0 = load i32*, i32** %c, align 8 
srcSVFGNodeID: 11 => dstSVFGNodeID: 16 >= LoadNode | MVER: {MRVERID: 13 MemRegion: pts{15 } MRVERSION: 2 MSSADef: 1, pts{15 }}
   %1 = load i32*, i32** %d, align 8 
srcSVFGNodeID: 12 => dstSVFGNodeID: 17 >= LoadNode | MVER: {MRVERID: 14 MemRegion: pts{17 } MRVERSION: 2 MSSADef: 1, pts{17 }}

The above information is obtained through SVFGReadWrite.cpp.

[yuleisui]

You may wish to add your function definition into this external api file and rebuild/remake SVF. https://github.com/SVF-tools/SVF/blob/master/svf-llvm/lib/extapi.c

[Ehu1]

You may wish to add your function definition into this external api file and rebuild/remake SVF. https://github.com/SVF-tools/SVF/blob/master/svf-llvm/lib/extapi.c

Thank you for your response, my issue has been resolved.

[Ehu1]

You may wish to add your function definition into this external api file and rebuild/remake SVF. https://github.com/SVF-tools/SVF/blob/master/svf-llvm/lib/extapi.c

  %77 = getelementptr i8, i8* %41, i64 %76, !dbg !125
  %118 = getelementptr i8, i8* %82, i64 %117, !dbg !125
  %136 = getelementptr i8, i8* %124, i64 %135, !dbg !125
  %137 = bitcast void (...)* @laplacian_ to void (i8*, i8*, i8*, ...)*, !dbg !125
  call void (i8*, i8*, i8*, ...) %137(i8* %77, i8* %118, i8* %136), !dbg !125

How to handle calls to external functions that require type conversion, where the original function is transformed into a function named ' '?