Merge branch 'diffblue:develop' into develop

Author: jparsert

COMPILING.md

@@ -577,27 +577,12 @@ make test
 
 ## Rust API
 
-CBMC is now offering a [Rust API](src/libcprover-rust/). To build that along with
-CBMC, you need two things:
+CBMC is now offering a [Rust API](src/libcprover-rust/).
 
-- Rust/Cargo, instructions the installation of which can be found [here](https://www.rust-lang.org/tools/install), and
-- CMake (the Rust API doesn't support being built with `Make` yet)
-  - Version `3.19.0`+ is required for the build, because of a dependency on CMake modules
-    that need the higher version themselves.
-
-Provided these two are available, you can perform a CBMC build *including*
-the Rust API by passing in the option `WITH_RUST_API` to `CMake` like this:
-
-```sh
-$ cmake -S. -Bbuild -DWITH_RUST_API=ON <other_options>
-[...]
--- Rust Target: aarch64-apple-darwin
--- Found Rust: /opt/homebrew/bin/rustc (found version "1.66.1") 
--- Using Corrosion as a subdirectory
--- Configuring done
--- Generating done
--- Build files have been written to: cbmc/build
-```
+The Rust API used to be built along with CBMC, but we have since decoupled that
+to be built on its own. Instructions for doing so are in the project's
+[`readme.md`](src/libcprover-rust/readme.md), which are also mirrored
+on the crate's webpage at [crates.io](https://crates.io/crates/libcprover_rust).
 
 If you come across any issues during the configuration or the build of the Rust API,
 please let us know by filing a [bug report](https://github.com/diffblue/cbmc/issues/new)

src/goto-instrument/Makefile

@@ -21,6 +21,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
       contracts/dynamic-frames/dfcc_contract_mode.cpp \
       contracts/dynamic-frames/dfcc_loop_contract_mode.cpp \
+      contracts/dynamic-frames/dfcc_loop_tags.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \

src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.cpp

@@ -0,0 +1,130 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Qinheping Hu, [email protected]
+Author: Remi Delmas, [email protected]
+
+\*******************************************************************/
+
+#include "dfcc_loop_tags.h"
+
+const irep_idt ID_loop_id = "loop-id";
+const irep_idt ID_loop_head = "loop-head";
+const irep_idt ID_loop_body = "loop-body";
+const irep_idt ID_loop_latch = "loop-latch";
+const irep_idt ID_loop_exiting = "loop-exiting";
+const irep_idt ID_loop_top_level = "loop-top-level";
+
+void dfcc_set_loop_id(
+  goto_programt::instructiont::targett &target,
+  const std::size_t loop_id)
+{
+  target->source_location_nonconst().set(ID_loop_id, loop_id);
+}
+
+optionalt<std::size_t>
+dfcc_get_loop_id(const goto_programt::instructiont::targett &target)
+{
+  if(target->source_location_nonconst().get(ID_loop_id).empty())
+    return {};
+
+  return target->source_location_nonconst().get_size_t(ID_loop_id);
+}
+
+bool dfcc_has_loop_id(
+  const goto_programt::instructiont::targett &target,
+  std::size_t loop_id)
+{
+  auto loop_id_opt = dfcc_get_loop_id(target);
+  return loop_id_opt.has_value() && loop_id_opt.value() == loop_id;
+}
+
+static void dfcc_set_loop_tag(
+  goto_programt::instructiont::targett &target,
+  const irep_idt &tag)
+{
+  target->source_location_nonconst().set(tag, true);
+}
+
+static bool has_loop_tag(
+  const goto_programt::instructiont::targett &target,
+  const irep_idt &tag)
+{
+  return target->source_location().get_bool(tag);
+}
+
+void dfcc_set_loop_head(goto_programt::instructiont::targett &target)
+{
+  dfcc_set_loop_tag(target, ID_loop_head);
+}
+
+bool dfcc_is_loop_head(const goto_programt::instructiont::targett &target)
+{
+  return has_loop_tag(target, ID_loop_head);
+}
+
+void dfcc_set_loop_body(goto_programt::instructiont::targett &target)
+{
+  dfcc_set_loop_tag(target, ID_loop_body);
+}
+
+bool dfcc_is_loop_body(const goto_programt::instructiont::targett &target)
+{
+  return has_loop_tag(target, ID_loop_body);
+}
+
+void dfcc_set_loop_exiting(goto_programt::instructiont::targett &target)
+{
+  dfcc_set_loop_tag(target, ID_loop_exiting);
+}
+
+bool dfcc_is_loop_exiting(const goto_programt::instructiont::targett &target)
+{
+  return has_loop_tag(target, ID_loop_exiting);
+}
+
+void dfcc_set_loop_latch(goto_programt::instructiont::targett &target)
+{
+  dfcc_set_loop_tag(target, ID_loop_latch);
+}
+
+bool dfcc_is_loop_latch(const goto_programt::instructiont::targett &target)
+{
+  return has_loop_tag(target, ID_loop_latch);
+}
+
+void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target)
+{
+  dfcc_set_loop_tag(target, ID_loop_top_level);
+}
+
+bool dfcc_is_loop_top_level(const goto_programt::instructiont::targett &target)
+{
+  return has_loop_tag(target, ID_loop_top_level);
+}
+
+void dfcc_remove_loop_tags(source_locationt &source_location)
+{
+  source_location.remove(ID_loop_id);
+  source_location.remove(ID_loop_head);
+  source_location.remove(ID_loop_body);
+  source_location.remove(ID_loop_exiting);
+  source_location.remove(ID_loop_latch);
+  source_location.remove(ID_loop_top_level);
+}
+
+void dfcc_remove_loop_tags(goto_programt::targett &target)
+{
+  dfcc_remove_loop_tags(target->source_location_nonconst());
+}
+
+void dfcc_remove_loop_tags(goto_programt &goto_program)
+{
+  for(auto target = goto_program.instructions.begin();
+      target != goto_program.instructions.end();
+      target++)
+  {
+    dfcc_remove_loop_tags(target);
+  }
+}

src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.h

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking for loop contracts
+
+Author: Qinheping Hu, [email protected]
+Author: Remi Delmas, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Functions that allow to tag GOTO instructions with loop identifiers and
+/// loop instruction type: head, body, exiting, latch.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
+
+#include <goto-programs/goto_program.h>
+
+void dfcc_set_loop_id(
+  goto_programt::instructiont::targett &target,
+  std::size_t loop_id);
+
+bool dfcc_has_loop_id(
+  const goto_programt::instructiont::targett &target,
+  std::size_t loop_id);
+
+optionalt<std::size_t>
+dfcc_get_loop_id(const goto_programt::instructiont::targett &target);
+
+void dfcc_set_loop_head(goto_programt::instructiont::targett &target);
+bool dfcc_is_loop_head(const goto_programt::instructiont::targett &target);
+
+void dfcc_set_loop_body(goto_programt::instructiont::targett &target);
+bool dfcc_is_loop_body(const goto_programt::instructiont::targett &target);
+
+void dfcc_set_loop_exiting(goto_programt::instructiont::targett &target);
+bool dfcc_is_loop_exiting(const goto_programt::instructiont::targett &target);
+
+void dfcc_set_loop_latch(goto_programt::instructiont::targett &target);
+bool dfcc_is_loop_latch(const goto_programt::instructiont::targett &target);
+
+void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target);
+bool dfcc_is_loop_top_level(const goto_programt::instructiont::targett &target);
+
+void dfcc_remove_loop_tags(source_locationt &source_location);
+void dfcc_remove_loop_tags(goto_programt &goto_program);
+void dfcc_remove_loop_tags(goto_programt::targett &target);
+#endif