Fix IntervalAnalysis arith.constant issue with i1 values (#284)

* Fix SMT expression error with arith.constant i1s

* Add changelog

* Revert unneeded formatting change

* Revert "Revert unneeded formatting change"

This reverts commit c87c7c7.

* Fix annoying diff between clang-format versions

* Update lib/Analysis/IntervalAnalysis.cpp

Co-authored-by: Timothy Hoffman <4001421+tim-hoffman@users.noreply.github.com>

---------

Co-authored-by: Timothy Hoffman <4001421+tim-hoffman@users.noreply.github.com>

Author: iangneal

changelogs/unreleased/iangneal__interval_analysis_const_bool_fix.yaml

@@ -0,0 +1,2 @@
+fixed:
+  - Fixed issue with interval analysis in creating SMT expressions for arith.constant operations

include/llzk/Analysis/AnalysisWrappers.h

@@ -221,6 +221,10 @@ class ModuleAnalysis {
     ensure(res.succeeded(), "solver failed to run on module!");
 
     const Context &ctx = getContext();
+    // Force construction of empty results here so `getCurrentResults()` on
+    // a module with no inner structs returns no results rather than an assertion
+    // failure.
+    results[ctx] = {};
     modOp.walk([this, &am, &ctx](component::StructDefOp s) mutable {
       auto &childAnalysis = am.getChildAnalysis<StructAnalysisTy>(s);
       // Don't re-run the analysis if we already have the results.

include/llzk/Analysis/IntervalAnalysis.h

@@ -307,11 +307,20 @@ class IntervalDataFlowAnalysis
 
   llvm::SMTExprRef createFeltSymbol(const char *name) const;
 
-  bool isConstOp(mlir::Operation *op) const {
+  inline bool isConstOp(mlir::Operation *op) const {
     return llvm::isa<
         felt::FeltConstantOp, mlir::arith::ConstantIndexOp, mlir::arith::ConstantIntOp>(op);
   }
 
+  inline bool isBoolConstOp(mlir::Operation *op) const {
+    if (auto constIntOp = llvm::dyn_cast<mlir::arith::ConstantIntOp>(op)) {
+      auto valAttr = dyn_cast<mlir::IntegerAttr>(constIntOp.getValue());
+      ensure(valAttr != nullptr, "arith::ConstantIntOp must have an IntegerAttr as its value");
+      return valAttr.getValue().getBitWidth() == 1;
+    }
+    return false;
+  }
+
   llvm::DynamicAPInt getConst(mlir::Operation *op) const;
 
   inline llvm::SMTExprRef createConstBitvectorExpr(const llvm::DynamicAPInt &v) const {
@@ -322,9 +331,7 @@ class IntervalDataFlowAnalysis
     return smtSolver->mkBitvector(v, field.get().bitWidth());
   }
 
-  llvm::SMTExprRef createConstBoolExpr(bool v) const {
-    return smtSolver->mkBitvector(mlir::APSInt((int)v), field.get().bitWidth());
-  }
+  llvm::SMTExprRef createConstBoolExpr(bool v) const { return smtSolver->mkBoolean(v); }
 
   bool isArithmeticOp(mlir::Operation *op) const {
     return llvm::isa<

lib/Analysis/IntervalAnalysis.cpp

@@ -463,7 +463,13 @@ mlir::LogicalResult IntervalDataFlowAnalysis::visitOperation(
   // Now, the way we update is dependent on the type of the operation.
   if (isConstOp(op)) {
     llvm::DynamicAPInt constVal = getConst(op);
-    llvm::SMTExprRef expr = createConstBitvectorExpr(constVal);
+    llvm::SMTExprRef expr;
+    if (isBoolConstOp(op)) {
+      expr = createConstBoolExpr(constVal != 0);
+    } else {
+      expr = createConstBitvectorExpr(constVal);
+    }
+
     ExpressionValue latticeVal(field.get(), expr, constVal);
     propagateIfChanged(results[0], results[0]->setValue(latticeVal));
   } else if (isArithmeticOp(op)) {
@@ -619,23 +625,28 @@ llvm::SMTExprRef IntervalDataFlowAnalysis::createFeltSymbol(const char *name) co
 llvm::DynamicAPInt IntervalDataFlowAnalysis::getConst(Operation *op) const {
   ensure(isConstOp(op), "op is not a const op");
 
-  llvm::DynamicAPInt fieldConst =
-      TypeSwitch<Operation *, llvm::DynamicAPInt>(op)
-          .Case<FeltConstantOp>([&](FeltConstantOp feltConst) {
-    llvm::APSInt constOpVal(feltConst.getValue());
-    return field.get().reduce(constOpVal);
-  })
-          .Case<arith::ConstantIndexOp>([&](arith::ConstantIndexOp indexConst) {
-    return DynamicAPInt(indexConst.value());
-  })
-          .Case<arith::ConstantIntOp>([&](arith::ConstantIntOp intConst) {
-    return DynamicAPInt(intConst.value());
-  }).Default([](Operation *illegalOp) {
-    std::string err;
-    debug::Appender(err) << "unhandled getConst case: " << *illegalOp;
-    llvm::report_fatal_error(Twine(err));
-    return llvm::DynamicAPInt();
-  });
+  // NOTE: I think clang-format makes these hard to read by default
+  // clang-format off
+  llvm::DynamicAPInt fieldConst = TypeSwitch<Operation *, llvm::DynamicAPInt>(op)
+      .Case<FeltConstantOp>([&](FeltConstantOp feltConst) {
+        llvm::APSInt constOpVal(feltConst.getValue());
+        return field.get().reduce(constOpVal);
+      })
+      .Case<arith::ConstantIndexOp>([&](arith::ConstantIndexOp indexConst) {
+        return DynamicAPInt(indexConst.value());
+      })
+      .Case<arith::ConstantIntOp>([&](arith::ConstantIntOp intConst) {
+        auto valAttr = dyn_cast<IntegerAttr>(intConst.getValue());
+        ensure(valAttr != nullptr, "arith::ConstantIntOp must have an IntegerAttr as its value");
+        return toDynamicAPInt(valAttr.getValue());
+      })
+      .Default([](Operation *illegalOp) {
+        std::string err;
+        debug::Appender(err) << "unhandled getConst case: " << *illegalOp;
+        llvm::report_fatal_error(Twine(err));
+        return llvm::DynamicAPInt();
+      });
+  // clang-format on
   return fieldConst;
 }
 

test/Analysis/interval_analysis/interval_analysis_pass.llzk

@@ -670,3 +670,8 @@ module attributes {veridise.lang = "llzk"} {
 // CHECK-NEXT:     %arg0[@y] in TypeA:[ 0, 255 ]
 // CHECK-NEXT:     %arg0[@z] in TypeF:[ 21888242871839275222246405745257275088696311157297823662689037894645226208328, 255 ]
 // CHECK-NEXT: }
+
+// -----
+
+// COM: Regression test to avoid assertion failure on empty modules
+module attributes {veridise.lang = "llzk"} { }

test/Analysis/interval_analysis/interval_analysis_pass_compute.llzk

@@ -604,6 +604,30 @@ module attributes {veridise.lang = "llzk"} {
 
 // -----
 
+module attributes {veridise.lang = "llzk"} {
+  struct.def @ConstBools {
+    struct.field @out : i1
+    function.def @compute() -> !struct.type<@ConstBools> attributes {function.allow_witness} {
+      %self = struct.new : !struct.type<@ConstBools>
+      %true = arith.constant true
+      %false = arith.constant false
+      %res = bool.and %true, %false
+      struct.writef %self[@out] = %res : !struct.type<@ConstBools>, i1
+      function.return %self : !struct.type<@ConstBools>
+    }
+    function.def @constrain(%arg0: !struct.type<@ConstBools>) attributes {function.allow_constraint} {
+      function.return
+    }
+  }
+}
+
+// CHECK-LABEL: @ConstBools StructIntervals {
+// CHECK-NEXT: compute {
+// CHECK-NEXT:    %self[@out] in Degenerate(0)
+// CHECK-NEXT:  }
+
+// -----
+
 module attributes {veridise.lang = "llzk"} {
   struct.def @ArithConstraint {