From 8a20bdb788f1e4d56a1d813dd109f4e210291cda Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 23 Oct 2024 17:28:29 -0300 Subject: [PATCH] Adding Timer Hook Implementation for K (#4673) Follow up of https://github.com/runtimeverification/llvm-backend/pull/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 --- .../include/kframework/builtin/timer.md | 11 +++ .../java/org/kframework/builtin/Hooks.java | 4 +- pyk/regression-new/imp-timer/Makefile | 6 ++ pyk/regression-new/imp-timer/collatz.imp | 19 +++++ pyk/regression-new/imp-timer/collatz.imp.out | 13 +++ pyk/regression-new/imp-timer/imp.k | 80 +++++++++++++++++++ pyk/regression-new/imp-timer/primes.imp | 26 ++++++ pyk/regression-new/imp-timer/primes.imp.out | 13 +++ pyk/regression-new/imp-timer/sum.imp | 12 +++ pyk/regression-new/imp-timer/sum.imp.out | 13 +++ 10 files changed, 196 insertions(+), 1 deletion(-) create mode 100644 k-distribution/include/kframework/builtin/timer.md create mode 100644 pyk/regression-new/imp-timer/Makefile create mode 100644 pyk/regression-new/imp-timer/collatz.imp create mode 100644 pyk/regression-new/imp-timer/collatz.imp.out create mode 100644 pyk/regression-new/imp-timer/imp.k create mode 100644 pyk/regression-new/imp-timer/primes.imp create mode 100644 pyk/regression-new/imp-timer/primes.imp.out create mode 100644 pyk/regression-new/imp-timer/sum.imp create mode 100644 pyk/regression-new/imp-timer/sum.imp.out diff --git a/k-distribution/include/kframework/builtin/timer.md b/k-distribution/include/kframework/builtin/timer.md new file mode 100644 index 00000000000..eb79d847144 --- /dev/null +++ b/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 +``` diff --git a/k-frontend/src/main/java/org/kframework/builtin/Hooks.java b/k-frontend/src/main/java/org/kframework/builtin/Hooks.java index 028047a474c..2a308914e46 100644 --- a/k-frontend/src/main/java/org/kframework/builtin/Hooks.java +++ b/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 namespaces = Collections.unmodifiableSet( @@ -48,5 +49,6 @@ public class Hooks { STRING, SUBSTITUTION, UNIFICATION, - JSON))); + JSON, + TIMER))); } diff --git a/pyk/regression-new/imp-timer/Makefile b/pyk/regression-new/imp-timer/Makefile new file mode 100644 index 00000000000..ad228b0db8d --- /dev/null +++ b/pyk/regression-new/imp-timer/Makefile @@ -0,0 +1,6 @@ +DEF=imp +EXT=imp +TESTDIR=. +KOMPILE_BACKEND=llvm + +include ../include/ktest.mak diff --git a/pyk/regression-new/imp-timer/collatz.imp b/pyk/regression-new/imp-timer/collatz.imp new file mode 100644 index 00000000000..d8e35fce848 --- /dev/null +++ b/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 diff --git a/pyk/regression-new/imp-timer/collatz.imp.out b/pyk/regression-new/imp-timer/collatz.imp.out new file mode 100644 index 00000000000..aa49c43958a --- /dev/null +++ b/pyk/regression-new/imp-timer/collatz.imp.out @@ -0,0 +1,13 @@ + + + + .K + + + q |-> 1 s |-> 66 n |-> 1 r |-> 3 m |-> 2 + + + + 0 + + diff --git a/pyk/regression-new/imp-timer/imp.k b/pyk/regression-new/imp-timer/imp.k new file mode 100644 index 00000000000..8dfe5bf3420 --- /dev/null +++ b/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 + timerstart ~> $PGM:Pgm ~> timerstop + .Map + + + rule X:Id => I ... ... X |-> I ... + + 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 X = I:Int; => .K ... ... X |-> (_ => I) ... + + 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 int (X,Xs => Xs);_ ... Rho:Map (.Map => X|->0) + requires notBool (X in keys(Rho)) + rule int .Ids; S => S + + rule timerstart => timerStart() + rule timerstop => timerStop() +endmodule diff --git a/pyk/regression-new/imp-timer/primes.imp b/pyk/regression-new/imp-timer/primes.imp new file mode 100644 index 00000000000..3edf1a58fc8 --- /dev/null +++ b/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. diff --git a/pyk/regression-new/imp-timer/primes.imp.out b/pyk/regression-new/imp-timer/primes.imp.out new file mode 100644 index 00000000000..7b09bfa09ac --- /dev/null +++ b/pyk/regression-new/imp-timer/primes.imp.out @@ -0,0 +1,13 @@ + + + + .K + + + q |-> 0 x |-> 0 s |-> 4 n |-> 11 i |-> 2 z |-> 10 r |-> 1 m |-> 10 y |-> 20 t |-> 0 + + + + 0 + + diff --git a/pyk/regression-new/imp-timer/sum.imp b/pyk/regression-new/imp-timer/sum.imp new file mode 100644 index 00000000000..23e8bb6df0d --- /dev/null +++ b/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 diff --git a/pyk/regression-new/imp-timer/sum.imp.out b/pyk/regression-new/imp-timer/sum.imp.out new file mode 100644 index 00000000000..00330b40f39 --- /dev/null +++ b/pyk/regression-new/imp-timer/sum.imp.out @@ -0,0 +1,13 @@ + + + + .K + + + n |-> 0 sum |-> 5050 + + + + 0 + +