Skip to content

Halmos new version#65

Merged
GalloDaSballo merged 7 commits intomainfrom
feat-halmos-2
Sep 23, 2025
Merged

Halmos new version#65
GalloDaSballo merged 7 commits intomainfrom
feat-halmos-2

Conversation

@0kn0t
Copy link
Copy Markdown
Contributor

@0kn0t 0kn0t commented Sep 22, 2025

No description provided.

Copilot AI review requested due to automatic review settings September 22, 2025 21:44
Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull Request Overview

This PR introduces a completely rewritten version of the Halmos parser for fuzzing logs. The update replaces the existing line-by-line parsing approach with a block-based parser that processes entire trace sections at once and includes enhanced argument handling for complex data types.

Key changes:

  • Complete rewrite of Halmos log parsing from line-by-line to block-based approach
  • New function generation system with improved struct, array, and bytes parameter support
  • Enhanced address book parsing and contract resolution for better test reproduction
  • Added ethers dependency for address validation and formatting

Reviewed Changes

Copilot reviewed 10 out of 15 changed files in this pull request and generated 3 comments.

Show a summary per file
File Description
tests/halmos.test.ts Removes all existing Halmos parser tests (651 lines deleted)
src/reportBuilder/reportBuilder.ts Updates function calls to use new Halmos API with additional parameters
src/main.ts Changes from line-by-line to full log processing for Halmos
src/index.ts Removes halmosSequenceToFunction export from public API
src/halmos/parameterUtils.ts Completely removes parameter utility functions (204 lines deleted)
src/halmos/logParser.ts Completely removes existing log parser implementation (324 lines deleted)
src/halmos/index.ts Complete rewrite with new block-based processing approach
src/halmos/functionGenerator.ts Complete rewrite with enhanced argument materialization and contract resolution
src/halmos/arrayUtils.ts Completely removes array utility functions (383 lines deleted)
package.json Adds ethers v6.15.0 dependency for address handling

Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.

const m = /^CALL\s+([^:]+)::([^\(]+)\((.*)\)/.exec(sanitized.replace(/^\s+/, ""));
if (!m) {
// Try form where left is a hex address: CALL 0xaaaa0003::increment()
const fm = /^CALL\s+(0x[a-fA-F0-9]{8,40})::([^\(]+)\((.*)\)/.exec(sanitized.replace(/^\s+/, ""));
Copy link

Copilot AI Sep 22, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Magic number 40 represents the length of an Ethereum address in hex characters. Consider extracting this to a named constant like ADDRESS_HEX_LENGTH = 40 for better maintainability.

Copilot uses AI. Check for mistakes.
}
}

const DEFAULT_SENDER = normalizeAddress("0x1804c8ab1f12e6bbf3894d4083f33e07309d1f38");
Copy link

Copilot AI Sep 22, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This hardcoded default sender address appears to be a magic value. Consider extracting it to a configuration constant or documenting why this specific address is used as the default.

Suggested change
const DEFAULT_SENDER = normalizeAddress("0x1804c8ab1f12e6bbf3894d4083f33e07309d1f38");
// Default sender address used for test environments; matches Ganache's first account.
const DEFAULT_SENDER_ADDRESS = "0x1804c8ab1f12e6bbf3894d4083f33e07309d1f38";
const DEFAULT_SENDER = normalizeAddress(DEFAULT_SENDER_ADDRESS);

Copilot uses AI. Check for mistakes.
function normalizeAddress(raw: string): string {
let h = raw.toLowerCase();
if (h.startsWith("0x")) h = h.slice(2);
if (h.length > 40) h = h.slice(h.length - 40); // keep right-most 20 bytes
Copy link

Copilot AI Sep 22, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Magic number 40 represents the length of an Ethereum address in hex characters. Consider extracting this to a named constant for consistency with other address-related operations.

Copilot uses AI. Check for mistakes.
@GalloDaSballo GalloDaSballo merged commit d30439f into main Sep 23, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants