Unbreak

common/expressions.cpp

@@ -30,14 +30,14 @@ namespace P4::ToZ3 {
 bool Z3Visitor::preorder(const IR::Constant *c) {
     if (const auto *tb = c->type->to<IR::Type_Bits>()) {
         auto val_string = Util::toString(c->value, 0, false);
-        auto expr = state->get_z3_ctx()->bv_val(val_string, tb->size);
+        auto expr = state->get_z3_ctx()->bv_val(val_string.c_str(), tb->size);
         auto *wrapper = new Z3Bitvector(state, tb, expr, tb->isSigned);
         state->set_expr_result(wrapper);
         return false;
     }
     if (c->type->is<IR::Type_InfInt>()) {
         auto val_string = Util::toString(c->value, 0, false);
-        auto expr = state->get_z3_ctx()->int_val(val_string);
+        auto expr = state->get_z3_ctx()->int_val(val_string.c_str());
         auto *var = new Z3Int(state, expr);
         state->set_expr_result(var);
         return false;
@@ -53,7 +53,7 @@ bool Z3Visitor::preorder(const IR::BoolLiteral *bl) {
 }
 
 bool Z3Visitor::preorder(const IR::StringLiteral *sl) {
-    auto expr = state->get_z3_ctx()->string_val(sl->value);
+    auto expr = state->get_z3_ctx()->string_val(sl->value.c_str());
     auto *wrapper = new Z3Bitvector(state, &STRING_TYPE, expr);
     state->set_expr_result(wrapper);
     return false;
@@ -238,7 +238,7 @@ P4Z3Instance *exec_function(Z3Visitor *visitor, const IR::Function *f) {
 
 P4Z3Instance *exec_method(Z3Visitor *visitor, const IR::Method *m) {
     auto *state = visitor->get_state();
-    auto method_name = infer_name(m->getAnnotations(), m->name.name);
+    auto method_name = infer_name(m, m->name.name);
     const auto *method_type = state->resolve_type(m->type->returnType);
     // TODO: Different types of arguments and multiple calls
     for (const auto *param : *m->getParameters()) {

common/state.cpp

@@ -171,7 +171,7 @@ std::vector<std::pair<z3::expr, P4Z3Instance *>> get_hdr_pairs(P4State *state,
                     auto max_idx = std::min<big_int>(max, size);
                     for (big_int idx = 0; idx < max_idx; ++idx) {
                         auto member_name = Util::toString(idx, 0, false);
-                        auto z3_val = state->get_z3_ctx()->bv_val(member_name, bv_size);
+                        auto z3_val = state->get_z3_ctx()->bv_val(member_name.c_str(), bv_size);
                         tmp_parent_pairs.emplace_back(parent_cond && *expr == z3_val,
                                                       parent_class->get_member(member_name));
                     }
@@ -228,7 +228,7 @@ void set_stack(P4State *state, const MemberStruct &member_struct, P4Z3Instance *
                     auto *orig_val = complex_class->get_member(member_name);
                     const auto *dest_type = complex_class->get_member_type(member_name);
                     auto *cast_val = rval->cast_allocate(dest_type);
-                    auto z3_val = state->get_z3_ctx()->bv_val(member_name, bv_size);
+                    auto z3_val = state->get_z3_ctx()->bv_val(member_name.c_str(), bv_size);
                     cast_val->merge(!(parent_cond && *expr == z3_val), *orig_val);
                     complex_class->update_member(member_name, cast_val);
                 }
@@ -493,15 +493,15 @@ void P4State::copy_out() {
 
 z3::expr P4State::gen_z3_expr(cstring name, const IR::Type *type) {
     if (const auto *tbi = type->to<IR::Type_Bits>()) {
-        return ctx->bv_const(name, tbi->size);
+        return ctx->bv_const(name.c_str(), tbi->size);
     }
     if (const auto *tvb = type->to<IR::Type_Varbits>()) {
-        return ctx->bv_const(name, tvb->size);
+        return ctx->bv_const(name.c_str(), tvb->size);
     }
     if (type->is<IR::Type_Boolean>()) {
-        return ctx->bool_const(name);
+        return ctx->bool_const(name.c_str());
     }
-    BUG("Type \"%s\" not supported for Z3 expressions!.", type);
+    BUG("Type \"%v\" not supported for Z3 expressions!.", type);
 }
 
 P4Z3Instance *P4State::gen_instance(cstring name, const IR::Type *type, uint64_t id) {

common/type_complex.cpp

@@ -161,7 +161,7 @@ void StructBase::bind(const z3::expr *bind_var, uint64_t offset) {
     if (var_width == 0) {
         return;
     }
-    z3::expr tmp_var = state->get_z3_ctx()->bv_const(instance_name, var_width);
+    z3::expr tmp_var = state->get_z3_ctx()->bv_const(instance_name.c_str(), var_width);
     if (bind_var == nullptr) {
         bind_var = &tmp_var;
         offset = var_width;
@@ -401,7 +401,7 @@ void HeaderInstance::isValid(Visitor * /*visitor*/, const IR::Vector<IR::Argumen
 void HeaderInstance::propagate_validity(const z3::expr *valid_expr) {
     if (valid_expr == nullptr) {
         cstring name = instance_name + "_valid";
-        set_valid(state->get_z3_ctx()->bool_const(name));
+        set_valid(state->get_z3_ctx()->bool_const(name.c_str()));
         valid_expr = &valid;
     } else {
         set_valid(*valid_expr);
@@ -565,7 +565,7 @@ P4Z3Instance *StackInstance::get_member(const z3::expr &index) const {
     for (big_int idx = 0; idx < max_idx; ++idx) {
         auto member_name = Util::toString(idx, 0, false);
         const auto *hdr = get_member(member_name);
-        auto z3_int = state->get_z3_ctx()->bv_val(member_name, bv_size);
+        auto z3_int = state->get_z3_ctx()->bv_val(member_name.c_str(), bv_size);
         base_hdr->merge(val == z3_int, *hdr);
     }
     return base_hdr;

common/type_simple.cpp

@@ -395,7 +395,7 @@ Z3Int
 Z3Int::Z3Int(const P4State *state, const z3::expr &val) : NumericVal(state, &INT_TYPE, val) {}
 Z3Int::Z3Int(const P4State *state, const big_int &int_val)
     : NumericVal(state, &INT_TYPE,
-                 state->get_z3_ctx()->int_val(Util::toString(int_val, 0, false))) {}
+                 state->get_z3_ctx()->int_val(Util::toString(int_val, 0, false).c_str())) {}
 
 Z3Int::Z3Int(const P4State *state, int64_t int_val)
     : NumericVal(state, &INT_TYPE, state->get_z3_ctx()->int_val(int_val)) {}
@@ -473,7 +473,7 @@ P4Z3Instance *Z3Int::operatorAddSat(const P4Z3Instance &other) const {
         auto no_underflow = z3::bvadd_no_underflow(cast_val, *other_val->get_val());
         auto sort = cast_val.get_sort();
         cstring big_str = get_max_bv_val(sort.bv_size());
-        auto max_val = state->get_z3_ctx()->bv_val(big_str, sort.bv_size());
+        auto max_val = state->get_z3_ctx()->bv_val(big_str.c_str(), sort.bv_size());
         return new Z3Bitvector(
             state, other_val->get_p4_type(),
             z3::ite(no_underflow && no_overflow, cast_val + *other_val->get_val(), max_val));

common/type_table.cpp

@@ -6,6 +6,7 @@
 
 #include "ir/id.h"
 #include "ir/indexed_vector.h"
+#include "ir/ir-generated.h"
 #include "ir/ir.h"
 #include "ir/vector.h"
 #include "ir/visitor.h"
@@ -34,7 +35,8 @@ void process_table_properties(const IR::P4Table *p4t, TableProperties *table_pro
     }
     if (const auto *action_list = p4t->getActionList()) {
         for (const auto *act : action_list->actionList) {
-            for (const auto *anno : act->getAnnotations()->annotations) {
+            // FIXME: This is likely broken logic in the loop below
+            for (const auto *anno : act->getAnnotations()) {
                 if (anno->name.name == "defaultonly") {
                     continue;
                 }
@@ -91,16 +93,12 @@ P4TableInstance::P4TableInstance(P4State *state, const IR::P4Table *p4t)
         apply(visitor, args);
     });
 
-    table_props.table_name = infer_name(p4t->getAnnotations(), p4t->name.name);
+    table_props.table_name = infer_name(p4t, p4t->name.name);
     // We first collect all the necessary properties
     process_table_properties(p4t, &table_props);
     // Also check if the table is invisible to the control plane.
     // This also implies that it cannot be modified.
-    auto annos = p4t->getAnnotations()->annotations;
-    if (std::any_of(annos.begin(), annos.end(),
-                    [](const IR::Annotation *anno) { return anno->name.name == "hidden"; })) {
-        table_props.immutable = true;
-    }
+    table_props.immutable = p4t->hasAnnotation(IR::Annotation::hiddenAnnotation);
 }
 
 P4TableInstance::P4TableInstance(P4State *state, const IR::StatOrDecl *decl, z3::expr hit,
@@ -137,22 +135,23 @@ z3::expr compute_table_hit(Visitor *visitor, P4State *state, cstring table_name,
         cstring key_name = table_name + "_table_key_" + std::to_string(idx);
         const auto key_eval_z3 = val_container->get_val()->simplify();
         const auto key_z3_sort = key_eval_z3.get_sort();
-        const auto key_match = ctx->constant(key_name, key_z3_sort);
+        const auto key_match = ctx->constant(key_name.c_str(), key_z3_sort);
         // It is actually possible to use a variety of types as key.
         // So we have to stay generic and produce a corresponding variable.
         cstring key_string = key->matchType->toString();
         if (key_string == "exact") {
             hit = hit || (key_eval_z3 == key_match);
         } else if (key_string == "lpm") {
+            // FIXME: switch to abseil routines for string manipulations
             cstring mask_name = table_name + "_table_lpm_key_" + std::to_string(idx);
-            const auto mask_var = ctx->constant(mask_name, key_z3_sort);
+            const auto mask_var = ctx->constant(mask_name.c_str(), key_z3_sort);
             auto max_return =
-                ctx->bv_val(get_max_bv_val(key_z3_sort.bv_size()), key_z3_sort.bv_size());
+                ctx->bv_val(get_max_bv_val(key_z3_sort.bv_size()).c_str(), key_z3_sort.bv_size());
             auto lpm_mask = z3::shl(max_return, mask_var).simplify();
             hit = hit || (key_eval_z3 & lpm_mask) == (key_match & lpm_mask);
         } else if (key_string == "ternary") {
             cstring mask_name = table_name + "_table_ternary_key_" + std::to_string(idx);
-            const auto mask_var = ctx->constant(mask_name, key_z3_sort);
+            const auto mask_var = ctx->constant(mask_name.c_str(), key_z3_sort);
             hit = hit || (key_eval_z3 & mask_var) == (key_match & mask_var);
         } else if (key_string == "range") {
             cstring min_name = table_name + "_table_min_" + std::to_string(idx);

common/util.cpp

@@ -26,33 +26,31 @@ cstring get_max_bv_val(uint64_t bv_width) {
     return Util::toString(max_return, 0, false);
 }
 
-cstring infer_name(const IR::Annotations *annots, cstring default_name) {
+cstring infer_name(const IR::IAnnotated *node, cstring default_name) {
     // This function is a bit of a hacky way to infer the true name of a
     // declaration. Since there are a couple of passes that rename but add
     // annotations we can infer the original name from the annotation.
     // not sure if this generalizes but this is as close we can get for now
-    for (const auto *anno : annots->annotations) {
+    if (const auto *anno = node->getAnnotation(IR::Annotation::nameAnnotation)) {
         // there is an original name in the form of an annotation
-        if (anno->name.name == "name") {
-            for (const auto *token : anno->body) {
-                // the full name can be a bit more convoluted
-                // we only need the last bit after the dot
-                // so hack it out
-                cstring full_name = token->text;
-                // find the last dot
-                const char *last_dot = full_name.findlast(static_cast<int>('.'));
-                // there is no dot in this string, just return the full name
-                if (last_dot == nullptr) {
-                    return full_name;
-                }
-                // otherwise get the index, remove the dot
-                auto idx = static_cast<size_t>(last_dot - full_name + 1);
-                return token->text.substr(idx);
-            }
-            // if the annotation is a member just get the root name
-            if (const auto *member = anno->expr.to<IR::Member>()) {
-                return member->member.name;
+        for (const auto *token : anno->body) {
+            // the full name can be a bit more convoluted
+            // we only need the last bit after the dot
+            // so hack it out
+            cstring full_name = token->text;
+            // find the last dot
+            const char *last_dot = full_name.findlast(static_cast<int>('.'));
+            // there is no dot in this string, just return the full name
+            if (last_dot == nullptr) {
+                return full_name;
             }
+            // otherwise get the index, remove the dot
+            auto idx = static_cast<size_t>(last_dot - full_name.c_str() + 1);
+            return token->text.substr(idx);
+        }
+        // if the annotation is a member just get the root name
+        if (const auto *member = anno->expr.to<IR::Member>()) {
+            return member->member.name;
         }
     }
 

common/util.h

@@ -37,7 +37,7 @@
 namespace P4::ToZ3 {
 
 cstring get_max_bv_val(uint64_t bv_width);
-cstring infer_name(const IR::Annotations *annots, cstring default_name);
+cstring infer_name(const IR::IAnnotated *node, cstring default_name);
 bool compare_files(const std::filesystem::path &filename1, const std::filesystem::path &filename2);
 int exec(const char *cmd, std::stringstream &output);
 

common/visitor_interpret.cpp

@@ -303,7 +303,7 @@ bool Z3Visitor::preorder(const IR::Declaration_Variable *dv) {
 
 bool Z3Visitor::preorder(const IR::P4ValueSet *pvs) {
     const auto *resolved_type = state->resolve_type(pvs->elementType);
-    auto pvs_name = infer_name(pvs->getAnnotations(), pvs->name.name);
+    auto pvs_name = infer_name(pvs, pvs->name.name);
     auto *instance = state->gen_instance(pvs_name, resolved_type);
     state->declare_var(pvs->name.name, instance, resolved_type);
     return false;