Proof fails on OSX 10.15 that worked earlier versions #5388

danielsn · 2020-06-22T14:08:08Z

CBMC version: 5.12 (cbmc-5.12.1)
Operating system:

ProductName:	Mac OS X
ProductVersion:	10.15.4
BuildVersion:	19E287

Exact command line resulting in the issue:
clone https://github.com/awslabs/aws-c-common/tree/master/.cbmc-batch/jobs/aws_array_list_get_at_ptr

➜  aws_array_list_get_at_ptr git:(master) time make report
echo "Setting up dependencies"
Setting up dependencies
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/source/
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/source/
echo /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/proof_allocators.c
/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/proof_allocators.c
goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/proof_allocators.c --export-function-local-symbols  \
	  -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/source/proof_allocators.goto \
	  2>&1 | tee /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/source/proof_allocators.log ; exit ${PIPESTATUS[0]}
The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/source/
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/source/
echo /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/make_common_data_structures.c
/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/make_common_data_structures.c
goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/make_common_data_structures.c --export-function-local-symbols  \
	  -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/source/make_common_data_structures.goto \
	  2>&1 | tee /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/source/make_common_data_structures.log ; exit ${PIPESTATUS[0]}
The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/source/
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/source/
echo /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/utils.c
/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/utils.c
goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/utils.c --export-function-local-symbols  \
	  -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/source/utils.goto \
	  2>&1 | tee /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/source/utils.log ; exit ${PIPESTATUS[0]}
The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.
/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/utils.c: In function 'uninterpreted_compare':
/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/source/utils.c:134:1: warning: function '__CPROVER_uninterpreted_hasher' is not declared
         __CPROVER_assume(__CPROVER_uninterpreted_hasher(a) == __CPROVER_uninterpreted_hasher(b));
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/stubs/
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/stubs/
echo /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/stubs/error.c
/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/stubs/error.c
goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/stubs/error.c --export-function-local-symbols  \
	  -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/stubs/error.goto \
	  2>&1 | tee /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/stubs/error.log ; exit ${PIPESTATUS[0]}
The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/stubs/
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/stubs/
echo /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/stubs/memcpy_override.c
/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/stubs/memcpy_override.c
goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/stubs/memcpy_override.c --export-function-local-symbols  \
	  -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/.cbmc-batch/stubs/memcpy_override.goto \
	  2>&1 | tee /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/.cbmc-batch/stubs/memcpy_override.log ; exit ${PIPESTATUS[0]}
The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/source/
echo /Users/dsn/ws/C-Common/aws-c-common/source/array_list.c
/Users/dsn/ws/C-Common/aws-c-common/source/array_list.c
goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/source/array_list.c --export-function-local-symbols  \
	  -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/array_list.goto \
	  2>&1 | tee /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/source/array_list.log ; exit ${PIPESTATUS[0]}
The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/
mkdir -p /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/source/
echo /Users/dsn/ws/C-Common/aws-c-common/source/common.c
/Users/dsn/ws/C-Common/aws-c-common/source/common.c
goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/source/common.c --export-function-local-symbols  \
	  -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8 -DCBMC=1 -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/common.goto \
	  2>&1 | tee /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/logs/source/common.log ; exit ${PIPESTATUS[0]}
