From 1161a44501abbe80efb0d5450b542b167879b403 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 22 Jun 2024 11:54:53 -0700
Subject: [PATCH] JSON output for the properties

This adds --json-properties, to get a JSON array with all the properties.
---
 regression/ebmc/CLI/json-properties.desc | 18 +++++++++
 regression/ebmc/CLI/json-properties.v    |  5 +++
 src/ebmc/ebmc_base.cpp                   |  6 +++
 src/ebmc/ebmc_base.h                     |  1 +
 src/ebmc/ebmc_parse_options.h            |  3 +-
 src/ebmc/show_properties.cpp             | 51 +++++++++++++++++++++++-
 6 files changed, 81 insertions(+), 3 deletions(-)
 create mode 100644 regression/ebmc/CLI/json-properties.desc
 create mode 100644 regression/ebmc/CLI/json-properties.v

diff --git a/regression/ebmc/CLI/json-properties.desc b/regression/ebmc/CLI/json-properties.desc
new file mode 100644
index 000000000..efb427813
--- /dev/null
+++ b/regression/ebmc/CLI/json-properties.desc
@@ -0,0 +1,18 @@
+CORE
+json-properties.v
+--json-properties -
+activate-multi-line-match
+\[
+  \{
+    "description": "",
+    "location": \{
+      "file": "json-properties\.v",
+      "line": "3",
+      "workingDirectory": ".*"
+    \},
+    "name": "main\.property\.p0"
+  \}
+\]
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/CLI/json-properties.v b/regression/ebmc/CLI/json-properties.v
new file mode 100644
index 000000000..4156b0a82
--- /dev/null
+++ b/regression/ebmc/CLI/json-properties.v
@@ -0,0 +1,5 @@
+module main;
+
+  always assert p0: 1 == 2;
+
+endmodule
diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
index 72c21c606..a3cc292a4 100644
--- a/src/ebmc/ebmc_base.cpp
+++ b/src/ebmc/ebmc_base.cpp
@@ -338,6 +338,12 @@ int ebmc_baset::get_properties()
     return 0;
   }
 
+  if(cmdline.isset("json-properties"))
+  {
+    json_properties(cmdline.get_value("json-properties"));
+    return 0;
+  }
+
   return -1; // done
 }
 
diff --git a/src/ebmc/ebmc_base.h b/src/ebmc/ebmc_base.h
index dc62d8ae4..2f878269a 100644
--- a/src/ebmc/ebmc_base.h
+++ b/src/ebmc/ebmc_base.h
@@ -52,6 +52,7 @@ class ebmc_baset
   bool parse_property(const std::string &property);
   bool get_model_properties();
   void show_properties();
+  void json_properties(const std::string &file_name);
 
   bool parse();
   bool parse(const std::string &filename);
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
index 29e45304e..4e798052a 100644
--- a/src/ebmc/ebmc_parse_options.h
+++ b/src/ebmc/ebmc_parse_options.h
@@ -32,7 +32,8 @@ class ebmc_parse_optionst:public parse_options_baset
         "(show-properties)(property):p:(trace)(waveform)(numbered-trace)"
         "(dimacs)(module):(top):"
         "(po)(cegar)(k-induction)(2pi)(bound2):"
-        "(outfile):(xml-ui)(verbosity):(gui)(json-result):"
+        "(outfile):(xml-ui)(verbosity):(gui)"
+        "(json-result):(json-properties):"
         "(neural-liveness)(neural-engine):"
         "(reset):"
         "(version)(verilog-rtl)(verilog-netlist)"
diff --git a/src/ebmc/show_properties.cpp b/src/ebmc/show_properties.cpp
index aa9e691c1..292024ca0 100644
--- a/src/ebmc/show_properties.cpp
+++ b/src/ebmc/show_properties.cpp
@@ -6,12 +6,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <iostream>
-
+#include <util/json.h>
+#include <util/json_irep.h>
+#include <util/unicode.h>
 #include <util/xml.h>
 #include <util/xml_irep.h>
 
 #include "ebmc_base.h"
+#include "ebmc_error.h"
+
+#include <iostream>
 
 /*******************************************************************\
 
@@ -62,3 +66,46 @@ void ebmc_baset::show_properties()
     p_nr++;
   }
 }
+
+/*******************************************************************\
+
+Function: ebmc_baset::json_properties
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void ebmc_baset::json_properties(const std::string &file_name)
+{
+  json_arrayt json;
+
+  for(const auto &p : properties.properties)
+  {
+    json_objectt json_property;
+    json_property["identifier"] = json_stringt{id2string(p.identifier)};
+    json_property["name"] = json_stringt{id2string(p.name)};
+    json_property["description"] = json_stringt{p.description};
+
+    if(p.location.is_not_nil())
+      json_property["location"] = ::json(p.location);
+
+    json.push_back(std::move(json_property));
+  }
+
+  if(file_name == "-")
+  {
+    std::cout << json;
+  }
+  else
+  {
+    std::ofstream out(widen_if_needed(file_name));
+    if(!out)
+      throw ebmc_errort() << "failed to open " << file_name;
+
+    out << json;
+  }
+}