Warn & document mismatching CBMC version (#308)

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

kanillian/CBMC_VERSION

@@ -0,0 +1 @@
+5.14.3

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

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))

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 ----------------------------------------------
 

sphinx/index.rst

@@ -14,6 +14,7 @@ Welcome to Gillian
 
    c/index
    js/index
+   kanillian/index
 
 .. toctree::
    :titlesonly:

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.