The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.
/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/dispatch/queue.h:812:1: error: syntax error before ':'
 DISPATCH_ENUM(dispatch_autorelease_frequency, unsigned long,
PARSING ERROR
make: *** [/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/common.goto] Error 1
make report  1.43s user 0.72s system 93% cpu 2.288 total

What behaviour did you expect:
CBMC to compile the file
What happened instead:
It failed with a PARSING ERROR

Note that we can get this to run using gcc but fails with goto-cc. I had to remove a couple flags gcc didn't know about, but this seems to be a minimal test case

➜  aws_array_list_get_at_ptr git:(master) gcc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/source/common.c \
          -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8  -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/common.goto  
➜  aws_array_list_get_at_ptr git:(master) goto-cc -Wall -c /Users/dsn/ws/C-Common/aws-c-common/source/common.c \
          -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8  -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/common.goto
/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/dispatch/queue.h:812:1: error: syntax error before ':'
 DISPATCH_ENUM(dispatch_autorelease_frequency, unsigned long,
PARSING ERROR

The text was updated successfully, but these errors were encountered:

danielsn · 2020-06-22T14:08:41Z

@danpoe @tautschnig @karkhaz

danielsn · 2020-06-22T14:10:18Z

Note: the relevant section of queue.h is

/*!
 * @typedef dispatch_autorelease_frequency_t
 * Values to pass to the dispatch_queue_attr_make_with_autorelease_frequency()
 * function.
 *
 * @const DISPATCH_AUTORELEASE_FREQUENCY_INHERIT
 * Dispatch queues with this autorelease frequency inherit the behavior from
 * their target queue. This is the default behavior for manually created queues.
 *
 * @const DISPATCH_AUTORELEASE_FREQUENCY_WORK_ITEM
 * Dispatch queues with this autorelease frequency push and pop an autorelease
 * pool around the execution of every block that was submitted to it
 * asynchronously.
 * @see dispatch_queue_attr_make_with_autorelease_frequency().
 *
 * @const DISPATCH_AUTORELEASE_FREQUENCY_NEVER
 * Dispatch queues with this autorelease frequency never set up an individual
 * autorelease pool around the execution of a block that is submitted to it
 * asynchronously. This is the behavior of the global concurrent queues.
 */
DISPATCH_ENUM(dispatch_autorelease_frequency, unsigned long,
	DISPATCH_AUTORELEASE_FREQUENCY_INHERIT DISPATCH_ENUM_API_AVAILABLE(
			macos(10.12), ios(10.0), tvos(10.0), watchos(3.0)) = 0,
	DISPATCH_AUTORELEASE_FREQUENCY_WORK_ITEM DISPATCH_ENUM_API_AVAILABLE(
			macos(10.12), ios(10.0), tvos(10.0), watchos(3.0)) = 1,
	DISPATCH_AUTORELEASE_FREQUENCY_NEVER DISPATCH_ENUM_API_AVAILABLE(
			macos(10.12), ios(10.0), tvos(10.0), watchos(3.0)) = 2,
);

danielsn · 2020-06-22T14:11:17Z

https://opensource.apple.com/source/libdispatch/libdispatch-685/dispatch/queue.h.auto.html

danielsn · 2020-06-22T14:53:23Z

common.preprocessed.txt

generated with

goto-cc -E -Wall -c /Users/dsn/ws/C-Common/aws-c-common/source/common.c \
          -I/Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/include/ -I/Users/dsn/ws/C-Common/aws-c-common/include/ -DMAX_ITEM_SIZE=2 -DMAX_INITIAL_ITEM_ALLOCATION=9223372036854775808ULL -DCBMC_OBJECT_BITS=8  -DAWS_DEEP_CHECKS=0 -o /Users/dsn/ws/C-Common/aws-c-common/.cbmc-batch/jobs/aws_array_list_get_at_ptr/gotos/source/common.goto

tautschnig · 2020-06-22T21:05:25Z

@danielsn Would GCC/Clang on Catalina actually accept that input? Doing clang -xc ../common.preprocessed.txt throws the same errors for me (which is as expected, as code like typedef enum : unsigned long { A } some_type; is valid C++ 11, but not actually valid C.

tautschnig · 2020-06-22T21:18:54Z

@danielsn Can you check whether your GCC/Clang accepts

typedef enum : unsigned long { A } some_type;

int main()
{
}

?

Even https://clang.llvm.org/docs/LanguageExtensions.html#enumerations-with-a-fixed-underlying-type suggests this is for Objective C, but perhaps this slipped into a C source nonetheless.

danielsn · 2020-06-23T00:22:04Z

@tautschnig It runs with no errors

➜  temp clang --version
Apple clang version 11.0.3 (clang-1103.0.32.62)
Target: x86_64-apple-darwin19.4.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

danielsn · 2020-06-23T00:22:35Z

➜  temp cat 5388.c
#include <stdio.h>

typedef enum : unsigned long { A } some_type;

int main()
{
  printf("hello world\n");
}
➜  temp clang 5388.c 
➜  temp ./a.out 
hello world

hannes-steffenhagen-diffblue · 2020-06-26T09:04:05Z

Yes this appears to be a clang extension. We’ll have to check if/how we can support it in the frontend (not sure off the top of my head if our enum representation has an easy way to change the underlying type, but it shouldn’t be too hard).

thk123 · 2020-07-03T16:09:13Z

We are currently investigating how to implement this in the C front end for CBMC.

hannes-steffenhagen-diffblue · 2020-07-23T12:33:23Z

We now have a PR for supporting the syntax, but not yet the semantics (i.e. you’ll no longer get a parse error, but the underlying type won’t be correct).

Also interesting to note that the clang support for this is rather new (less than 2 years old apparently) and has some interesting quirks, like syntax like this

enum X : uint32_t {A};
enum X : uint16_t V = A;

works, sort of – the underlying spec of uint16_t is just completely ignored in the variable declaration.

Fully supporting this will take a bit longer, but in the meantime the syntax changes might be enough to run certain proofs on OSX again already.

danpoe · 2020-07-23T12:40:49Z

Also cbmc warns about the fact that in e.g. enum enum1 : unsigned { X, Y} the underlying type specification (here unsigned) is ignored.

hannes-steffenhagen-diffblue · 2020-07-31T08:29:17Z

@danielsn We believe this will be fixed once #5438 is merged.

hannes-steffenhagen-diffblue · 2020-08-06T13:08:25Z

@danielsn We believe this is fixed on latest develop, therefore we’re closing this for now.

danielsn added the aws Bugs or features of importance to AWS CBMC users label Jun 22, 2020

danielsn added the aws-high label Jul 23, 2020

hannes-steffenhagen-diffblue closed this as completed Aug 6, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Proof fails on OSX 10.15 that worked earlier versions #5388

Proof fails on OSX 10.15 that worked earlier versions #5388

danielsn commented Jun 22, 2020

danielsn commented Jun 22, 2020

Uh oh!

danielsn commented Jun 22, 2020

Uh oh!

danielsn commented Jun 22, 2020

Uh oh!

danielsn commented Jun 22, 2020 •

edited

Loading

Uh oh!

tautschnig commented Jun 22, 2020

Uh oh!

tautschnig commented Jun 22, 2020

Uh oh!

danielsn commented Jun 23, 2020

Uh oh!

danielsn commented Jun 23, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Jun 26, 2020

Uh oh!

thk123 commented Jul 3, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Jul 23, 2020 •

edited

Loading

Uh oh!

danpoe commented Jul 23, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Jul 31, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Aug 6, 2020

Uh oh!

Proof fails on OSX 10.15 that worked earlier versions #5388

Proof fails on OSX 10.15 that worked earlier versions #5388

Comments

danielsn commented Jun 22, 2020

danielsn commented Jun 22, 2020

Uh oh!

danielsn commented Jun 22, 2020

Uh oh!

danielsn commented Jun 22, 2020

Uh oh!

danielsn commented Jun 22, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Jun 22, 2020

Uh oh!

tautschnig commented Jun 22, 2020

Uh oh!

danielsn commented Jun 23, 2020

Uh oh!

danielsn commented Jun 23, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Jun 26, 2020

Uh oh!

thk123 commented Jul 3, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Jul 23, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

danpoe commented Jul 23, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Jul 31, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Aug 6, 2020

Uh oh!

danielsn commented Jun 22, 2020 •

edited

Loading

hannes-steffenhagen-diffblue commented Jul 23, 2020 •

edited

Loading