FFI for KLLVM

.github/actions/with-docker/Dockerfile.fuzz

@@ -0,0 +1,23 @@
+ARG K_VERSION=7.1.241
+ARG RUST_TOOLCHAIN=1.82.0
+
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION} AS semantics
+
+WORKDIR /opt/imp-semantics
+COPY examples/fuzzer/k-semantics .
+RUN kompile --llvm-kompile-type c fuzz.k
+
+FROM rust:${RUST_TOOLCHAIN}
+
+COPY --from=semantics /opt/imp-semantics/fuzz-kompiled/interpreter.so /usr/lib
+RUN apt-get update && apt-get install --yes build-essential binutils-dev libunwind-dev libblocksruntime-dev liblzma-dev
+RUN cargo install honggfuzz
+
+ARG USER=user
+ARG GROUP=$USER
+ARG USER_ID=1000
+ARG GROUP_ID=$USER_ID
+
+RUN groupadd -g $GROUP_ID $GROUP && useradd -m -u $USER_ID -s /bin/sh -g $GROUP $USER
+
+USER $USER:$GROUP

.github/actions/with-docker/action.yml

@@ -5,6 +5,10 @@ inputs:
     description: 'Docker container name to use'
     required: true
     type: string
+  dockerfile:
+    description: 'Dockerfile to use'
+    required: true
+    type: string
 runs:
   using: 'composite'
   steps:
@@ -15,7 +19,7 @@ runs:
 
       CONTAINER_NAME=${{ inputs.container-name }}
       TAG=runtimeverificationinc/${CONTAINER_NAME}
-      DOCKERFILE=${{ github.action_path }}/Dockerfile
+      DOCKERFILE=${{ github.action_path }}/${{ inputs.dockerfile }}
 
       docker build .         \
         --file ${DOCKERFILE} \

.github/workflows/test-pr.yml

@@ -16,9 +16,40 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kframework-rs-${{ github.sha }}
+          dockerfile: Dockerfile
       - name: 'Build and test'
         run: docker exec -u user kframework-rs-${GITHUB_SHA} make
       - name: 'Tear down Docker'
         if: always()
         run: |
           docker stop --time=0 kframework-rs-${GITHUB_SHA}
+
+  build-ffi-and-fuzz:
+    name: 'Build with the FFI and run the fuzzing example'
+    runs-on: [self-hosted, linux, normal]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          container-name: kframework-rs-fuzz-${{ github.sha }}
+          dockerfile: Dockerfile.fuzz
+      - name: 'Build and test'
+        run: |
+          export HFUZZ_RUN_ARGS="--verbose --logfile log.txt --run_time 60"
+          docker exec                                \
+            --env HFUZZ_RUN_ARGS="${HFUZZ_RUN_ARGS}" \
+            --workdir /home/user/examples/fuzzer     \
+            kframework-rs-fuzz-${GITHUB_SHA}         \
+            cargo hfuzz run fuzzer
+          echo "Final lines of hfuzz output:"
+          docker exec                                \
+            --env HFUZZ_RUN_ARGS="${HFUZZ_RUN_ARGS}" \
+            --workdir /home/user/examples/fuzzer     \
+            kframework-rs-fuzz-${GITHUB_SHA}         \
+            tail log.txt
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 kframework-rs-fuzz-${GITHUB_SHA}

examples/fuzzer/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "fuzzer"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+arbitrary = "1.4.1"
+honggfuzz = "0.5.57"
+kframework = { path = "../.." }
+kframework_ffi = { path = "../../kframework_ffi" }

examples/fuzzer/README.md

