Btor2Xcfa by szaboeva2004 · Pull Request #348 · ftsrg/theta

szaboeva2004 · 2025-03-03T11:08:57Z

🚀 Description

This PR introduces a direct frontend and transformation pipeline for BTOR2 hardware descriptions. By bypassing external intermediate C translation steps (such as Btor2C), this direct approach avoids the semantic mismatches and structural bloat associated with simulating hardware concurrency in sequential C code.

Key Impacts:

Significantly Reduces Structural Complexity: The direct transformation yields a highly concise intermediate representation, reducing variable counts by ~66% and atomic statements by ~82% compared to indirect methods.
Enhances Verification Efficiency: Provides a cleaner, less redundant state space that drastically lowers the memory footprint and improves algorithmic success rates, particularly for solvers utilizing predicate abstraction.

🛠️ Key Changes

Frontend & Parsing

Added Unofficial BTOR2 Grammar: Built using ANTLR4 to enable systematic parsing of domain-specific BTOR2 hardware descriptions.
Implemented Visitor Model: Allows for structured extraction and processing of circuit elements for transformation.

Core Logic & Transformation

BTOR2 to XCFA Transformation: Created a direct pipeline that maps hardware circuits to formal verification models.
Native Semantic Preservation: Bit-vector types now map directly to underlying SMT solver types, preserving precise semantics without manual bit-masking or temporary variables.
Natural Loop Representation: Cyclic hardware behavior and state updates are natively expressed as graph loops within the control-flow representation.
Systematic Node Mapping: Accurately maps core BTOR2 concepts, including constants, initial states (init), unconstrained inputs (havoc), sequential operations, safety properties (bad), and state transitions (next).
Optimizations: Implemented Btr2Passes to seamlessly integrate with the existing suite of optimization techniques already provided by Theta.
Witness Generation (Experimental): Added support for BTOR2 witness generation to .sat files. If the input is BTOR2, a .sat file is generated matching the BTOR2 witness format.

🧪 Testing

Manual Testing Resources: Added some HWMCC benchmark .btor2 and configuration files to validate the direct transformation workflow and witness generation, mostly for run configurations.

⚠️ Known Limitations & Future Work

Incomplete Language Support: Currently lacks support for the BTOR2 array sort and associated operations (e.g., read, write), preventing the verification of designs that rely on memory modeling.
Missing Operators: Specific arithmetic and bit-manipulation operators, such as overflow predicates (saddo, uaddo, etc.) and reduction operations (redand, redor, redxor), are not yet supported.
Limited Property Scope: Verification is currently restricted to safety properties (bad states). Liveness properties (e.g., justice, fairness) and other temporal specifications remain unsupported.
Witness Generation Testing: The .sat witness generation feature is experimental and needs to be validated by btor2sim.

✅ Checklist

Added an unofficial BTOR2 grammar
Implemented the Visitor model for the BTOR2 frontend
Implemented BTOR2 circuit to XCFA transformation
Added resources for test purposes
Implemented BTOR2 witness generation to .sat files

…o btor2xcfa

AdamZsofi · 2026-03-30T10:19:52Z

@szaboeva2004

I approved the CI to run, please check when it's done what's left to do based on that - I can already see that spotless needs to be run.
If witness generation is untested, can you remove or at least disable it, please? I think the witnesses can go into a separate PR later. If this is done, please unmark "draft", it's a proper PR now. :)

In the meantime, I'll do a quick review and ask others for review as well, but we can parallelize there.

AdamZsofi · 2026-03-30T10:21:18Z

@mondokm I could not add Dani as a reviewer, but I think it's you two who are the main stakeholders in Btor2Xcfa currently - can either of you please review? Thanks!

AdamZsofi

I left quite a few small tasks, but overall, I think the frontend is a really nice shape, great work! You are almost there. :D

AdamZsofi · 2026-03-30T10:24:07Z

...ts/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/models/Btor2Operation.kt

