Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/llvm-backend

.github/workflows/develop.yml

@@ -37,3 +37,56 @@ jobs:
           if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
             git push origin master
           fi
+
+  post-performance-tests:
+    name: 'Performace Tests'
+    runs-on: [self-hosted, linux, normal]
+    continue-on-error: true
+    steps:
+      - uses: actions/checkout@v3
+      - name: 'Set up Docker Test Image'
+        env:
+          BASE_OS: ubuntu
+          BASE_DISTRO: jammy
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          BENCHER_API_TOKEN: ${{ secrets.BENCHER_API_TOKEN }}
+          BENCHER_PROJECT: k-framework
+          BENCHER_ADAPTER: json
+        run: |
+          set -euxo pipefail
+          workspace=$(pwd)
+          docker run --name k-posting-profiling-tests-${GITHUB_SHA}                                   \
+            --rm -it --detach                                                  \
+            -e BENCHER_API_TOKEN=$BENCHER_API_TOKEN                            \
+            -e BENCHER_PROJECT=$BENCHER_PROJECT                                \
+            -e BENCHER_ADAPTER=$BENCHER_ADAPTER                                \
+            -e GITHUB_HEAD_REF=$GITHUB_HEAD_REF                                \
+            -e GITHUB_BASE_REF=$GITHUB_BASE_REF                                \
+            -e GITHUB_TOKEN=$GITHUB_TOKEN                                      \
+            -e GITHUB_ACTIONS=true                                             \
+            -e GITHUB_EVENT_NAME=$GITHUB_EVENT_NAME                            \
+            -e GITHUB_REPOSITORY=$GITHUB_REPOSITORY                            \
+            -e GITHUB_REF=$GITHUB_REF                                          \
+            --workdir /opt/workspace                                           \
+            -v "${workspace}:/opt/workspace"                                   \
+            ${BASE_OS}:${BASE_DISTRO}
+      - name: 'Setting up dependencies'
+        run: |
+          set -euxo pipefail
+          docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c './k-distribution/tests/profiling/setup_profiling.sh SKIP_K_BUILD'
+      - name: 'Getting Performance Tests Results'
+        run: |
+          set -euxo pipefail
+          docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c './k-distribution/tests/profiling/post_results_to_develop.py'
+      - name: 'Posting Performance Tests Results'
+        run: |
+          set -euxo pipefail
+          docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c 'bencher run            \
+            --if-branch "develop" --else-if-branch "master"                    \
+            --file .profiling-results.json --err --ci-only-on-alert            \
+            --github-actions "${GITHUB_TOKEN}" 'echo "Exporting report"'
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 k-posting-profiling-tests-${GITHUB_SHA}
+          docker container rm --force k-posting-profiling-tests-${GITHUB_SHA} || true

flake.nix

@@ -8,7 +8,6 @@
       # NB booster-backend will bring in another dependency on haskell-backend,
       # but the two are not necessarily the same (different more often than not).
       # We get two transitive dependencies on haskell-nix.
-      inputs.k-framework.follows = "";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
     };
     llvm-backend.url = "github:runtimeverification/llvm-backend";

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java