@@ -0,0 +1,29 @@
+# Imp fuzzing with kframework_ffi
+
+This is an example of a fuzzing target for a hashing function that uses the kllvm execution engine for the Imp semantics.
+
+## Requirements
+
+- An installation of the [kframework](https://github.com/runtimeverification/k)
+- An installation of [rustup](https://rustup.rs/)
+- Cargo installed [honggfuzz](https://github.com/rust-fuzz/honggfuzz-rs)
+
+NOTE: If you are using a `kup` installed version of K, then you are very likely to run into linking errors between the nix libraries and your installation of `rustup`. This should be able to get resolved by a proper derivation, but no such thing exists at the time of writing.
+
+## Setup
+
+```
+$ cd k-semantics
+$ kompile --llvm-kompile-type c fuzz.k
+$ export LD_LIBRARY_PATH=$(realpath fuzz-kompiled)
+$ cd ..
+$ cargo hfuzz run fuzzer
+```
+
+## Explanation
+
+The `FUZZ` semantics module extends Imp with an `Assert` statement which rewrites the entire configuration into a failing symbol when it doesn't pass. It also has a success symbol which it will rewrite the configuration to when execution is finished (ie. the <k> cell is empty).
+
+There is an `init_fuzz` utility symbol which takes two integer parameters and then rewrites to an Imp program that performs a hash over those integers. The failure case for this program is arbitrarily if the hash ends up being a very low number.
+
+On the rust side, the fuzzing target uses the random input to construct this `init_fuzz` symbol and the initial configuration in the form of a kore string. Then it uses the foreign functions to build that configuration in kllvm's interned representation, execute it, and retrieve the resulting configuration as another kore string. Then it parses the kore string and checks for the failure or success case.

examples/fuzzer/build.rs

@@ -0,0 +1,17 @@
+use std::env;
+
+fn main() {
+    // Link interpreter.so
+    println!("cargo:rustc-link-arg=-l:interpreter.so");
+
+    // Add the location of interpreter.so to your LD_LIBRARY_PATH variable
+    // You will also need this variable set when you run the program
+    match env::var_os("LD_LIBRARY_PATH") {
+        Some(paths) => {
+            for lib_path in env::split_paths(&paths) {
+                println!("cargo:rustc-link-search={}", lib_path.display());
+            }
+        }
+        None => (),
+    };
+}

examples/fuzzer/k-semantics/fuzz.k

@@ -0,0 +1,45 @@
+requires "imp.k"
+
+module FUZZ
+  imports IMP
+
+  configuration <T/>
+
+  syntax Stmt ::= "Assert" "(" BExp ")" ";" [strict]
+  rule Assert( true ); => .K
+
+  syntax Pgm   ::= "init_fuzz" "(" Int "," Int ")" [symbol(init_fuzz)]
+  syntax TCell ::= "FUZZ_SUCCESS" [symbol(fuzz_success)]
+                 | "FUZZ_FAILURE" [symbol(fuzz_failure)]
+
+  syntax Id ::= "x" [token]
+              | "y" [token]
+              | "combined" [token]
+              | "salted" [token]
+              | "z" [token]
+              | "hash_val" [token]
+
+  rule <k> init_fuzz(X, Y)
+        => int x, y, combined, salted, z, hash_val;
+
+           x = X;
+           y = Y;
+
+           combined = x * 1000000 + y;
+
+           salted = combined + 1;
+
+           z = salted + 11400714819323198485;
+           z = (z ^ (z >> 30)) * 13787848793156543929;
+           z = (z ^ (z >> 27)) * 10723151780598845931;
+           z = z ^ (z >> 31);
+
+           hash_val = z & 4294967295;
+
+           Assert( !( hash_val <= 15000 ) );
+           ...
+       </k>
+
+  rule <T> <k> .K </k> ... </T> => FUZZ_SUCCESS
+  rule <T> <k> Assert(false); ... </k> ... </T> => FUZZ_FAILURE
+endmodule

examples/fuzzer/k-semantics/imp.k

@@ -0,0 +1,68 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+
+module IMP-SYNTAX
+  imports DOMAINS-SYNTAX
+  syntax AExp  ::= Int | Id
+                 | "-" Int
+                 | AExp "*" AExp              [left, strict]
+                 | AExp "^" AExp              [left, strict]
+                 | AExp ">>" AExp             [left, strict]
+                 | AExp "&" AExp             [left, strict]
+                 | "(" AExp ")"               [bracket]
+                 > AExp "+" AExp              [left, strict]
+  syntax BExp  ::= Bool
+                 | AExp "<=" AExp             [seqstrict]
+                 | "!" BExp                   [strict]
+                 | "(" BExp ")"               [bracket]
+                 > BExp "&&" BExp             [left, strict(1)]
+  syntax Block ::= "{" "}"
+                 | "{" Stmt "}"
+  syntax Stmt  ::= Block
+                 | Id "=" AExp ";"            [strict(2)]
+                 | "if" "(" BExp ")"
+                   Block "else" Block         [strict(1)]
+                 | "while" "(" BExp ")" Block
+                 > Stmt Stmt                  [left]
+  syntax Pgm ::= "int" Ids ";" Stmt
+  syntax Ids ::= List{Id,","}
+endmodule
+
+
+module IMP
+  imports IMP-SYNTAX
+  imports DOMAINS
+  syntax KResult ::= Int | Bool
+
+  configuration <T color="yellow">
+                  <k color="green"> $PGM:Pgm </k>
+                  <state color="red"> .Map </state>
+                </T>
+
+// AExp
+  rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
+  rule I1 * I2 => I1 *Int I2
+  rule I1 ^ I2 => I1 xorInt I2
+  rule I1 >> I2 => I1 >>Int I2
+  rule I1 & I2 => I1 &Int I2
+  rule I1 + I2 => I1 +Int I2
+  rule - I1 => 0 -Int I1
+// BExp
+  rule I1 <= I2 => I1 <=Int I2
+  rule ! T => notBool T
+  rule true && B => B
+  rule false && _ => false
+// Block
+  rule {} => .K
+  rule {S} => S
+// Stmt
+  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 {}
+// Pgm
+  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
+
+endmodule

examples/fuzzer/src/main.rs

@@ -0,0 +1,103 @@
+use std::panic;
+
+use arbitrary::{Arbitrary, Unstructured};
+use honggfuzz::fuzz;
+use kframework::kore::{App, Parser, Pattern, SymbolId};
+use kframework_ffi::kllvm;
+
+#[derive(Clone, Copy)]
+struct FuzzInput {
+    field1: u32,
+    field2: u32,
+}
+
+impl Arbitrary<'_> for FuzzInput {
+    fn arbitrary(u: &mut Unstructured<'_>) -> arbitrary::Result<Self> {
+        let field1 = u.int_in_range(0..=1000000)?;
+        let field2 = u.int_in_range(0..=1000000)?;
+        Ok(FuzzInput { field1, field2 })
+    }
+}
+
+/// Hardcoded kore strings for assembling the initial configuration
+const PREFIX: &str = r#"
+Lbl'-LT-'generatedTop'-GT-'{}(
+  Lbl'-LT-'T'-GT-'{}(
+    Lbl'-LT-'k'-GT-'{}(
+      kseq{}(inj{SortPgm{}, SortKItem{}}(
+        Lblinit'Unds'fuzz{}(\dv{SortInt{}}(""#;
+const MIDFIX: &str = r#""),\dv{SortInt{}}(""#;
+const POSTFIX: &str = r#""))), dotk{}())), Lbl'-LT-'state'-GT-'{}(Lbl'Stop'Map{}())), Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))"#;
+
+impl From<FuzzInput> for String {
+    /// Build the kore string to send off to kllvm's parser
+    fn from(input: FuzzInput) -> String {
+        let field1_str = input.field1.to_string();
+        let field2_str = input.field2.to_string();
+
+        format!(
+            "{}{}{}{}{}",
+            PREFIX, field1_str, MIDFIX, field2_str, POSTFIX
+        )
+    }
+}
+
+fn main() {
+    kllvm::init();
+
+    // Free kllvm's memory when panicking.
+    panic::set_hook(Box::new(|_| {
+        kllvm::free_all_memory();
+    }));
+
+    loop {
+        fuzz!(|seed: &[u8]| {
+            let mut u = Unstructured::new(seed);
+            let Ok(input) = FuzzInput::arbitrary(&mut u) else {
+                panic!("Failed to generate input from seed");
+            };
+
+            // Build the initial config, execute it, retrieve the final config kore string
+            let pattern_string: String = input.clone().into();
+            let pattern: kllvm::Pattern =
+                pattern_string.parse().expect("Failed parsing kore string");
+            let mut block: kllvm::Block = pattern.into();
+
+            block.take_steps(-1);
+
+            let result: kllvm::Pattern = block.into();
+
+            // Parse the final kore string as [Pattern] for matching
+            let result_pattern: Pattern = Parser::new(&result.to_string())
+                .unwrap()
+                .pattern()
+                .expect("Failed to parse result pattern");
+
+            match result_pattern {
+                Pattern::App(App { symbol, args, .. }, ..) => {
+                    if symbol == SymbolId::new("Lbl'-LT-'generatedTop'-GT-'".to_string()).unwrap() {
+                        let expected = args
+                            .get(0)
+                            .expect("Expected first argument of generatedTop to be present");
+                        match expected {
+                            Pattern::App(App { symbol, .. }, ..) => {
+                                if *symbol
+                                    == SymbolId::new("Lblfuzz'Unds'failure".to_string()).unwrap()
+                                {
+                                    // <generatedTop> FUZZ_FAILURE </generatedTop>
+                                    panic!("Failure!");
+                                }
+                            }
+                            _ => panic!(
+                                "Expected first argument of generatedTop to be an App pattern"
+                            ),
+                        }
+                    } else {
+                        panic!("Expected symbol for <generatedTop> but found {:?}", symbol);
+                    }
+                }
+                _ => panic!("Expected App pattern but found: {:?}", result_pattern),
+            };
+        });
+    }
+}

kframework_ffi/Cargo.toml

@@ -0,0 +1,3 @@
+[package]
+name = "kframework_ffi"
+version = "0.1.0"