+
+  override fun getExpr(): Expr<BvType> {
+    val newU: BigInteger = u + BigInteger.valueOf(1)
+    // val newU: BigInteger = if (u == l) u + BigInteger.valueOf(1) else u


remove commented code if not needed

AdamZsofi · 2026-03-30T10:25:53Z

...cts/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/models/Btor2Stateful.kt

+  }
+
+  override fun getStmt(): Stmt {
+    TODO("We might not even need this Stmt for states")


Is this a comment or a todo? What's the solution? If it's not implemented on purpose, please throw an appropriate exception, not a TODO

AdamZsofi · 2026-03-30T10:26:24Z

...cts/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/models/Btor2Stateful.kt

+  }
+
+  override fun getExpr(): Expr<*> {
+    TODO("Not yet implemented")


Why not implemented? Can it be? Or exception instead of TODO?

AdamZsofi · 2026-03-30T10:27:14Z

...ts/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitors/Btor2Visitor.kt

+  private val operationVisitor = OperationVisitor()
+  private val statefulVisitor = StateVisitor()
+
+  // private val logger = ConsoleLogger(Logger.Level.VERBOSE)


Either remove or uncomment. Would be nice to have some verbose level logging, so maybe uncomment, if possible?

Same for all the other logger calls around here.

AdamZsofi · 2026-03-30T10:28:32Z

...frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/visitors/ConstantVisitor.kt

+    val size = sort.width.toInt()
+    val binArray =
+      BooleanArray(size) { index ->
+        val hexDigit = value[index / 4]


These 3 lines are a bit of a magic code - can you maybe leave a short comment on how this formula works here?

AdamZsofi · 2026-03-30T10:33:35Z

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

  var disable: Boolean = false,
  @Parameter(names = ["--induction-solver", "--ind-solver"], description = "Induction solver name")
-  var indSolver: String = "Z3",
+  var indSolver: String = "mathsat:5.6.10",


Was this changed on purpose? If not, change back, please. :)

AdamZsofi · 2026-03-30T10:33:40Z

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

    description = "Interpolation solver name",
  )
-  var itpSolver: String = "Z3",
+  var itpSolver: String = "mathsat:5.6.10",


Was this changed on purpose? If not, change back, please. :)

AdamZsofi · 2026-03-30T10:33:45Z

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

 data class MddConfig(
  @Parameter(names = ["--solver", "--mdd-solver"], description = "MDD solver name")
-  var solver: String = "Z3",
+  var solver: String = "mathsat:5.6.10",


Was this changed on purpose? If not, change back, please. :)

AdamZsofi · 2026-03-30T10:35:12Z

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

 data class Ic3Config(
  @Parameter(names = ["--solver", "--mdd-solver"], description = "MDD solver name")
-  var solver: String = "Z3",
+  var solver: String = "mathsat:5.6.10",


Was this changed on purpose? If not, change back, please. :) (And just use the flag when running Theta, isntead of changing it in code?)

AdamZsofi · 2026-03-30T10:36:22Z

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/Btor2WitnessWriter.kt