@@ -9,13 +9,16 @@
 @RequestScoped
 public class HaskellKRunOptions {
 
-    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", hidden = true)
+    @Parameter(names="--haskell-backend-command", descriptionKey = "command",
+            description="Command to run the Haskell backend execution engine.", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 
-    @Parameter(names="--haskell-backend-home", description="Directory where the Haskell backend source installation resides.", hidden = true)
+    @Parameter(names="--haskell-backend-home", descriptionKey = "directory",
+            description="Directory where the Haskell backend source installation resides.", hidden = true)
     public String haskellBackendHome = System.getenv("KORE_HOME");
 
-    @Parameter(names="--default-claim-type", converter = SentenceTypeConverter.class, description="Default type for claims. Values: [all-path|one-path].")
+    @Parameter(names="--default-claim-type", descriptionKey = "type", converter = SentenceTypeConverter.class,
+            description="Default type for claims. Values: [all-path|one-path].")
     public ModuleToKORE.SentenceType defaultClaimType = ModuleToKORE.SentenceType.ALL_PATH;
 
     public static class SentenceTypeConverter extends BaseEnumConverter<ModuleToKORE.SentenceType> {

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java

@@ -7,7 +7,7 @@
 @RequestScoped
 public class HaskellKompileOptions {
 
-    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", hidden = true)
+    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 
     @Parameter(names="--no-haskell-binary", description="Use the textual KORE format in the haskell backend instead of the binary KORE format. This is a development option, but may be necessary on MacOS due to known issues with the binary format.")

k-distribution/src/main/scripts/lib/k

@@ -5,6 +5,7 @@ ulimit -s "$(ulimit -H -s)"
 K_BASE="$(cd "$(dirname "${BASH_SOURCE[0]}")/../" && pwd)"
 GIT_DESCRIBE="${K_BASE}/kframework/git-describe.out"
 TIMESTAMP="${K_BASE}/kframework/timestamp.out"
+version=
 
 for flag in "$@"; do
     if [[ "$flag" == "--version" ]]; then

k-distribution/src/main/scripts/lib/k-util.sh

@@ -33,7 +33,7 @@ k_util_usage() {
   --no-exc-wrap     Do not wrap messages to 80 chars (keep long lines).
   --profile         Print coarse process timing information. Format printed:
                     exit-code wall-time user-time system-time command args*
-  --temp-dir        Put temp files in this location. Default: /tmp/.<tool>-xxx
+  --temp-dir PATH   Put temp files in this location. Default: /tmp/.<tool>-xxx
   -v, --verbose     Print significant sub-commands executed.
 HERE
 }

k-distribution/tests/profiling/Makefile

@@ -1,4 +1,4 @@
-EXCLUDE=Makefile kprofiling.mak setup_profiling.sh
+EXCLUDE=Makefile kprofiling.mak setup_profiling.sh post_results_to_develop.py
 SUBDIRS=$(filter-out $(EXCLUDE), $(wildcard *))
 
 SUBCLEAN=$(addsuffix .clean,$(SUBDIRS))

k-distribution/tests/profiling/post_results_to_develop.py

@@ -0,0 +1,73 @@
+#!/usr/bin/env python3
+import json
+import subprocess
+
+COMMIT_SHA=''
+FROM_BRANCH=''
+TO_BRANCH='develop'
+
+def execute_command(command):
+    # Try to run the command
+    try:
+        result = subprocess.run(command,stdout=subprocess.PIPE,
+                                stderr=subprocess.PIPE, text=True)
+
+        # Check for errors
+        if result.returncode != 0:
+            print("Error:", result.stderr)
+            exit(1)
+
+    except subprocess.CalledProcessError as e:
+        # Handle any errors or exceptions here
+        print("Error:", e)
+        exit(1)
+
+    return result.stdout
+
+# git command to get the last commit in develop
+commit_command = [ 'git', 'log', '--format=\"%H\"', '-n', '1' ]
+COMMIT_SHA = execute_command(commit_command).strip('\"').strip('\"\n')
+
+# curl command to get the branch name of last commit in develop
+API_URL = 'https://api.github.com/repos/runtimeverification/k/commits/' \
+        + COMMIT_SHA + '/pulls'
+branch_command = ['curl', '-L', '-H', 'Accept:', 'application/vnd.github+json',
+                  '-H', '\"Authorization', 'Bearer', '${GITHUB_TOKEN}\"', '-H',
+                  '\"X-GitHub-Api-Version:', '2022-11-28\"', API_URL]
+FROM_BRANCH = json.loads(execute_command(branch_command))[0]['head']['label']
+
+print("Exporting last bencher report from", FROM_BRANCH, "to", TO_BRANCH)
+
+# This command will generate a JSON file with a list containing the last reports
+# sorted in descendenting order for the project.
+bencher_command = ["bencher", "report", "list", "--project", "k-framework",
+                   "--sort", "date_time", "--direction", "desc", "--per-page",
+                   "255"]
+data = json.loads(execute_command(bencher_command))
+
+# Collect all elemnts where the key 'project' is 'k_framework'
+k_framework = [item for item in data if item['project']['slug'] == 'k-framework'
+               and item['branch']['slug'] == FROM_BRANCH]
+
+# Append the last 6 reports to the list, they correspond to the last performance
+# execution on the last commit in FROM_BRANCH
+def get_name_and_value(item):
+    return item['metric_kind']['slug'], item['benchmarks'][0]['metric']['value']
+
+data = {}
+for i in range(0,6):
+    item = k_framework[i]
+    results = item['results']
+    benchmark_name = results[0][0]['benchmarks'][0]['name']
+    metric_name_memory, value_memory = get_name_and_value(results[0][0])
+    metric_name_size, value_size = get_name_and_value(results[0][1])
+
+    branch = item['branch']
+    print("Appended:", benchmark_name, "created in", item['created'],
+          "on branch", branch['name'], "with version", branch['version']['number'])
+
+    data.update({benchmark_name: {metric_name_size: {"value": value_size},
+                                  metric_name_memory: {"value": value_memory}}
+                 })
+
+json.dump(data, open('.profiling-results.json', 'w'), indent=4)

k-distribution/tests/profiling/setup_profiling.sh

@@ -6,8 +6,11 @@ export DEBIAN_FRONTEND=noninteractive
 export BENCHER_VERSION="0.3.10"
 apt-get update
 apt-get upgrade --yes
-apt-get install --yes make time sudo wget
-apt-get install --yes ./kframework.deb
+apt-get install --yes python3 git curl make time sudo wget
+# Build K if no flag was given and don't execute if flag was given
+if [ $# -eq 0 ]; then
+    apt-get install --yes ./kframework.deb
+fi
 
 wget https://github.com/bencherdev/bencher/releases/download/v"${BENCHER_VERSION}"/bencher_"${BENCHER_VERSION}"_amd64.deb
 sudo dpkg -i bencher_"${BENCHER_VERSION}"_amd64.deb

kernel/src/main/java/org/kframework/kast/KastOptions.java

@@ -101,20 +101,23 @@ public File bisonOutputFile() {
         return files.get().resolveWorkingDirectory(parameters.get(0));
     }
 
-    @Parameter(names="--bison-file", description="C file containing functions to link into bison parser.", hidden = true)
+    @Parameter(names="--bison-file", descriptionKey = "file", hidden = true,
+            description="C file containing functions to link into bison parser.")
     public String bisonFile;
 
-    @Parameter(names="--bison-stack-max-depth", description="Maximum size of bison parsing stack (default: 10000).", hidden = true)
+    @Parameter(names="--bison-stack-max-depth", descriptionKey = "size", hidden = true,
+            description="Maximum size of bison parsing stack.")
     public long bisonStackMaxDepth = 10000;
 
-    @Parameter(names={"--expression", "-e"}, description="An expression to parse passed on the command " +
-    "line. It is an error to provide both this option and a file to parse.")
+    @Parameter(names={"--expression", "-e"}, descriptionKey = "expression",
+            description="An expression to parse passed on the command line. It is an error to provide both this " +
+                    "option and a file to parse.")
     private String expression;
 
-    @Parameter(names={"--sort", "-s"}, converter=SortTypeConverter.class, description="The start sort for the default parser. " +
-            "The default is the sort of $PGM from the configuration. A sort may also be specified " +
-            "with the 'KRUN_SORT' environment variable, in which case it is used if the option is " +
-            "not specified on the command line.")
+    @Parameter(names={"--sort", "-s"}, descriptionKey = "sort", converter=SortTypeConverter.class,
+            description="The start sort for the default parser. The default is the sort of $PGM from the configuration. " +
+                    "A sort may also be specified with the 'KRUN_SORT' environment variable, in which case it is used " +
+                    "if the option is not specified on the command line.")
     public Sort sort;
 
     public static class SortTypeConverter implements IStringConverter<Sort> {
@@ -125,17 +128,20 @@ public Sort convert(String arg) {
         }
     }
 
-    @Parameter(names={"--module", "-m"}, description="Parse text in the specified module. Defaults to the syntax module of the definition.")
+    @Parameter(names={"--module", "-m"}, descriptionKey = "name",
+            description="Parse text in the specified module. Defaults to the syntax module of the definition.")
     public String module;
 
     @Parameter(names="--expand-macros", description="Also expand macros in the parsed string.")
     public boolean expandMacros = false;
 
-    @Parameter(names={"--input", "-i"}, converter=InputModeConverter.class,
+    @Parameter(names={"--input", "-i"}, descriptionKey = "mode", converter=InputModeConverter.class,
             description="How to read kast input in. <mode> is either [program|binary|kast|json|kore|rule].")
     public InputModes input = InputModes.PROGRAM;
 
-    @Parameter(names={"--steps"}, description="Apply specified kompilation steps to the parsed term. Only for --input rule. Use --steps help for a detailed description of available steps.")
+    @Parameter(names={"--steps"}, descriptionKey = "steps",
+            description="Apply specified kompilation steps to the parsed term. Only for --input rule. " +
+                    "Use --steps help for a detailed description of available steps.")
     public List<KastFrontEnd.KompileSteps> steps = Lists.newArrayList(KastFrontEnd.KompileSteps.anonVars);
 
     public static class InputModeConverter extends BaseEnumConverter<InputModes> {

kernel/src/main/java/org/kframework/kompile/KompileOptions.java

@@ -49,10 +49,12 @@ GlobalOptions getGlobalOptions_UseOnlyInGuiceProvider() {
     public OutputDirectoryOptions outputDirectory = new OutputDirectoryOptions();
 
     // Common options
-    @Parameter(names="--backend", description="Choose a backend. <backend> is one of [llvm|haskell|kore]. Each creates the kompiled K definition.")
+    @Parameter(names="--backend", description="Choose a backend. <backend> is one of [llvm|haskell|kore]. Each creates the kompiled K definition.", descriptionKey = "backend")
     public String backend = Backends.LLVM;
 
-    @Parameter(names="--main-module", description="Specify main module in which a program starts to execute. This information is used by 'krun'. The default is the name of the given K definition file without the extension (.k).")
+    @Parameter(names="--main-module", descriptionKey = "name",
+            description="Specify main module in which a program starts to execute. This information is used by 'krun'. " +
+            "The default is the name of the given K definition file without the extension (.k).")
     private String mainModule;
 
     public String mainModule(FileUtil files) {
@@ -62,7 +64,8 @@ public String mainModule(FileUtil files) {
         return mainModule;
     }
 
-    @Parameter(names="--syntax-module", description="Specify main module for syntax. This information is used by 'krun'. (Default: <main-module>-SYNTAX).")
+    @Parameter(names="--syntax-module", descriptionKey = "name",
+            description="Specify main module for syntax. This information is used by 'krun'. (Default: <main-module>-SYNTAX).")
     private String syntaxModule;
 
     public String syntaxModule(FileUtil files) {
@@ -75,7 +78,7 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--coverage", description="Generate coverage data when executing semantics.")
     public boolean coverage;
 
-    @Parameter(names="--hook-namespaces", listConverter=StringListConverter.class, description="<string> is a whitespace-separated list of namespaces to include in the hooks defined in the definition", hidden = true)
+    @Parameter(names="--hook-namespaces", listConverter=StringListConverter.class, description="<string> is a whitespace-separated list of namespaces to include in the hooks defined in the definition", descriptionKey = "string", hidden = true)
     public List<String> hookNamespaces = Collections.emptyList();
 
     @Parameter(names="-O1", description="Optimize in ways that improve performance and code size, but interfere with debugging and increase compilation time slightly.")
@@ -96,8 +99,7 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--read-only-kompiled-directory", description="Files in the generated kompiled directory should be read-only to other frontend tools.", hidden = true)
     public boolean readOnlyKompiledDirectory = false;
 
-    @Parameter(names="--concrete-rules", description="List of rule labels to be considered concrete, in addition to " +
-            "rules marked with `[concrete]` attribute")
+    @Parameter(names="--concrete-rules", description="List of rule labels to be considered concrete, in addition to rules marked with `[concrete]` attribute", descriptionKey = "labels")
     public List<String> extraConcreteRuleLabels = Collections.emptyList();
 
     @ParametersDelegate
@@ -115,10 +117,10 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--gen-glr-bison-parser", description="Emit GLR bison parser for the PGM configuration variable within the syntax module of your definition into the kompiled definition.")
     public boolean genGlrBisonParser;
 
-    @Parameter(names="--bison-file", description="C file containing functions to link into bison parser.", hidden = true)
+    @Parameter(names="--bison-file", description="C file containing functions to link into bison parser.", descriptionKey = "file", hidden = true)
     public String bisonFile;
 
-    @Parameter(names="--bison-stack-max-depth", description="Maximum size of bison parsing stack (default: 10000).", hidden = true)
+    @Parameter(names="--bison-stack-max-depth", description="Maximum size of bison parsing stack.", descriptionKey = "size", hidden = true)
     public long bisonStackMaxDepth = 10000;
 
     @Parameter(names="--bison-parser-library", description="Generate a shared library rather than an executable for Bison parsers", hidden = true)
@@ -129,10 +131,10 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--top-cell", description="Choose the top configuration cell when more than one is provided. Does nothing if only one top cell exists.")
     public String topCell;
 
-    @Parameter(names="--debug-type-inference", description="Filename and source line of rule to debug type inference for. This is generally an option used only by maintainers.", hidden = true)
+    @Parameter(names="--debug-type-inference", description="Filename and source line of rule to debug type inference for. This is generally an option used only by maintainers.", descriptionKey = "file", hidden = true)
     public String debugTypeInference;
 
-    @Parameter(names={"--post-process"}, description="JSON KAST => JSON KAST converter to run on definition after kompile pipeline.", hidden = true)
+    @Parameter(names={"--post-process"}, description="JSON KAST => JSON KAST converter to run on definition after kompile pipeline.", descriptionKey = "command", hidden = true)
     public String postProcess;
 
     // TODO(dwightguth): remove this when it is no longer needed

kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java

@@ -195,12 +195,16 @@ public void appendAllParametersDetails(StringBuilder out, int indentCount, Strin
             WrappedParameter parameter = pd.getParameter();
             String description = pd.getDescription();
             boolean hasDescription = !description.isEmpty();
+            String descriptionKey = pd.getParameter().getParameter().descriptionKey();
+            descriptionKey = descriptionKey.isEmpty() ? "" : " <" + descriptionKey + ">";
 
             // First line, command name
             out.append(indent)
                     .append("  ")
                     .append(parameter.required() ? "* " : "  ")
-                    .append(pd.getNames())
+                    .append(pd.getLongestName())
+                    .append(descriptionKey)
+                    .append(Arrays.stream(pd.getParameter().names()).count() > 1 ? ", " + pd.getParameter().names()[1] + descriptionKey : "")
                     .append("\n");
 
             if (hasDescription) {