Merge branch 'diffblue:develop' into loop_invariant_synthesis

Author: qinheping

CMakeLists.txt

@@ -157,6 +157,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
               "$<TARGET_FILE:goto-cc>"
               "$<TARGET_FILE:goto-diff>"
               "$<TARGET_FILE:goto-instrument>"
+              "$<TARGET_FILE:goto-synthesizer>"
               "$<TARGET_FILE:janalyzer>"
               "$<TARGET_FILE:jbmc>"
               "$<TARGET_FILE:jdiff>"
@@ -215,6 +216,7 @@ cprover_default_properties(
     cbmc
     cbmc-lib
     cpp
+    cprover-api-cpp
     cprover
     cprover-lib
     crangler
@@ -232,6 +234,8 @@ cprover_default_properties(
     goto-instrument-lib
     goto-programs
     goto-symex
+    goto-synthesizer
+    goto-synthesizer-lib
     jsil
     json
     json-symtab-language

CODEOWNERS

@@ -44,7 +44,7 @@
 /jbmc/src/java_bytecode/ @romainbrenguier @peterschrammel
 /src/analyses/ @martin-cs @peterschrammel @chris-ryder
 /src/pointer-analysis/ @martin-cs @peterschrammel @chris-ryder
-
+/src/libcprover-cpp @NlightNFotis @thomasspriggs @esteffin @TGWDB @peterschrammel
 
 # These files change frequently and changes are medium-risk
 
@@ -53,6 +53,7 @@
 /src/goto-instrument/ @martin-cs @chris-ryder @peterschrammel @tautschnig @kroening
 /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-instrument/synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
+/src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-diff/ @tautschnig @peterschrammel
 /src/jsil/ @kroening @tautschnig
 /src/memory-analyzer/ @tautschnig @chris-ryder @kroening

doc/man/goto-synthesizer.1

@@ -0,0 +1,40 @@
+.TH GOTO-SYNTHESIZER "1" "December 2022" "goto-synthesizer-5.59.0" "User Commands"
+.SH NAME
+goto\-synthesizer \- Synthesize and apply loop contracts of goto binaries.
+.SH SYNOPSIS
+.TP
+.B goto\-synthesizer [\-?] [\-h] [\-\-help]
+show help
+.TP
+.B goto\-synthesizer \-\-version
+show version and exit
+.TP
+.B goto\-synthesizer [options] \fIin\fR [\fIout\fR]
+perform synthesis and loop-contracts transformation
+.SH DESCRIPTION
+\fBgoto-synthesis\fR reads a GOTO binary, performs loop-contracts synthesis and
+program transformation for the synthesized contracts, and then writes the
+resulting program as GOTO binary on disk.
+.SH OPTIONS
+.SS "User-interface options:"
+.TP
+\fB\-\-xml\-ui\fR
+use XML\-formatted output
+.TP
+\fB\-\-json\-ui\fR
+use JSON\-formatted output
+.TP
+\fB\-\-verbosity\fR \fIn\fR
+verbosity level
+.SH ENVIRONMENT
+All tools honor the TMPDIR environment variable when generating temporary
+files and directories.
+.SH BUGS
+If you encounter a problem please create an issue at
+.B https://github.com/diffblue/cbmc/issues
+.SH SEE ALSO
+.BR cbmc (1),
+.BR goto-cc (1)
+.BR goto-instrument (1)
+.SH COPYRIGHT
+2022, Qinheping Hu

regression/CMakeLists.txt

@@ -85,6 +85,7 @@ add_subdirectory(goto-interpreter)
 add_subdirectory(cbmc-sequentialization)
 add_subdirectory(cpp-linter)
 add_subdirectory(catch-framework)
+add_subdirectory(libcprover-cpp)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)

regression/ansi-c/gcc_attribute_used1/main.c

@@ -0,0 +1,6 @@
+static int foo __attribute__((used)) = 42;
+
+int main()
+{
+  return 0;
+}

regression/ansi-c/gcc_attribute_used1/other.c

@@ -0,0 +1,15 @@
+struct bar
+{
+  char *ptr;
+};
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data")));
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data"))) = {0};
+
+void use_foo()
+{
+  __CPROVER_assert(foo.ptr == 0, "null");
+}

regression/cbmc-library/Float_lib2/test.desc renamed to regression/ansi-c/gcc_attribute_used1/test.desc

@@ -1,8 +1,8 @@
-CORE
+CORE gcc-only
 main.c
---floatbv
+other.c
 ^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc-concurrency/thread_chain_cbmc1/main.c

@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-concurrency/thread_chain_cbmc2/main.c

@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c renamed to regression/cbmc-incr-smt2/pointers-conversions/byte_extract.c

@@ -6,7 +6,7 @@ int main()
   uint32_t input;
   uint32_t original = input;
   uint8_t *ptr = (uint8_t *)(&input);
-  assert(*ptr == 0); // falsifiable
+  assert(*ptr != 42); // falsifiable
   *ptr = ~(*ptr);
   assert(input != original); // valid
 }

regression/cbmc-incr-smt2/pointers-conversions/byte_extract.desc

@@ -0,0 +1,19 @@
+CORE
+byte_extract.c
+--trace
+Running incremental SMT2 solving via
+Building error trace
+\[main\.assertion\.\d+\] line \d+ assertion \*ptr != 42: FAILURE
+\[main\.assertion\.\d+\] line \d+ assertion input != original: SUCCESS
+  input=42ul? \(00000000 00000000 00000000 00101010\)
+  original=42ul? \(00000000 00000000 00000000 00101010\)
+Violated property:
+  file byte_extract.c function main line \d+ thread \d+
+  assertion \*ptr != 42
+^EXIT=10$
+^SIGNAL=0$
+--
+Reached unimplemented Generation of SMT formula for byte extract expression: byte_extract_little_endian
+--
+This test is here to document our lack of support for byte_extract_little_endian
+in the pointers support for the new SMT backend.

regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.desc

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint32_t x = 0u;
+  uint8_t *ptr = (uint8_t *)(&x);
+  uint32_t offset;
+  __CPROVER_assume(offset >= 0u && offset < 4u);
+  *(ptr + offset) = 1u;
+  assert(x != 256u);
+}

regression/cbmc-incr-smt2/pointers-conversions/byte_update.c

@@ -0,0 +1,23 @@
+CORE
+byte_update.c
+--trace
+Running incremental SMT2 solving via
+Building error trace
+\[main\.assertion\.\d+\] line \d+ assertion x != 256u: FAILURE
+State \d+ file byte_update\.c function main line \d+ thread \d
+  offset=1ul? \(00000000 00000000 00000000 00000001\)
+Assumption:
+  file byte_update\.c line \d+ function main
+  offset >= 0u && offset < 4u
+State \d+ file byte_update\.c function main line \d+ thread \d+
+  byte_extract_little_endian\(x, \(signed long( long)? int\)offset, uint8_t\)=1 \(00000001\)
+Violated property:
+  file byte_update.c function main line \d+ thread \d+
+  assertion x != 256u
+^EXIT=10$
+^SIGNAL=0$
+--
+Reached unimplemented Generation of SMT formula for byte extract expression: byte_update_little_endian
+--
+This test is here to document our lack of support for byte_update_little_endian
+in the pointers support for the new SMT backend.