From 75b12412f551f064a93027cff302b2f697edfd1d Mon Sep 17 00:00:00 2001
From: Aaron Councilman <aaronjc4@illinois.edu>
Date: Wed, 15 Jan 2025 17:20:43 -0600
Subject: [PATCH] Checked CCP

---
 hercules_opt/src/ccp.rs                   | 310 +++++++++++-----------
 juno_samples/nested_ccp/src/main.rs       |   3 +
 juno_samples/nested_ccp/src/nested_ccp.jn |  10 +
 3 files changed, 168 insertions(+), 155 deletions(-)

diff --git a/hercules_opt/src/ccp.rs b/hercules_opt/src/ccp.rs
index 39fab9da..68693e8b 100644
--- a/hercules_opt/src/ccp.rs
+++ b/hercules_opt/src/ccp.rs
@@ -485,7 +485,7 @@ fn ccp_flow_function(
         // TODO: This should really be constant interpreted, since dynamic
         // constants as values are used frequently.
         Node::DynamicConstant { id: _ } => CCPLattice::bottom(),
-        // Interpret unary op on constant. TODO: avoid UB.
+        // Interpret unary op on constant.
         Node::Unary { input, op } => {
             let CCPLattice {
                 ref reachability,
@@ -494,24 +494,24 @@ fn ccp_flow_function(
 
             let new_constant = if let ConstantLattice::Constant(cons) = constant {
                 match (op, cons) {
-                    (UnaryOperator::Not, Constant::Boolean(val)) => ConstantLattice::Constant(Constant::Boolean(!val)),
-                    (UnaryOperator::Not, Constant::Integer8(val)) => ConstantLattice::Constant(Constant::Integer8(!val)),
-                    (UnaryOperator::Not, Constant::Integer16(val)) => ConstantLattice::Constant(Constant::Integer16(!val)),
-                    (UnaryOperator::Not, Constant::Integer32(val)) => ConstantLattice::Constant(Constant::Integer32(!val)),
-                    (UnaryOperator::Not, Constant::Integer64(val)) => ConstantLattice::Constant(Constant::Integer64(!val)),
-                    (UnaryOperator::Not, Constant::UnsignedInteger8(val)) => ConstantLattice::Constant(Constant::UnsignedInteger8(!val)),
-                    (UnaryOperator::Not, Constant::UnsignedInteger16(val)) => ConstantLattice::Constant(Constant::UnsignedInteger16(!val)),
-                    (UnaryOperator::Not, Constant::UnsignedInteger32(val)) => ConstantLattice::Constant(Constant::UnsignedInteger32(!val)),
-                    (UnaryOperator::Not, Constant::UnsignedInteger64(val)) => ConstantLattice::Constant(Constant::UnsignedInteger64(!val)),
-                    (UnaryOperator::Neg, Constant::Integer8(val)) => ConstantLattice::Constant(Constant::Integer8(-val)),
-                    (UnaryOperator::Neg, Constant::Integer16(val)) => ConstantLattice::Constant(Constant::Integer16(-val)),
-                    (UnaryOperator::Neg, Constant::Integer32(val)) => ConstantLattice::Constant(Constant::Integer32(-val)),
-                    (UnaryOperator::Neg, Constant::Integer64(val)) => ConstantLattice::Constant(Constant::Integer64(-val)),
-                    (UnaryOperator::Neg, Constant::Float32(val)) => ConstantLattice::Constant(Constant::Float32(-val)),
-                    (UnaryOperator::Neg, Constant::Float64(val)) => ConstantLattice::Constant(Constant::Float64(-val)),
-                    (UnaryOperator::Cast(_), _) => ConstantLattice::Bottom,
+                    (UnaryOperator::Not, Constant::Boolean(val)) => Some(ConstantLattice::Constant(Constant::Boolean(!val))),
+                    (UnaryOperator::Not, Constant::Integer8(val)) => Some(ConstantLattice::Constant(Constant::Integer8(!val))),
+                    (UnaryOperator::Not, Constant::Integer16(val)) => Some(ConstantLattice::Constant(Constant::Integer16(!val))),
+                    (UnaryOperator::Not, Constant::Integer32(val)) => Some(ConstantLattice::Constant(Constant::Integer32(!val))),
+                    (UnaryOperator::Not, Constant::Integer64(val)) => Some(ConstantLattice::Constant(Constant::Integer64(!val))),
+                    (UnaryOperator::Not, Constant::UnsignedInteger8(val)) => Some(ConstantLattice::Constant(Constant::UnsignedInteger8(!val))),
+                    (UnaryOperator::Not, Constant::UnsignedInteger16(val)) => Some(ConstantLattice::Constant(Constant::UnsignedInteger16(!val))),
+                    (UnaryOperator::Not, Constant::UnsignedInteger32(val)) => Some(ConstantLattice::Constant(Constant::UnsignedInteger32(!val))),
+                    (UnaryOperator::Not, Constant::UnsignedInteger64(val)) => Some(ConstantLattice::Constant(Constant::UnsignedInteger64(!val))),
+                    (UnaryOperator::Neg, Constant::Integer8(val)) => val.checked_neg().map(|v| ConstantLattice::Constant(Constant::Integer8(v))),
+                    (UnaryOperator::Neg, Constant::Integer16(val)) => val.checked_neg().map(|v| ConstantLattice::Constant(Constant::Integer16(v))),
+                    (UnaryOperator::Neg, Constant::Integer32(val)) => val.checked_neg().map(|v| ConstantLattice::Constant(Constant::Integer32(v))),
+                    (UnaryOperator::Neg, Constant::Integer64(val)) => val.checked_neg().map(|v| ConstantLattice::Constant(Constant::Integer64(v))),
+                    (UnaryOperator::Neg, Constant::Float32(val)) => Some(ConstantLattice::Constant(Constant::Float32(-val))),
+                    (UnaryOperator::Neg, Constant::Float64(val)) => Some(ConstantLattice::Constant(Constant::Float64(-val))),
+                    (UnaryOperator::Cast(_), _) => Some(ConstantLattice::Bottom),
                     _ => panic!("Unsupported combination of unary operation and constant value. Did typechecking succeed?")
-                }
+                }.unwrap_or(ConstantLattice::bottom())
             } else {
                 constant.clone()
             };
@@ -521,7 +521,7 @@ fn ccp_flow_function(
                 constant: new_constant,
             }
         }
-        // Interpret binary op on constants. TODO: avoid UB.
+        // Interpret binary op on constants.
         Node::Binary { left, right, op } => {
             let CCPLattice {
                 reachability: ref left_reachability,
@@ -538,146 +538,146 @@ fn ccp_flow_function(
             ) = (left_constant, right_constant)
             {
                 let new_cons = match (op, left_cons, right_cons) {
-                    (BinaryOperator::Add, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val + right_val),
-                    (BinaryOperator::Add, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val + right_val),
-                    (BinaryOperator::Add, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val + right_val),
-                    (BinaryOperator::Add, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val + right_val),
-                    (BinaryOperator::Add, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val + right_val),
-                    (BinaryOperator::Add, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val + right_val),
-                    (BinaryOperator::Add, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val + right_val),
-                    (BinaryOperator::Add, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val + right_val),
-                    (BinaryOperator::Add, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Float32(*left_val + *right_val),
-                    (BinaryOperator::Add, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Float64(*left_val + *right_val),
-                    (BinaryOperator::Sub, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val - right_val),
-                    (BinaryOperator::Sub, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Float32(*left_val - *right_val),
-                    (BinaryOperator::Sub, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Float64(*left_val - *right_val),
-                    (BinaryOperator::Mul, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val * right_val),
-                    (BinaryOperator::Mul, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Float32(*left_val * *right_val),
-                    (BinaryOperator::Mul, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Float64(*left_val * *right_val),
-                    (BinaryOperator::Div, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val / right_val),
-                    (BinaryOperator::Div, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val / right_val),
-                    (BinaryOperator::Div, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val / right_val),
-                    (BinaryOperator::Div, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val / right_val),
-                    (BinaryOperator::Div, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val / right_val),
-                    (BinaryOperator::Div, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val / right_val),
-                    (BinaryOperator::Div, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val / right_val),
-                    (BinaryOperator::Div, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val / right_val),
-                    (BinaryOperator::Div, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Float32(*left_val / *right_val),
-                    (BinaryOperator::Div, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Float64(*left_val / *right_val),
-                    (BinaryOperator::Rem, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val % right_val),
-                    (BinaryOperator::Rem, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Float32(*left_val % *right_val),
-                    (BinaryOperator::Rem, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Float64(*left_val % *right_val),
-                    (BinaryOperator::LT, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::Boolean(left_val < right_val),
-                    (BinaryOperator::LT, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Boolean(*left_val < *right_val),
-                    (BinaryOperator::LT, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Boolean(*left_val < *right_val),
-                    (BinaryOperator::LTE, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::Boolean(left_val <= right_val),
-                    (BinaryOperator::LTE, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Boolean(*left_val <= *right_val),
-                    (BinaryOperator::LTE, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Boolean(*left_val <= *right_val),
-                    (BinaryOperator::GT, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::Boolean(left_val > right_val),
-                    (BinaryOperator::GT, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Boolean(*left_val > *right_val),
-                    (BinaryOperator::GT, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Boolean(*left_val > *right_val),
-                    (BinaryOperator::GTE, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::Boolean(left_val >= right_val),
-                    (BinaryOperator::GTE, Constant::Float32(left_val), Constant::Float32(right_val)) => Constant::Boolean(*left_val >= *right_val),
-                    (BinaryOperator::GTE, Constant::Float64(left_val), Constant::Float64(right_val)) => Constant::Boolean(*left_val >= *right_val),
+                    (BinaryOperator::Add, Constant::Integer8(left_val), Constant::Integer8(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::Integer8(v)),
+                    (BinaryOperator::Add, Constant::Integer16(left_val), Constant::Integer16(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::Integer16(v)),
+                    (BinaryOperator::Add, Constant::Integer32(left_val), Constant::Integer32(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::Integer32(v)),
+                    (BinaryOperator::Add, Constant::Integer64(left_val), Constant::Integer64(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::Integer64(v)),
+                    (BinaryOperator::Add, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::UnsignedInteger8(v)),
+                    (BinaryOperator::Add, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::UnsignedInteger16(v)),
+                    (BinaryOperator::Add, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::UnsignedInteger32(v)),
+                    (BinaryOperator::Add, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => left_val.checked_add(*right_val).map(|v| Constant::UnsignedInteger64(v)),
+                    (BinaryOperator::Add, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Float32(*left_val + *right_val)),
+                    (BinaryOperator::Add, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Float64(*left_val + *right_val)),
+                    (BinaryOperator::Sub, Constant::Integer8(left_val), Constant::Integer8(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::Integer8(v)),
+                    (BinaryOperator::Sub, Constant::Integer16(left_val), Constant::Integer16(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::Integer16(v)),
+                    (BinaryOperator::Sub, Constant::Integer32(left_val), Constant::Integer32(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::Integer32(v)),
+                    (BinaryOperator::Sub, Constant::Integer64(left_val), Constant::Integer64(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::Integer64(v)),
+                    (BinaryOperator::Sub, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::UnsignedInteger8(v)),
+                    (BinaryOperator::Sub, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::UnsignedInteger16(v)),
+                    (BinaryOperator::Sub, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::UnsignedInteger32(v)),
+                    (BinaryOperator::Sub, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => left_val.checked_sub(*right_val).map(|v| Constant::UnsignedInteger64(v)),
+                    (BinaryOperator::Sub, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Float32(*left_val - *right_val)),
+                    (BinaryOperator::Sub, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Float64(*left_val - *right_val)),
+                    (BinaryOperator::Mul, Constant::Integer8(left_val), Constant::Integer8(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::Integer8(v)),
+                    (BinaryOperator::Mul, Constant::Integer16(left_val), Constant::Integer16(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::Integer16(v)),
+                    (BinaryOperator::Mul, Constant::Integer32(left_val), Constant::Integer32(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::Integer32(v)),
+                    (BinaryOperator::Mul, Constant::Integer64(left_val), Constant::Integer64(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::Integer64(v)),
+                    (BinaryOperator::Mul, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::UnsignedInteger8(v)),
+                    (BinaryOperator::Mul, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::UnsignedInteger16(v)),
+                    (BinaryOperator::Mul, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::UnsignedInteger32(v)),
+                    (BinaryOperator::Mul, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => left_val.checked_mul(*right_val).map(|v| Constant::UnsignedInteger64(v)),
+                    (BinaryOperator::Mul, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Float32(*left_val * *right_val)),
+                    (BinaryOperator::Mul, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Float64(*left_val * *right_val)),
+                    (BinaryOperator::Div, Constant::Integer8(left_val), Constant::Integer8(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::Integer8(v)),
+                    (BinaryOperator::Div, Constant::Integer16(left_val), Constant::Integer16(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::Integer16(v)),
+                    (BinaryOperator::Div, Constant::Integer32(left_val), Constant::Integer32(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::Integer32(v)),
+                    (BinaryOperator::Div, Constant::Integer64(left_val), Constant::Integer64(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::Integer64(v)),
+                    (BinaryOperator::Div, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::UnsignedInteger8(v)),
+                    (BinaryOperator::Div, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::UnsignedInteger16(v)),
+                    (BinaryOperator::Div, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::UnsignedInteger32(v)),
+                    (BinaryOperator::Div, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => left_val.checked_div(*right_val).map(|v| Constant::UnsignedInteger64(v)),
+                    (BinaryOperator::Div, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Float32(*left_val / *right_val)),
+                    (BinaryOperator::Div, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Float64(*left_val / *right_val)),
+                    (BinaryOperator::Rem, Constant::Integer8(left_val), Constant::Integer8(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::Integer8(v)),
+                    (BinaryOperator::Rem, Constant::Integer16(left_val), Constant::Integer16(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::Integer16(v)),
+                    (BinaryOperator::Rem, Constant::Integer32(left_val), Constant::Integer32(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::Integer32(v)),
+                    (BinaryOperator::Rem, Constant::Integer64(left_val), Constant::Integer64(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::Integer64(v)),
+                    (BinaryOperator::Rem, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::UnsignedInteger8(v)),
+                    (BinaryOperator::Rem, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::UnsignedInteger16(v)),
+                    (BinaryOperator::Rem, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::UnsignedInteger32(v)),
+                    (BinaryOperator::Rem, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => left_val.checked_rem(*right_val).map(|v| Constant::UnsignedInteger64(v)),
+                    (BinaryOperator::Rem, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Float32(*left_val % *right_val)),
+                    (BinaryOperator::Rem, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Float64(*left_val % *right_val)),
+                    (BinaryOperator::LT, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::Boolean(left_val < right_val)),
+                    (BinaryOperator::LT, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Boolean(*left_val < *right_val)),
+                    (BinaryOperator::LT, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Boolean(*left_val < *right_val)),
+                    (BinaryOperator::LTE, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::Boolean(left_val <= right_val)),
+                    (BinaryOperator::LTE, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Boolean(*left_val <= *right_val)),
+                    (BinaryOperator::LTE, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Boolean(*left_val <= *right_val)),
+                    (BinaryOperator::GT, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::Boolean(left_val > right_val)),
+                    (BinaryOperator::GT, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Boolean(*left_val > *right_val)),
+                    (BinaryOperator::GT, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Boolean(*left_val > *right_val)),
+                    (BinaryOperator::GTE, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::Boolean(left_val >= right_val)),
+                    (BinaryOperator::GTE, Constant::Float32(left_val), Constant::Float32(right_val)) => Some(Constant::Boolean(*left_val >= *right_val)),
+                    (BinaryOperator::GTE, Constant::Float64(left_val), Constant::Float64(right_val)) => Some(Constant::Boolean(*left_val >= *right_val)),
                     // EQ and NE can be implemented more easily, since we don't
                     // need to unpack the constants.
-                    (BinaryOperator::EQ, left_val, right_val) => Constant::Boolean(left_val == right_val),
-                    (BinaryOperator::NE, left_val, right_val) => Constant::Boolean(left_val != right_val),
-                    (BinaryOperator::Or, Constant::Boolean(left_val), Constant::Boolean(right_val)) => Constant::Boolean(*left_val || *right_val),
-                    (BinaryOperator::Or, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val | right_val),
-                    (BinaryOperator::Or, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val | right_val),
-                    (BinaryOperator::Or, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val | right_val),
-                    (BinaryOperator::Or, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val | right_val),
-                    (BinaryOperator::Or, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val | right_val),
-                    (BinaryOperator::Or, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val | right_val),
-                    (BinaryOperator::Or, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val | right_val),
-                    (BinaryOperator::Or, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val | right_val),
-                    (BinaryOperator::And, Constant::Boolean(left_val), Constant::Boolean(right_val)) => Constant::Boolean(*left_val && *right_val),
-                    (BinaryOperator::And, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val & right_val),
-                    (BinaryOperator::And, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val & right_val),
-                    (BinaryOperator::And, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val & right_val),
-                    (BinaryOperator::And, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val & right_val),
-                    (BinaryOperator::And, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val & right_val),
-                    (BinaryOperator::And, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val & right_val),
-                    (BinaryOperator::And, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val & right_val),
-                    (BinaryOperator::And, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val & right_val),
-                    (BinaryOperator::Xor, Constant::Boolean(left_val), Constant::Boolean(right_val)) => Constant::Boolean(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val ^ right_val),
-                    (BinaryOperator::Xor, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val ^ right_val),
-                    (BinaryOperator::LSh, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val << right_val),
-                    (BinaryOperator::LSh, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val << right_val),
-                    (BinaryOperator::LSh, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val << right_val),
-                    (BinaryOperator::LSh, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val << right_val),
-                    (BinaryOperator::LSh, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val << right_val),
-                    (BinaryOperator::LSh, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val << right_val),
-                    (BinaryOperator::LSh, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val << right_val),
-                    (BinaryOperator::LSh, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val << right_val),
-                    (BinaryOperator::RSh, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Constant::Integer8(left_val >> right_val),
-                    (BinaryOperator::RSh, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Constant::Integer16(left_val >> right_val),
-                    (BinaryOperator::RSh, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Constant::Integer32(left_val >> right_val),
-                    (BinaryOperator::RSh, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Constant::Integer64(left_val >> right_val),
-                    (BinaryOperator::RSh, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Constant::UnsignedInteger8(left_val >> right_val),
-                    (BinaryOperator::RSh, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Constant::UnsignedInteger16(left_val >> right_val),
-                    (BinaryOperator::RSh, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Constant::UnsignedInteger32(left_val >> right_val),
-                    (BinaryOperator::RSh, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Constant::UnsignedInteger64(left_val >> right_val),
+                    (BinaryOperator::EQ, left_val, right_val) => Some(Constant::Boolean(left_val == right_val)),
+                    (BinaryOperator::NE, left_val, right_val) => Some(Constant::Boolean(left_val != right_val)),
+                    (BinaryOperator::Or, Constant::Boolean(left_val), Constant::Boolean(right_val)) => Some(Constant::Boolean(*left_val || *right_val)),
+                    (BinaryOperator::Or, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Integer8(left_val | right_val)),
+                    (BinaryOperator::Or, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Integer16(left_val | right_val)),
+                    (BinaryOperator::Or, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Integer32(left_val | right_val)),
+                    (BinaryOperator::Or, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Integer64(left_val | right_val)),
+                    (BinaryOperator::Or, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::UnsignedInteger8(left_val | right_val)),
+                    (BinaryOperator::Or, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::UnsignedInteger16(left_val | right_val)),
+                    (BinaryOperator::Or, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::UnsignedInteger32(left_val | right_val)),
+                    (BinaryOperator::Or, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::UnsignedInteger64(left_val | right_val)),
+                    (BinaryOperator::And, Constant::Boolean(left_val), Constant::Boolean(right_val)) => Some(Constant::Boolean(*left_val && *right_val)),
+                    (BinaryOperator::And, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Integer8(left_val & right_val)),
+                    (BinaryOperator::And, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Integer16(left_val & right_val)),
+                    (BinaryOperator::And, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Integer32(left_val & right_val)),
+                    (BinaryOperator::And, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Integer64(left_val & right_val)),
+                    (BinaryOperator::And, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::UnsignedInteger8(left_val & right_val)),
+                    (BinaryOperator::And, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::UnsignedInteger16(left_val & right_val)),
+                    (BinaryOperator::And, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::UnsignedInteger32(left_val & right_val)),
+                    (BinaryOperator::And, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::UnsignedInteger64(left_val & right_val)),
+                    (BinaryOperator::Xor, Constant::Boolean(left_val), Constant::Boolean(right_val)) => Some(Constant::Boolean(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Integer8(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Integer16(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Integer32(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Integer64(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::UnsignedInteger8(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::UnsignedInteger16(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::UnsignedInteger32(left_val ^ right_val)),
+                    (BinaryOperator::Xor, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::UnsignedInteger64(left_val ^ right_val)),
+                    (BinaryOperator::LSh, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Integer8(left_val << right_val)),
+                    (BinaryOperator::LSh, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Integer16(left_val << right_val)),
+                    (BinaryOperator::LSh, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Integer32(left_val << right_val)),
+                    (BinaryOperator::LSh, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Integer64(left_val << right_val)),
+                    (BinaryOperator::LSh, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::UnsignedInteger8(left_val << right_val)),
+                    (BinaryOperator::LSh, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::UnsignedInteger16(left_val << right_val)),
+                    (BinaryOperator::LSh, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::UnsignedInteger32(left_val << right_val)),
+                    (BinaryOperator::LSh, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::UnsignedInteger64(left_val << right_val)),
+                    (BinaryOperator::RSh, Constant::Integer8(left_val), Constant::Integer8(right_val)) => Some(Constant::Integer8(left_val >> right_val)),
+                    (BinaryOperator::RSh, Constant::Integer16(left_val), Constant::Integer16(right_val)) => Some(Constant::Integer16(left_val >> right_val)),
+                    (BinaryOperator::RSh, Constant::Integer32(left_val), Constant::Integer32(right_val)) => Some(Constant::Integer32(left_val >> right_val)),
+                    (BinaryOperator::RSh, Constant::Integer64(left_val), Constant::Integer64(right_val)) => Some(Constant::Integer64(left_val >> right_val)),
+                    (BinaryOperator::RSh, Constant::UnsignedInteger8(left_val), Constant::UnsignedInteger8(right_val)) => Some(Constant::UnsignedInteger8(left_val >> right_val)),
+                    (BinaryOperator::RSh, Constant::UnsignedInteger16(left_val), Constant::UnsignedInteger16(right_val)) => Some(Constant::UnsignedInteger16(left_val >> right_val)),
+                    (BinaryOperator::RSh, Constant::UnsignedInteger32(left_val), Constant::UnsignedInteger32(right_val)) => Some(Constant::UnsignedInteger32(left_val >> right_val)),
+                    (BinaryOperator::RSh, Constant::UnsignedInteger64(left_val), Constant::UnsignedInteger64(right_val)) => Some(Constant::UnsignedInteger64(left_val >> right_val)),
                     _ => panic!("Unsupported combination of binary operation and constant values. Did typechecking succeed?")
                 };
-                ConstantLattice::Constant(new_cons)
+                new_cons.map(|c| ConstantLattice::Constant(c)).unwrap_or(ConstantLattice::bottom())
             } else if (left_constant.is_top() && !right_constant.is_bottom())
                 || (!left_constant.is_bottom() && right_constant.is_top())
             {
diff --git a/juno_samples/nested_ccp/src/main.rs b/juno_samples/nested_ccp/src/main.rs
index 974a488c..f49171ce 100644
--- a/juno_samples/nested_ccp/src/main.rs
+++ b/juno_samples/nested_ccp/src/main.rs
@@ -12,10 +12,13 @@ fn main() {
         let b = HerculesBox::from_slice_mut(&mut b);
         let output_example = ccp_example(a).await;
         let output_median = median_array(9, b).await;
+        let out_no_underflow = no_underflow().await;
         println!("{}", output_example);
         println!("{}", output_median);
+        println!("{}", out_no_underflow);
         assert_eq!(output_example, 1.0);
         assert_eq!(output_median, 18);
+        assert_eq!(out_no_underflow, 7);
     });
 }
 
diff --git a/juno_samples/nested_ccp/src/nested_ccp.jn b/juno_samples/nested_ccp/src/nested_ccp.jn
index ffa2d4f1..aed4e297 100644
--- a/juno_samples/nested_ccp/src/nested_ccp.jn
+++ b/juno_samples/nested_ccp/src/nested_ccp.jn
@@ -28,3 +28,13 @@ fn median_array<n : usize>(arr : i32[n]) -> i32 {
 
   return arr[n / 2];
 }
+
+#[entry]
+fn no_underflow() -> usize {
+  let res = 7;
+
+  let i = 0;
+  if i >= 1 { res = i - 1; }
+
+  return res;
+}
-- 
GitLab