Merge pull request #5432 from natasha-jeppu/byte-extract-update-pr

CBMC additional profiling info: byte extract, update metrics

Author: NlightNFotis

regression/cbmc/byte-op-metric/main.c

@@ -0,0 +1,11 @@
+typedef unsigned char BYTE;
+
+int main()
+{
+  unsigned int value;
+  BYTE *bp = (BYTE *)(&value);
+
+  bp[0] = bp[2];
+  assert(1);
+  return 0;
+}

regression/cbmc/byte-op-metric/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--show-byte-ops
+^EXIT=0$
+^SIGNAL=0$
+^Byte Extracts:$
+^.*main\.c line 8 function main$
+^.* byte\_extract\_little\_endian\(.*\)$
+^Number of byte extracts: 1$
+^Byte Updates:$
+^.*main\.c line 8 function main$
+^.* byte\_update\_little\_endian\(.*\)$
+^Number of byte updates: 1$
+--
+--
+To test --show-byte-ops option that displays byte extract and update metrics.

regression/cbmc/byte-op-metric/test_json.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show-byte-ops --json-ui
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+"byteOpsStats": \{\n\s*"byteExtractStats": \{\n\s*"byteExtractList": \[\n\s*\{\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"ssaExpr": \{(\n.*)*\},\n\s*"ssaExprString": ".* .* byte\_extract\_little\_endian\(.*\)"\n\s*\}\n\s*\],\n\s*"numOfExtracts": 1\n\s*\},\n\s*"byteUpdateStats": \{\n\s*"byteUpdateList": \[\n\s*\{\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"ssaExpr": \{(\n.*)*\},\n\s*"ssaExprString": ".* .* byte\_update\_little\_endian\(.*\)"\n\s*\}\n\s*\],\n\s*"numOfUpdates": 1\n\s*\}
+--
+--
+To test json output for --show-byte-ops option that displays byte extract and update metrics.

src/cbmc/cbmc_parse_options.cpp

@@ -198,6 +198,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
 
+  if(cmdline.isset("show-byte-ops"))
+    options.set_option("show-byte-ops", true);
+
   if(cmdline.isset("show-vcc"))
     options.set_option("show-vcc", true);
 
@@ -640,7 +643,8 @@ int cbmc_parse_optionst::doit()
 
   if(
     options.get_bool_option("program-only") ||
-    options.get_bool_option("show-vcc"))
+    options.get_bool_option("show-vcc") ||
+    options.get_bool_option("show-byte-ops"))
   {
     if(options.get_bool_option("paths"))
     {

src/goto-checker/bmc_util.h

@@ -173,6 +173,7 @@ void run_property_decider(
 // clang-format off
 #define OPT_BMC \
   "(program-only)" \
+  "(show-byte-ops)" \
   "(show-loops)" \
   "(show-vcc)" \
   "(show-goto-symex-steps)" \
@@ -203,6 +204,7 @@ void run_property_decider(
   " --show-goto-symex-steps      show which steps symex travels, includes " \
   "                              diagnostic information\n" \
   " --program-only               only show program expression\n" \
+  " --show-byte-ops              show all byte extracts and updates\n" \
   " --show-loops                 show the loops in the program\n" \
   " --depth nr                   limit search depth\n" \
   " --max-field-sensitivity-array-size M\n" \

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -59,6 +59,11 @@ operator()(propertiest &properties)
     show_program(ns, equation);
   }
 
+  if(options.get_bool_option("show-byte-ops"))
+  {
+    show_byte_ops(options, ui_message_handler, ns, equation);
+  }
+
   resultt result(resultt::progresst::DONE);
   update_properties(properties, result.updated_properties);
   return result;

src/goto-checker/single_path_symex_only_checker.cpp

@@ -127,6 +127,9 @@ void single_path_symex_only_checkert::equation_output(
   if(options.get_bool_option("program-only"))
     show_program(ns, equation);
 
+  if(options.get_bool_option("show-byte-ops"))
+    show_byte_ops(options, ui_message_handler, ns, equation);
+
   if(options.get_bool_option("validate-ssa-equation"))
   {
     symex.validate(validation_modet::INVARIANT);

src/goto-diff/goto_diff_parse_options.cpp

@@ -83,6 +83,9 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
 
+  if(cmdline.isset("show-byte-ops"))
+    options.set_option("show-byte-ops", true);
+
   if(cmdline.isset("show-vcc"))
     options.set_option("show-vcc", true);