Adding Timer Hook Implementation for K (#4673)

Follow up of
runtimeverification/llvm-backend#1131

This Hook is commonly used to measure VM time in Semantics executions.

The execution of a semantics with `timerStart` and `timerStop` produces
a `hook_time.txt` file with the difference of two timestamps in
nanoseconds.

---------

Co-authored-by: Theodoros Kasampalis <[email protected]>

k-distribution/include/kframework/builtin/timer.md

@@ -0,0 +1,11 @@
+---
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+---
+
+```k
+module TIMER
+    syntax K ::= "timerStart" "(" ")" [function, hook(TIMER.timerStart)]
+
+    syntax K ::= "timerStop" "(" ")" [function, hook(TIMER.timerStop)]
+endmodule
+```

k-frontend/src/main/java/org/kframework/builtin/Hooks.java

@@ -26,6 +26,7 @@ public class Hooks {
   public static final String SUBSTITUTION = "SUBSTITUTION";
   public static final String UNIFICATION = "UNIFICATION";
   public static final String JSON = "JSON";
+  public static final String TIMER = "TIMER";
 
   public static final Set<String> namespaces =
       Collections.unmodifiableSet(
@@ -48,5 +49,6 @@ public class Hooks {
                   STRING,
                   SUBSTITUTION,
                   UNIFICATION,
-                  JSON)));
+                  JSON,
+                  TIMER)));
 }

pyk/regression-new/imp-timer/Makefile

@@ -0,0 +1,6 @@
+DEF=imp
+EXT=imp
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+
+include ../include/ktest.mak

pyk/regression-new/imp-timer/collatz.imp

@@ -0,0 +1,19 @@
+// This program tests the Collatz conjecture for all numbers up to m
+// and accumulates the total number of steps in s.
+
+int m, n, q, r, s;
+m = 10;
+while (!(m<=2)) {
+  n = m;
+  m = m + -1;
+  while (!(n<=1)) {
+    s = s + 1;
+    q = n/2;
+    r = q+q + 1;
+    if (r<=n) {
+      n = n+n+n + 1;         // n becomes 3*n+1 if odd
+    } else {n=q;}          //        or   n/2 if even
+  }
+}
+
+// s should be 66 when m is 10

pyk/regression-new/imp-timer/collatz.imp.out

@@ -0,0 +1,13 @@
+<generatedTop>
+  <T>
+    <k>
+      .K
+    </k>
+    <state>
+      q |-> 1 s |-> 66 n |-> 1 r |-> 3 m |-> 2
+    </state>
+  </T>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>

pyk/regression-new/imp-timer/imp.k

@@ -0,0 +1,80 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+
+requires "timer.md"
+
+module IMP-SYNTAX
+  imports BOOL-SYNTAX
+  imports INT-SYNTAX
+  imports ID
+
+  syntax AExp  ::= Int | Id
+                 | "-" Int                    [format(%1%2)]
+                 | AExp "/" AExp              [left, strict, color(pink)]
+                 | "(" AExp ")"               [bracket]
+                 > AExp "+" AExp              [left, strict, color(pink)]
+  syntax BExp  ::= Bool
+                 | AExp "<=" AExp             [seqstrict, color(pink)]
+                 | "!" BExp                   [strict, color(pink)]
+                 | "(" BExp ")"               [bracket]
+                 > BExp "&&" BExp             [left, strict(1), color(pink)]
+  syntax Block ::= "{" "}"
+                 | "{" Stmt "}"               [format(%1%i%n%2%d%n%3)]
+  syntax Stmt  ::= Block
+                 | Id "=" AExp ";"            [strict(2), color(pink), format(%1 %2 %3%4)]
+                 | "if" "(" BExp ")"
+                   Block "else" Block         [strict(1), colors(yellow, white, white, yellow), format(%1 %2%3%4 %5 %6 %7)]
+                 | "while" "(" BExp ")" Block [colors(yellow,white,white), format(%1 %2%3%4 %5)]
+                 > Stmt Stmt                  [left, format(%1%n%2)]
+
+  syntax Pgm ::= "int" Ids ";" Stmt           [format(%1 %2%3%n%4), colors(yellow,pink)]
+  syntax Ids ::= List{Id,","} [format(%1%2 %3)]
+endmodule
+
+module IMP
+  imports IMP-SYNTAX
+  imports BOOL
+  imports INT
+  imports MAP
+  imports SET
+  imports TIMER
+
+  syntax KResult ::= Int | Bool
+
+  syntax KItem ::= "timerstart"
+  syntax KItem ::= "timerstop"
+
+  configuration <T color="yellow">
+                  <k color="green"> timerstart ~> $PGM:Pgm ~> timerstop </k>
+                  <state color="red"> .Map </state>
+                </T>
+
+  rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
+
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
+  rule I1 + I2 => I1 +Int I2
+  rule - I1 => 0 -Int I1
+
+  rule I1 <= I2 => I1 <=Int I2
+  rule ! T => notBool T
+  rule true && B => B
+  rule false && _ => false
+
+  rule {} => .K
+  rule {S} => S
+
+  rule <k> X = I:Int; => .K ...</k> <state>... X |-> (_ => I) ...</state>
+
+  rule S1:Stmt S2:Stmt => S1 ~> S2
+
+  rule if (true)  S else _ => S
+  rule if (false) _ else S => S
+
+  rule while (B) S => if (B) {S while (B) S} else {}
+
+  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
+
+  rule timerstart => timerStart()
+  rule timerstop => timerStop()
+endmodule

pyk/regression-new/imp-timer/primes.imp

@@ -0,0 +1,26 @@
+// This program counts in s all the prime numbers up to m.
+
+int i, m, n, q, r, s, t, x, y, z;
+m = 10;  n = 2;
+while (n <= m) {
+  // checking primality of n and writing t to 1 or 0
+  i = 2;  q = n/i;  t = 1;
+  while (i<=q && 1<=t) {
+    x = i;
+    y = q;
+    // fast multiplication (base 2) algorithm
+    z = 0;
+    while (!(x <= 0)) {
+      q = x/2;
+      r = q+q + 1;
+      if (r <= x) { z = z+y; } else {}
+      x = q;
+      y = y+y;
+    } // end fast multiplication
+    if (n <= z) { t = 0; } else { i = i + 1;  q = n/i; }
+  } // end checking primality
+  if (1 <= t) { s = s + 1; } else {}
+  n = n + 1;
+}
+
+// s should be 4 when m = 10.

pyk/regression-new/imp-timer/primes.imp.out

@@ -0,0 +1,13 @@
+<generatedTop>
+  <T>
+    <k>
+      .K
+    </k>
+    <state>
+      q |-> 0 x |-> 0 s |-> 4 n |-> 11 i |-> 2 z |-> 10 r |-> 1 m |-> 10 y |-> 20 t |-> 0
+    </state>
+  </T>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>

pyk/regression-new/imp-timer/sum.imp

@@ -0,0 +1,12 @@
+// This program calculates in sum
+// the sum of numbers from 1 to n.
+
+int n, sum;
+n = 100;
+sum = 0;
+while (!(n <= 0)) {
+  sum = sum + n;
+  n = n + -1;
+}
+
+// sum should be 5050 when n is 100

pyk/regression-new/imp-timer/sum.imp.out

@@ -0,0 +1,13 @@
+<generatedTop>
+  <T>
+    <k>
+      .K
+    </k>
+    <state>
+      n |-> 0 sum |-> 5050
+    </state>
+  </T>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>