if function is not in the function map, treat as if it has no body #2636

polgreen · 2018-07-31T06:55:13Z

For the call graph, we add the function to the call graph but do not try to look for function calls in the body.
For slicing global inits, we do not try to look in the function body for symbols.
This fixes issue #2631

polgreen · 2018-07-31T07:23:03Z

I can't access the AWS code build, my AWS account says "No build found
Unable to find build cbmc-windows:9c0f71ed-92dc-4ed1-8ed6-29254ccf3638". Could someone please send me the output?

allredj

Passed Diffblue compatibility checks (cbmc commit: ed33ede).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80457679

allredj

Passed Diffblue compatibility checks (cbmc commit: 9e8d973).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80462217

smowton

Seems fine but the test case is doing lots of stuff that's unrelated to the particular behaviour it's looking to expose

smowton · 2018-07-31T08:58:47Z

regression/goto-instrument/assembly_call_graph_test/main.c

+#define assert(e) __CPROVER_assert(e,"error")
+#endif
+
+volatile int turn; // integer variable to hold the ID of the thread whose turn is it


Can this test case be minimised to do just enough to expose the bug?

smowton · 2018-07-31T09:01:21Z

Test compile failure under Windows was:

Failed test: assembly_call_graph_test
file main.c line 12 function thr1: syntax error before `__volatile__'
PARSING ERROR
EXIT=64
SIGNAL=0

I guess that's a GCC-ism. Trimming the test case should fix it.

polgreen · 2018-07-31T09:11:15Z

The test case is just a copy paste from another regression test; that regression test must have the same gcc error.

I can minimise but I can't make the gcc-ism go away, because the error is due to the line __asm__ __volatile__ ("mfence": : :"memory");, which is the line that makes the reachable call graph fail in develop, and pass with my fix

polgreen · 2018-07-31T09:19:58Z

I've minimised the test; it probably won't fix the AWS CodeBuild problem, but I need to keep the assembly in the test, because that is the bug.

smowton · 2018-07-31T09:30:04Z

Explanation for the failure not happening otherwise: from regression/Makefile:

DIRS = cbmc \
       goto-analyzer \
       ansi-c \
       goto-instrument \
       cpp \
       cbmc-cover \
       goto-instrument-typedef \
       smt2_solver \
       strings \
       invariants \
       goto-diff \
       test-script \
       goto-analyzer-taint \
       goto-gcc \
       goto-cc-cbmc \
       cbmc-cpp \
       goto-cc-goto-analyzer \
       systemc \
       contracts

i.e. the cbmc-concurrency tests are not run by CI.

smowton · 2018-07-31T09:35:43Z

From https://msdn.microsoft.com/en-us/library/5f7adz6y.aspx looks like for Microsoft compilers __asm mfence might suffice.

smowton · 2018-07-31T09:36:52Z

regression/goto-instrument/assembly_call_graph_test/main.c

@@ -0,0 +1,13 @@
+void* thr1(void * arg) {
+ __asm__ __volatile__ ("mfence": : :"memory");


While you're minimising, might as well kill one of the duplicate thr methods

polgreen · 2018-07-31T09:40:34Z

The regression test is valid C code, I would prefer to leave it in the exact format it is in Xen, since that is what I want to compile and run things like slice-global-inits on.

I don't think regression tests should be required to be C code that compiles on windows, if it is valid C code. Otherwise it's impossible to have regression tests for some of the actual CBMC industrial use cases.

Is there a way for me to get access to the output from the Aws Code Build please, without having to request it via GitHub?

smowton · 2018-07-31T09:46:30Z

Sure, do something like

#ifdef __GNUC__
__asm__ __volatile__ ("mfence": : :"memory");
#elif defined(_MSC_VER)
__asm mfence;
#endif

That should test the construct in Xen under GCC and compatible compilers, and as an added bonus test the MSVC syntax for the same thing when testing under Win32

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 6fa41f9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80472665
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: a73b9d8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80473032

For the call graph, we add the function to the call graph but do not try to look for function calls in the body. For slicing global inits, we do not try to look in the function body for symbols. This fixes issue diffblue#2631

polgreen · 2018-07-31T09:52:53Z

Changed.

Perhaps, since 14 of them fail, the CBMC-concurrency tests should be run as part of the regression.

smowton · 2018-07-31T09:57:00Z

Not volunteering for the cleanup, but yes

polgreen · 2018-07-31T10:51:15Z

Ok, this still fails, can I have the output please?

If it is not possible for external collaborators to get access to AWS Code Build output, I think that either:

this should be removed as CI and replaced with something external collaborators can see or
someone that has access to the output should fix the issue in cases where it is something small like this.

The cycle time for debugging is just too great if I have to keep asking people to copy paste the output to GitHub.
cc @kroening

polgreen · 2018-07-31T11:17:01Z

OK, I got the output from Kroening, CBMC doesn't appear to recognise __asm mfence and it doesn't appear in the call graph at all.

That probably needs fixing, but it can't be me that does it. I have replaced the test with a hack so that it should work for windows.

Ideally I need this fix merged without waiting for someone to fix the way CBMC handles __asm mfence, which doesn't sound unreasonable since that is a separate bug.

Diffblue should also want this PR merged since it fixes a bug which otherwise causes the goto-instrument global init slicer to throw an ugly exception.

peterschrammel · 2018-07-31T11:23:49Z

I can't access the AWS code build

smowton · 2018-07-31T11:24:06Z

regression/goto-instrument/assembly_call_graph_test/main.c

+void* thr(void * arg) {
+#ifdef __GNUC__
+__asm__ __volatile__ ("mfence": : :"memory");
+#elif defined(_MSC_VER)


Make this #else in that case

this was a straight copy+paste of the code you put above!

I know, "in that case" was if we're no longer using anything MSVC-specific

peterschrammel · 2018-07-31T11:24:16Z

I can't access the AWS code build

@polgreen, I'll give you access.

smowton · 2018-07-31T11:24:18Z

regression/goto-instrument/assembly_call_graph_test/main.c

+// windows handles assembly code needs to be fixed.
+// CBMC doesn't recognise __asm mfence as a function.
+
+#ifdef _MSC_VER


(and this #ifndef __GNUC__)

allredj

Passed Diffblue compatibility checks (cbmc commit: 6d0776f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80481544

This is a hack, but "__asm__ __volatile__ ("mfence": : :"memory");" doesn't compile on windows and the way CBMC handles "__asm mfence" needs to be fixed. Currently "__asm mfence" is not recognised as a function by CBMC.

polgreen · 2018-07-31T11:32:15Z

changes done

allredj

Passed Diffblue compatibility checks (cbmc commit: ea2d393).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80493788

6a10f1a Merge pull request diffblue#2462 from tautschnig/vs-goto-inline 96fc7b1 Merge pull request diffblue#2654 from peterschrammel/update-jml8 1847066 Update jbmc/lib/java-models-library to java-models-library#8 (remove sun.* imports) c157ba7 Revert "CMake version.cpp: switch back to add_custom_target" 7a009d6 Merge pull request diffblue#2650 from diffblue/aws-codebuild-clcache 63652fc add clcache to Windows build 6f72b3b Merge pull request diffblue#2657 from smowton/smowton/fix/cmake-version-cpp 35d09d5 CMake version.cpp: switch back to add_custom_target 80331d8 Merge pull request diffblue#2638 from diffblue/CBMC_VERSION_string 7c066f9 Merge pull request diffblue#2618 from owen-jones-diffblue/doc/move-irep-docs-from-util-to-irep ad5c375 use a string instead of macro for version number b6258db Merge pull request diffblue#2509 from danpoe/feature/sharing-map-stats eb71a01 Merge pull request diffblue#2639 from thk123/array-element-type c5519ec Merge pull request diffblue#2640 from allredj/support-for-load-containing-class-only 0855872 Address review comments diffblue#2 eaa7664 Wrap lines properly e682eb9 Add \ref in lots of places 3023cca Address review comments 758f069 Move dstringt documentation to above dstringt a54c82d Move documentation of irept to be above irept b827ea4 Use type equality check in unit tests 77185fd Merge pull request diffblue#2607 from jeannielynnmoulton/jeannie/ParseThrownExceptions2 1f4ef40 Add class loader debug output 4ae8eb6 Move sharing map friends declarations to unit tests 186897c Sharing stats for the sharing map 4438b43 Fix sharing map internal assertion 332febe Remove wrong sharing map internal assertions be7e140 Activate internal checks for the sharing map unit tests 713d3fe Merge pull request diffblue#2636 from polgreen/fix_function_map 87f90ee Add replace_all string utility ea2d393 Make test work on windows 4fa9943 Make array element type be not a comment 655248a Add unit test for when there are no exceptions. a6e7c4b Refactors interface for exceptions to not use irepts. 1134bba Creates java_method_typet which extends code_typet aa83622 Unit tests method get_super_class 565c999 Unit tests throws exceptions parsing. eb88509 Use parsed information for thrown exceptions. 5c7dcac Parses the exception attribute 7fcc42d Adds const to get/set_outer_class 5994dd8 Add method to get super class from java class type. fbad2d9 Rename variable extends to super_class 6d0776f if function is not in the function map, treat as if it has no body da86bdb Merge pull request diffblue#2602 from diffblue/__CPROVER_r/w_ok 0202f34 refactor pointer_validity_check using address_check 4a24ad4 use __CPROVER_r/w_ok in string.c library 732ce2a expand __CPROVER_r/w_ok in goto_check acfea65 __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end 0618f7d Merge pull request diffblue#2628 from diffblue/clang-extensions 5e43131 Merge pull request diffblue#2608 from diffblue/ms_cl_int64 7c56091 Merge pull request diffblue#2634 from qaphla/local_bitvector_analysis_regression 44ef8d5 Merge pull request diffblue#2630 from diffblue/invalid-pointer-flattening f74c161 test for __float80 and __float128 8288a72 __float80 is a typedef, not a keyword 5495625 FreeBSD: default flavor is now CLANG e63402e added _Null_unspecified clang extension 16a49a7 bugfix: __float128 3849bb0 rename APPLE flavor to CLANG 060b59c separate pointer check for integer addresses 9b5847e fix flattening of ID_invalid_pointer 432dcf1 Added a regression test checking that --pointer-check does not generate excess checks if local_bitvector_analysis can gather information on the pointer being checked. cbfcc5c added support for _int64 keyword 0148347 Avoid signed/unsigned casts and conversion in goto_inline git-subtree-dir: cbmc git-subtree-split: 6a10f1a

polgreen requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners July 31, 2018 06:55