@@ -0,0 +1,92 @@
+/*


Please quickly remove the witnesses from this PR to a separate branch, so that half-done code is not merged to master.

mondokm · 2026-03-31T16:20:27Z

...ojects/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/models/Btor2Model.kt

+  fun visit(node: Btor2Const, param: P): R
+}
+
+object Btor2Circuit {


I think the parsed circuit being a singleton object is not a good pattern, we should instantiate a different object for each parsing.

mondokm · 2026-03-31T16:25:18Z

...ts/frontends/btor2-frontend/src/main/java/hu/bme/mit/theta/frontend/models/Btor2Operation.kt

+  }
+}
+
+// Ehhez a nidhez vezetünk be egy változót, bekötjük


Please only add english comments, or remove if this is not important

mondokm · 2026-03-31T16:28:04Z

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt

    val visited = mutableSetOf<XcfaEdge>()
    while (toVisit.isNotEmpty()) {
-      val visiting = toVisit.removeFirst()
+      val visiting = toVisit.removeAt(0)


What is the reason for this change? I see that it was applied to quite a few files

mondokm · 2026-03-31T16:29:04Z

subprojects/xcfa/xcfa-cli/.z3-trace

Please remove this

mondokm · 2026-03-31T16:31:05Z

subprojects/xcfa/xcfa-cli/build.gradle.kts

    implementation("com.zaxxer:nuprocess:2.0.5")
    implementation("org.jetbrains.kotlin:kotlin-scripting-jsr223:${Versions.kotlin}")
+    implementation(project(mapOf("path" to ":theta-btor2-frontend")))
+    implementation(project(mapOf("path" to ":theta-btor2xcfa")))


Pleae use the format that is used above for both imports:
implementation(project(":theta-btor2-frontend"))
implementation(project(":theta-btor2xcfa"))

mondokm · 2026-03-31T16:31:22Z

.z3-trace

Please remove this

szaboeva2004 added 3 commits February 25, 2025 14:07

Btor2 is now in project

7c5019b

Btor2Xcfa, tests are good and running

d5e44a1

Examples added, println changed to logger

3cdde30

szaboeva2004 marked this pull request as ready for review March 3, 2025 11:09

szaboeva2004 marked this pull request as draft March 3, 2025 11:09

Merge branch 'ftsrg:master' into btor2xcfa

f62bb8c

AdamZsofi self-requested a review March 3, 2025 12:41

AdamZsofi added enhancement xcfa Issue is XCFA specific (not core or XSTS or other formalisms) labels Mar 3, 2025

szaboeva2004 and others added 21 commits March 4, 2025 12:53

Fixed up logger, count2&4 works

5ee57f9

Merge branch 'btor2xcfa' of https://github.com/szaboeva2004/theta int…

3414084

…o btor2xcfa

Visitors, models are reworked (ongoing)

2bd77ab

Model reworked, grammar changed according to btor2tools

3e903f4

Merge branch 'ftsrg:master' into btor2xcfa

798b83c

Added operation expressions

43f8d05

Zsófi konzi

886d110

Zsófi konzi

faa0235

fixed ref for btor2bad get expr

fd99e2f

Small changes in models and visitors

72aa8a6

Btor2 config added

ad9c4a7

Checks added

15fa41c

Run config added

73ff08f

procedure to initial proc fix

1f8300e

Added more resources and minuses

bab1bc3

Minus still doesn't work

ad98e80

Added visitors and operations, still not working minuses

9b71fde

Binary operators working, comparison still not

bb7446a

Constants have a problem

72ffa57

create instead of of in getExpr in btor2

c0823fe

removed booltype, todo ite

f5b75b3

AdamZsofi and others added 19 commits July 16, 2025 14:57

added bitwise trait to xcfa made from btor2

c1ac755

parsecontext integrated to btor2xcfa

4d91bac

removeFirst to removeAt fix

0179f14

minor remove first fix

4b1f0f9

added missing initial state havocs

87a8b06

minor fix

d5eda86

over-cautious check removed

f80ce52

added some refs instead of expr

78a643c

Mathsat added for local bechmarks

58b44c5

Adding bads right after operations

84d710f

Test file added

8b8a0db

merge mainline theta

be3015d

Enabling all or no optimizations

0b55508

Slight change in function

0ce42ae

Merge remote-tracking branch 'origin/master' into btor2xcfa

0347786

Simple test for havocs

b30a08d

Added witness writer and ran spotless

0c87660

Merge remote-tracking branch 'origin/master' into btor2xcfa

f53a47f

Changed the version to 6.28.0

2787c75

AdamZsofi requested a review from mondokm March 30, 2026 10:20

AdamZsofi requested changes Mar 30, 2026

View reviewed changes

AdamZsofi requested a review from dantpu March 31, 2026 12:42

mondokm reviewed Mar 31, 2026

View reviewed changes

subprojects/xcfa/xcfa-cli/.z3-trace

Copy link
Copy Markdown

Contributor

mondokm Mar 31, 2026

Choose a reason for hiding this comment

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

Please remove this

mondokm reviewed Mar 31, 2026

View reviewed changes

.z3-trace

Copy link
Copy Markdown

Contributor

mondokm Mar 31, 2026

Choose a reason for hiding this comment

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

Please remove this

Conversation

szaboeva2004 commented Mar 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🚀 Description

🛠️ Key Changes

Frontend & Parsing

Core Logic & Transformation

🧪 Testing

⚠️ Known Limitations & Future Work

✅ Checklist

Uh oh!

AdamZsofi commented Mar 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

AdamZsofi commented Mar 30, 2026

Uh oh!

AdamZsofi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

szaboeva2004 commented Mar 3, 2025 •

edited

Loading

AdamZsofi commented Mar 30, 2026 •

edited

Loading