From cff2c703d48be9c11707067c6921a42319d8951c Mon Sep 17 00:00:00 2001
From: Nat Karmios <nat@karmios.com>
Date: Mon, 5 Aug 2024 17:49:56 +0100
Subject: [PATCH] Warn & document mismatching CBMC version (#308)

---
 GillianCore/lib/gillian.ml          |  3 +++
 kanillian/CBMC_VERSION              |  1 +
 kanillian/lib/KParserAndCompiler.ml | 28 ++++++++++++++++++++++++++++
 kanillian/lib/dune                  |  9 +++++++++
 sphinx/conf.py                      |  7 +++++++
 sphinx/index.rst                    |  1 +
 sphinx/kanillian/index.rst          | 14 ++++++++++++++
 7 files changed, 63 insertions(+)
 create mode 100644 kanillian/CBMC_VERSION
 create mode 100644 sphinx/kanillian/index.rst

diff --git a/GillianCore/lib/gillian.ml b/GillianCore/lib/gillian.ml
index 3f2c5ac63..afff66534 100644
--- a/GillianCore/lib/gillian.ml
+++ b/GillianCore/lib/gillian.ml
@@ -105,6 +105,9 @@ module Logging = struct
     Use this when you need a pretty printer,
     but don't expect it to actually be seen anywhere *)
   let dummy_pp = dummy_pp
+
+  (** Prints a message to all available reporters, and stdout if applicable. *)
+  let print_to_all = print_to_all
 end
 
 module IncrementalAnalysis = IncrementalAnalysis
diff --git a/kanillian/CBMC_VERSION b/kanillian/CBMC_VERSION
new file mode 100644
index 000000000..7f3588a1d
--- /dev/null
+++ b/kanillian/CBMC_VERSION
@@ -0,0 +1 @@
+5.14.3
\ No newline at end of file
diff --git a/kanillian/lib/KParserAndCompiler.ml b/kanillian/lib/KParserAndCompiler.ml
index f095a1f16..8e9befcb2 100644
--- a/kanillian/lib/KParserAndCompiler.ml
+++ b/kanillian/lib/KParserAndCompiler.ml
@@ -88,7 +88,35 @@ let create_compilation_result path goto_prog gil_prog =
     init_data = ();
   }
 
+let cbmc_version_checked = ref false
+
+let check_cbmc_version () =
+  if not !cbmc_version_checked then
+    let () = cbmc_version_checked := true in
+    let expected_cbmc_version = Cbmc_version.expected in
+    let cbmc_version =
+      let inp = Unix.open_process_in "cbmc --version" in
+      let r = In_channel.input_all inp in
+      let () =
+        match Unix.close_process_in inp with
+        | Unix.WEXITED 0 -> ()
+        | _ ->
+            failwith
+              "Failed to check CBMC version! Make sure CBMC is installed."
+      in
+      r |> String.trim |> String.split_on_char ' ' |> List.hd
+    in
+    if cbmc_version <> expected_cbmc_version then
+      let msg =
+        Fmt.str
+          "WARNING: expected CBMC version %s, but found %s. There may be \
+           consequences!"
+          expected_cbmc_version cbmc_version
+      in
+      Logging.print_to_all msg
+
 let compile_c_to_symtab c_file =
+  let () = check_cbmc_version () in
   let symtab_file = c_file ^ ".symtab.json" in
   let status =
     Sys.command
diff --git a/kanillian/lib/dune b/kanillian/lib/dune
index 9ef2be0a5..47857e06b 100644
--- a/kanillian/lib/dune
+++ b/kanillian/lib/dune
@@ -10,6 +10,15 @@
   dune-site)
  (flags :standard -open Goto_lib))
 
+(rule
+ (target cbmc_version.ml)
+ (deps
+  (file ../CBMC_VERSION))
+ (action
+  (with-stdout-to
+   %{target}
+   (bash "echo let expected = \\\"$(cat %{deps})\\\""))))
+
 (generate_sites_module
  (module runtime_sites)
  (sites kanillian))
diff --git a/sphinx/conf.py b/sphinx/conf.py
index abf24abdb..d959acf0b 100644
--- a/sphinx/conf.py
+++ b/sphinx/conf.py
@@ -92,6 +92,13 @@
 # If true, `todo` and `todoList` produce output, else they produce nothing.
 todo_include_todos = False
 
+cbmc_version = None
+with open("../kanillian/CBMC_VERSION", "r") as f:
+    cbmc_version = f.read().strip()
+# https://stackoverflow.com/a/39214302
+rst_epilog = f"""
+.. |cbmc_version| replace:: {cbmc_version}
+"""
 
 # -- Options for HTML output ----------------------------------------------
 
diff --git a/sphinx/index.rst b/sphinx/index.rst
index b68cbee55..521cae439 100644
--- a/sphinx/index.rst
+++ b/sphinx/index.rst
@@ -14,6 +14,7 @@ Welcome to Gillian
 
    c/index
    js/index
+   kanillian/index
 
 .. toctree::
    :titlesonly:
diff --git a/sphinx/kanillian/index.rst b/sphinx/kanillian/index.rst
new file mode 100644
index 000000000..846d54579
--- /dev/null
+++ b/sphinx/kanillian/index.rst
@@ -0,0 +1,14 @@
+Kanillian (New Gillian-C)
+=========================
+
+.. danger::
+
+  Kanillian is currently in development and unstable.
+
+Kanillian is a new instantiation of Gillian to the C language (or more precisely, CBMC's `GOTO-C <https://diffblue.github.io/cbmc/group__goto-programs.html>`_). It can be found in the ``kanillian`` folder of the repository.
+
+Kanillian requires CBMC to be present on your path.
+
+.. attention::
+
+  Kanillian is currently built to work with CBMC version |cbmc_version| - newer versions are known to cause problems.
\ No newline at end of file