Fix static analysis issues: null dereferences, unsafe casts, branch clones, uninitialized members (#9424)

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/6e64242e-78e5-4807-8369-02baaf405a70

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/ast_lt.cpp

@@ -18,12 +18,12 @@ Revision History:
 --*/
 #include "ast/ast.h"
 
-#define check_symbol(S1,S2) if (S1 != S2) return lt(S1,S2)
-#define check_value(V1,V2) if (V1 != V2) return V1 < V2
-#define check_bool(B1,B2) if (B1 != B2) return !B1 && B2
-#define check_ptr(P1,P2) if (!P1 && P2) return true; if (P1 && !P2) return false
-#define check_ast(T1,T2) if (T1 != T2) { n1 = T1; n2 = T2; goto start; }
-#define check_zstring(S1, S2) if (S1 != S2) return S1 < S2
+#define check_symbol(S1,S2) if ((S1) != (S2)) return lt((S1),(S2))
+#define check_value(V1,V2) if ((V1) != (V2)) return (V1) < (V2)
+#define check_bool(B1,B2) if ((B1) != (B2)) return !(B1) && (B2)
+#define check_ptr(P1,P2) if (!(P1) && (P2)) return true; if ((P1) && !(P2)) return false
+#define check_ast(T1,T2) if ((T1) != (T2)) { n1 = (T1); n2 = (T2); goto start; }
+#define check_zstring(S1, S2) if ((S1) != (S2)) return (S1) < (S2)
 
 #define check_parameter(p1, p2) {                               \
     check_value(p1.get_kind(), p2.get_kind());                  \

src/ast/ast_pp_dot.cpp

@@ -77,7 +77,7 @@ private:
 
     void pp_atomic_step(const expr * e) {
         unsigned id = get_id(e);
-        m_out << "node_" << id << " [shape=box,color=\"yellow\",style=\"filled\",label=\"" << label_of_expr(e) << "\"] ;" << std::endl;
+        m_out << "node_" << id << " [shape=box,color=\"yellow\",style=\"filled\",label=\"" << label_of_expr(e) << "\"] ;" << '\n';
     }
     
     void pp_step(const proof * p) {
@@ -91,7 +91,7 @@ private:
                 m_first ? (m_first=false,"color=\"red\"") : num_parents==0 ? "color=\"yellow\"": "";
             m_out << "node_" << id <<
                 " [shape=box,style=\"filled\",label=\"" << label_of_expr(p_res) << "\""
-                << color << "]" << std::endl;
+                << color << "]" << '\n';
             // now print edges to parents (except last one, which is the result)
             std::string label = p->get_decl()->get_name().str();
             for (unsigned i = 0 ; i < num_parents; ++i) {
@@ -99,7 +99,7 @@ private:
                 // explore parent, also print a link to it
                 push_term(to_app(parent));
                 m_out << "node_" << id << " -> " << "node_" << get_id((expr*)parent)
-                    << "[label=\"" << label << "\"];" << std::endl;;
+                    << "[label=\"" << label << "\"];" << '\n';
             }
         } else {
             pp_atomic_step(p);
@@ -120,11 +120,11 @@ private:
 
 // main printer
 std::ostream & ast_pp_dot::pp(std::ostream & out) const {
-    out << "digraph proof { " << std::endl;
+    out << "digraph proof { " << '\n';
     ast_pp_dot_st pp_st(this, out);
     pp_st.push_term(m_pr);
     pp_st.pp_loop();
-    out << std::endl << " } " << std::endl << std::flush;
+    out << '\n' << " } " << '\n' << std::flush;
     return out;
 }
 

src/ast/ast_smt_pp.cpp

@@ -733,7 +733,8 @@ public:
         m_AUFLIRA("AUFLIRA"),
         // It's much easier to read those testcases with that.
         m_no_lets(no_lets),
-        m_simplify_implies(simplify_implies)
+        m_simplify_implies(simplify_implies),
+        m_top(nullptr)
     {
         m_basic_fid = m.get_basic_family_id();
         m_label_fid = m.mk_family_id("label");

src/ast/ast_util.cpp

@@ -168,7 +168,7 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) {
 }
 
 app* mk_and(ast_manager & m, unsigned num_args, app * const * args) {
-    return to_app(mk_and(m, num_args, (expr* const*) args));
+    return to_app(mk_and(m, num_args, reinterpret_cast<expr* const*>(args)));
 }
 
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {

src/sat/sat_aig_finder.cpp

@@ -192,7 +192,7 @@ namespace sat {
                 return false;
             }
             binary b(~y, x, nullptr);
-            if (!binaries.find(b, b)) {
+            if (!binaries.find(b, b) || !b.use_list) {
                 return false;
             }
             for (auto p : *b.use_list) {

src/smt/arith_eq_solver.cpp

@@ -53,10 +53,7 @@ void arith_eq_solver::prop_mod_const(expr * e, unsigned depth, numeral const& k,
     numeral n;
     bool is_int;
 
-    if (depth == 0) {
-        result = e;
-    }
-    else if (m_util.is_add(e) || m_util.is_mul(e)) {
+    if (depth != 0 && (m_util.is_add(e) || m_util.is_mul(e))) {
         expr_ref_vector args(m);
         expr_ref tmp(m);
         app* a = to_app(e);
@@ -66,7 +63,7 @@ void arith_eq_solver::prop_mod_const(expr * e, unsigned depth, numeral const& k,
         }
         m_arith_rewriter.mk_app(a->get_decl(), args.size(), args.data(), result);
     }
-    else if (m_util.is_numeral(e, n, is_int) && is_int) {
+    else if (depth != 0 && m_util.is_numeral(e, n, is_int) && is_int) {
         result = m_util.mk_numeral(mod(n, k), true);
     }
     else {

src/smt/expr_context_simplifier.cpp

@@ -401,10 +401,7 @@ void expr_strong_context_simplifier::simplify_basic(expr* fml, expr_ref& result)
                     args.push_back(arg);
                 }
             }
-            else if (!m.is_bool(arg)) {
-                args.push_back(arg);
-            }
-            else if (!n2) {                
+            else if (!n2 && m.is_bool(arg)) {                
                 n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
                 todo.push_back(arg);
                 parent_ids.push_back(self_pos);
@@ -677,10 +674,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r
                     args.push_back(arg);
                 }
             }
-            else if (!m.is_bool(arg)) {
-                args.push_back(arg);
-            }
-            else if (!n2) {                
+            else if (!n2 && m.is_bool(arg)) {                
                 n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
                 todo.push_back(arg);
                 parent_ids.push_back(self_pos);

src/smt/mam.cpp

@@ -1115,7 +1115,8 @@ namespace {
                     }
                 }
                 m_mp_already_processed[best_j] = true;
-                SASSERT(best != 0);
+                if (best == nullptr)
+                    continue;
                 app * p                 = best;
                 func_decl * lbl         = p->get_decl();
                 unsigned short num_args = p->get_num_args();
@@ -1225,7 +1226,11 @@ namespace {
 
             SASSERT(head->m_next == 0);
 
-            m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
+            unsigned num_decls = m_qa->get_num_decls();
+            unsigned_vector var_regs(num_decls);
+            for (unsigned i = 0; i < num_decls; ++i)
+                var_regs[i] = static_cast<unsigned>(m_vars[i]);
+            m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, num_decls, var_regs.data()));
 
             for (instruction* curr : m_seq) {
                 head->m_next = curr;