ExCuter

Pure Elixir concolic testing tool for finding bugs in your code.

ExCuter uses concolic (concrete + symbolic) execution to systematically explore paths through your code and find inputs that trigger errors.

Requirements

• Elixir 1.14+
• Z3 SMT solver

Installing Z3

macOS:

brew install z3

Linux (Debian/Ubuntu):

apt install z3

Verify installation:

z3 --version

Nix Include the z3 package in your mkShell's nativeBuildInputs, add to home manager, or nix-env -i z3.

Installation

Add to your mix.exs:

def deps do
  [
    {:ex_cuter, git: "https://github.com/cuter-testing/ex_cuter.git", only: [:dev, :test]}
  ]
end

CRITICAL: ExCuter needs debug_info to analyze your modules. Ensure your project has:

def project do
  [
    # ... other options
    elixirc_options: [debug_info: true]
  ]
end

Then run:

mix deps.get

Usage

Command Line (Mix Task)

# Basic usage
mix ex_cuter MyModule my_function '[initial_args]'

# With options
mix ex_cuter MyModule my_function '[0]' --depth 15 --timeout 30000

The idea is to run the task with the module name, the function name, the list of args in a single expression, and any options.

Programmatic API

# Run concolic testing on a function
case ExCuter.run(MyModule, :my_function, [0], depth: 10) do
  {:errors, error_inputs} ->
    IO.puts("Found bugs with inputs: #{inspect(error_inputs)}")

  {:ok, _} ->
    IO.puts("No bugs found!")

  {:error, reason} ->
    IO.puts("Testing failed: #{inspect(reason)}")
end

In ExUnit Tests

ExCuter provides a test DSL for clean integration with ExUnit:

defmodule MyModuleTest do
  use ExCuter.Test

  # Test that a specific input triggers an error
  cuter_test "finds bug at 42", MyModule, :buggy_func, [0] do
    assert_error_found [42]
  end

  # Test that multiple specific inputs trigger errors
  cuter_test "finds multiple bugs", MyModule, :buggy_func, [0] do
    assert_errors_found [[42], [-42]]
  end

  # Test that a function has no bugs
  cuter_test "safe function has no bugs", MyModule, :safe_func, [0], depth: 10 do
    assert_no_errors()
  end

  # Test that at least one error exists
  cuter_test "has bugs", MyModule, :buggy_func, [0] do
    assert_any_error()
  end

  # Test with a predicate on error inputs
  cuter_test "finds value > 100", MyModule, :buggy_func, [0] do
    assert_error_satisfies fn [x] -> x > 100 end
  end

  # Custom assertions using get_errors()
  cuter_test "custom check", MyModule, :buggy_func, [0] do
    errors = get_errors()
    assert length(errors) >= 2
  end
end

Test Options

When using use ExCuter.Test, you can set defaults:

use ExCuter.Test, default_depth: 15, default_timeout: 120_000, async: false

Individual tests can override with the opts argument:

cuter_test "deep search", MyModule, :func, [0], depth: 50, timeout: 180_000 do
  assert_any_error()
end

Filtering Tests

All cuter tests are tagged with :cuter:

# Run only cuter tests
mix test --only cuter

# Run everything except cuter tests
mix test --exclude cuter

How It Works

1. Concrete Execution: Run the function with actual input values
2. Symbolic Tracking: Track symbolic constraints along the execution path
3. Constraint Solving: Use Z3 to solve for inputs that take different paths
4. Path Exploration: Systematically explore new paths by negating constraints
5. Error Detection: Report inputs that cause the function to raise errors

Supported Features

• Integer arithmetic and comparisons
• Guards and pattern matching
• Lists, tuples, and binaries
• Recursive functions
• Higher-order functions (map, filter, fold, etc.)
• Multi-process execution (spawn, send, receive)
• Exception handling (try/catch/rescue)
• Binary pattern matching with various types/endianness

Example

Given a buggy function:

defmodule Example do
  def divide(x, y) do
    if y == 0 do
      raise "division by zero"
    else
      x / y
    end
  end
end

ExCuter will find that y = 0 triggers the error:

{:errors, [[_, 0]]} = ExCuter.run(Example, :divide, [10, 5], depth: 10)

License

GPL-3.0 - See LICENSE file for details.