Goblint crashes on SQLite

[jerhard]

Goblint crashes (within ~1 minute) when running on sqlite with an exception: exception Goblint_lib.LibraryDsl.Pattern.Expected("nil")

Stack trace

``` Fatal error: exception Goblint_lib.LibraryDsl.Pattern.Expected("nil") Raised at Goblint_lib__LibraryDsl.Pattern.fail in file "src/analyses/libraryDsl.ml", line 14, characters 15-33 Called from Goblint_lib__MallocWrapperAnalysis.Spec.special in file "src/analyses/mallocWrapperAnalysis.ml", line 97, characters 10-30 Called from Goblint_lib__MCP.MCP2.special.f in file "src/analyses/mCP.ml", line 458, characters 17-37 Called from Goblint_lib__MCP.MCP2.map_deadcode.one_el in file "src/analyses/mCP.ml", line 100, characters 49-78 Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34 Called from Goblint_lib__MCP.MCP2.map_deadcode in file "src/analyses/mCP.ml", line 101, characters 13-35 Called from Goblint_lib__MCP.MCP2.special in file "src/analyses/mCP.ml", line 460, characters 15-52 Called from Goblint_lib__Constraints.WidenContextLifterSide.lift_fun in file "src/framework/constraints.ml", line 340, characters 25-41 Called from Goblint_lib__Constraints.PathSensitive2.map.h in file "src/framework/constraints.ml", line 992, characters 16-36 Called from BatSet.Concrete.fold in file "src/batSet.ml", line 310, characters 35-56 Called from Goblint_lib__Constraints.PathSensitive2.map in file "src/framework/constraints.ml", line 995, characters 12-43 Called from Goblint_lib__Constraints.DeadCodeLifter.lift_fun in file "src/framework/constraints.ml", line 410, characters 13-29 Called from Goblint_lib__Constraints.HashconsLifter.special in file "src/framework/constraints.ml", line 73, characters 14-43 Called from BatList.map.loop in file "src/batList.mlv", line 237, characters 28-33 Called from BatList.map in file "src/batList.mlv", line 240, characters 4-12 Called from Goblint_lib__Constraints.FromSpec.tf_proc in file "src/framework/constraints.ml", line 650, characters 17-48 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.fold_left2 in file "src/batList.mlv", line 660, characters 39-54 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 734, characters 19-44 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 180, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 234, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 262, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 7-17 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 734, characters 19-44 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 180, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 234, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 262, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 7-17 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 734, characters 19-44 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 180, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 234, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 262, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 7-17 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 734, characters 19-44 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 180, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 234, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 262, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 7-17 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 734, characters 19-44 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 180, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 234, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 262, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 7-17 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 ``` (abbreviated)

This issue appears with 512b6298638b4b14bc1ec58028c97dc600c5b3ac.

[sim642]

I should probably try to make the error-reporting of library functions more informative...

This exception means that some library function call in the program has more arguments than our LibraryFunctions specification for it allows.

[jerhard]

This issue is actually caused by Goblint not knowing what function is called. SQLite keeps a number of library functions in an array. On a function call to a function pointer actually pointing to a wrapper of open (taking three arguments), Goblint cannot exclude that the function call actually targets ftruncate, which takes only two arguments.

[jerhard]

I created a failing test case illustrating this issue.

[sim642]

I guess we should have some kind of function pointer filtering in FromSpec then to assume incompatible ones don't happen. I think the same issue is possible for non-special functions, where enter might get a different number of args than fd.sformals specifies. Right now in base we just zip/combine the difference away...

[jerhard]

Yes, it seems like one could fix this in FromSpec.tf_proc. There is currently no way to determine the number of arguments expected for a LibraryDesc.t, is there?

[sim642]

No, and it's complicated by the fact that there are varargs functions.

But a generic solution both for normal and special functions could be to simply compare the length of args with the number of arguments in the type of f being called. That assumes the declaration in the program has the right number of arguments, but if it doesn't for a special function, then we're doomed either way. This at least allows us to filter out some to prevent problems caused by imprecision.

Special functions don't have a fundec, so there's no way to look at fd.sformals, but the varinfo should still have TFun type with the correct length (and a varargs flag).