Updating imp.md, kore tests and kore-proof-trace to parse side co…

…ndition events (#1032)

This PR fixes Pi-Squared-Inc/pi2#1348. This
issue reports that `kore-proof-trace` doesn't generate any hints when a
`requires` clause is used in an example.

After investigating the issue, we realized that our regression tests
didn't cover this case. Therefore, we updated the current `imp-*.kore`
tests to contain it. We also updated `imp.md` to be compatible with K
v7.0.15. To improve the reproducibility of our tests in the future, we
made `imp.md` the source code of `imp.kore`, `imp-proof.kore`, and
`imp-slow-proof.kore`.

Then, we needed to update the Proof Hints version and the
`kore-proof-trace` tool to include "side condition" events as arguments
and parse them appropriately to hints for the `requires` clause and the
rest of the test.

docs/proof-trace.md

@@ -40,6 +40,8 @@ event             ::= hook
 argument          ::= hook
                     | function
                     | rule
+                    | side_cond_entry
+                    | side_cond_exit
                     | kore_term
 
 name              ::= string

include/kllvm/binary/ProofTraceParser.h

@@ -260,7 +260,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 8U;
+  static constexpr uint32_t expected_version = 9U;
 
 private:
   bool verbose_;
@@ -631,6 +631,24 @@ class proof_trace_parser {
       return true;
     }
 
+    case side_condition_event_sentinel: {
+      auto side_condition_event = parse_side_condition(ptr, end);
+      if (!side_condition_event) {
+        return false;
+      }
+      event.set_step_event(side_condition_event);
+      return true;
+    }
+
+    case side_condition_end_sentinel: {
+      auto side_condition_end_event = parse_side_condition_end(ptr, end);
+      if (!side_condition_end_event) {
+        return false;
+      }
+      event.set_step_event(side_condition_end_event);
+      return true;
+    }
+
     default: return false;
     }
   }

runtime/util/util.cpp

@@ -35,7 +35,7 @@ block *construct_raw_term(void *subject, char const *sort, bool raw_value) {
 }
 
 void print_proof_hint_header(FILE *file) {
-  uint32_t version = 8;
+  uint32_t version = 9;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }

test/defn/k-files/imp.md

@@ -33,7 +33,7 @@ argument, because we want to give it a short-circuit semantics.
                  | "(" AExp ")"               [bracket]
                  > AExp "+" AExp              [left, strict, color(pink)]
   syntax BExp  ::= Bool
-                 | AExp "<=" AExp             [seqstrict, latex({#1}\leq{#2}), color(pink)]
+                 | AExp "<=" AExp             [seqstrict, color(pink)]
                  | "!" BExp                   [strict, color(pink)]
                  | "(" BExp ")"               [bracket]
                  > BExp "&&" BExp             [left, strict(1), color(pink)]
@@ -160,8 +160,8 @@ systems.  You can make these rules computational (dropping the attribute
 `structural`) if you do want these to count as computational steps.
 
 ```k
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .K
+  rule {S} => S
 ```
 
 ### Assignment
@@ -170,7 +170,7 @@ to be declared, otherwise the semantics will get stuck.  At the same time,
 the assignment is dissolved.
 
 ```k
-  rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
+  rule <k> X = I:Int; => .K ...</k> <state>... X |-> (_ => I) ...</state>
 ```
 
 ### Sequential composition
@@ -185,7 +185,7 @@ transitions (i.e., hiding the structural rules as unobservable, or
 internal steps).
 
 ```k
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 ```
 
 ### Conditional
@@ -205,7 +205,7 @@ We give the semantics of the `while` loop by unrolling.
 Note that we preferred to make the rule below structural.
 
 ```k
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 ```
 
 ### Programs
@@ -224,6 +224,6 @@ a computational step.
 ```k
   rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 endmodule
 ```