Trivial change to test repository state

PiperOrigin-RevId: 570109698
kammoh · Oct 2, 2023 · 086e322 · 086e322
1 parent 7e8bada
commit 086e322
Show file tree

Hide file tree

Showing 6 changed files with 50 additions and 66 deletions.
diff --git a/dependency_support/load_external.bzl b/dependency_support/load_external.bzl
@@ -147,13 +147,14 @@ def load_external_repositories():
 
     http_archive(
         name = "z3",
-        urls = ["https://github.com/Z3Prover/z3/archive/z3-4.12.2.tar.gz"],
-        sha256 = "9f58f3710bd2094085951a75791550f547903d75fe7e2fcb373c5f03fc761b8f",
-        strip_prefix = "z3-z3-4.12.2",
+        urls = ["https://github.com/Z3Prover/z3/archive/z3-4.8.8.tar.gz"],
+        sha256 = "6962facdcdea287c5eeb1583debe33ee23043144d0e5308344e6a8ee4503bcff",
+        strip_prefix = "z3-z3-4.8.8",
         build_file = "@com_google_xls//dependency_support/z3:bundled.BUILD.bazel",
-        # Fix gcc 13.x build failure
-        # https://github.com/Z3Prover/z3/issues/6722
-        patches = ["@com_google_xls//dependency_support/z3:6723.patch"],
+        # Fix Undefined Behavior (UB) of overflow in mpz::bitwise_not by cherry picking
+        # https://github.com/Z3Prover/z3/commit/a96f5a9b425b6f5ba7e8ce1c1a75db6683c4bdc9 and
+        # https://github.com/Z3Prover/z3/commit/9ebacd87e2ee8a79adfe128021fbfd444db7857a.
+        patches = ["@com_google_xls//dependency_support/z3:mpz_cpp.patch"],
     )
 
     http_archive(

diff --git a/dependency_support/z3/6723.patch b/dependency_support/z3/6723.patch
diff --git a/dependency_support/z3/build_defs.bzl b/dependency_support/z3/build_defs.bzl
@@ -28,39 +28,39 @@ MK_MAKE_HDRS = [
 ]
 
 PARAMS_HDRS = [
-    "src/model/model_evaluator_params.hpp",
-    "src/model/model_params.hpp",
+    "src/ackermannization/ackermannization_params.hpp",
+    "src/ackermannization/ackermannize_bv_tactic_params.hpp",
+    "src/ast/fpa/fpa2bv_rewriter_params.hpp",
     "src/ast/normal_forms/nnf_params.hpp",
+    "src/ast/pattern/pattern_inference_params_helper.hpp",
     "src/ast/pp_params.hpp",
-    "src/ackermannization/ackermannize_bv_tactic_params.hpp",
-    "src/ackermannization/ackermannization_params.hpp",
-    "src/math/realclosure/rcf_params.hpp",
+    "src/ast/rewriter/arith_rewriter_params.hpp",
+    "src/ast/rewriter/array_rewriter_params.hpp",
+    "src/ast/rewriter/bool_rewriter_params.hpp",
+    "src/ast/rewriter/bv_rewriter_params.hpp",
+    "src/ast/rewriter/fpa_rewriter_params.hpp",
+    "src/ast/rewriter/poly_rewriter_params.hpp",
+    "src/ast/rewriter/rewriter_params.hpp",
+    "src/ast/rewriter/seq_rewriter_params.hpp",
     "src/math/polynomial/algebraic_params.hpp",
-    "src/tactic/sls/sls_params.hpp",
-    "src/tactic/smtlogics/qfufbv_tactic_params.hpp",
-    "src/params/poly_rewriter_params.hpp",
-    "src/params/array_rewriter_params.hpp",
-    "src/params/seq_rewriter_params.hpp",
-    "src/params/fpa_rewriter_params.hpp",
-    "src/params/arith_rewriter_params.hpp",
-    "src/params/rewriter_params.hpp",
-    "src/params/bv_rewriter_params.hpp",
-    "src/params/tactic_params.hpp",
-    "src/params/pattern_inference_params_helper.hpp",
-    "src/params/solver_params.hpp",
-    "src/params/fpa2bv_rewriter_params.hpp",
-    "src/params/bool_rewriter_params.hpp",
-    "src/solver/combined_solver_params.hpp",
-    "src/solver/parallel_params.hpp",
+    "src/math/realclosure/rcf_params.hpp",
+    "src/model/model_params.hpp",
+    "src/model/model_evaluator_params.hpp",
+    "src/muz/base/fp_params.hpp",
+    "src/nlsat/nlsat_params.hpp",
     "src/opt/opt_params.hpp",
     "src/parsers/util/parser_params.hpp",
-    "src/muz/base/fp_params.hpp",
-    "src/sat/sat_params.hpp",
     "src/sat/sat_asymm_branch_params.hpp",
-    "src/sat/sat_simplifier_params.hpp",
+    "src/sat/sat_params.hpp",
     "src/sat/sat_scc_params.hpp",
-    "src/nlsat/nlsat_params.hpp",
+    "src/sat/sat_simplifier_params.hpp",
     "src/smt/params/smt_params_helper.hpp",
+    "src/solver/parallel_params.hpp",
+    "src/solver/solver_params.hpp",
+    "src/solver/combined_solver_params.hpp",
+    "src/tactic/smtlogics/qfufbv_tactic_params.hpp",
+    "src/tactic/sls/sls_params.hpp",
+    "src/tactic/tactic_params.hpp",
 ]
 
 DB_HDRS = [

diff --git a/dependency_support/z3/bundled.BUILD.bazel b/dependency_support/z3/bundled.BUILD.bazel
@@ -60,16 +60,13 @@ cc_library(
         "src/ackermannization/*.cpp",
         "src/api/*.cpp",
         "src/ast/*.cpp",
-        "src/ast/converters/*.cpp",
-        "src/ast/euf/*.cpp",
         "src/ast/fpa/*.cpp",
         "src/ast/macros/*.cpp",
         "src/ast/normal_forms/*.cpp",
         "src/ast/pattern/*.cpp",
         "src/ast/proofs/*.cpp",
         "src/ast/rewriter/*.cpp",
         "src/ast/rewriter/bit_blaster/*.cpp",
-        "src/ast/simplifiers/*.cpp",
         "src/ast/substitution/*.cpp",
         "src/cmd_context/*.cpp",
         "src/cmd_context/extra_cmds/*.cpp",
@@ -99,22 +96,17 @@ cc_library(
         "src/nlsat/*.cpp",
         "src/nlsat/tactic/*.cpp",
         "src/opt/*.cpp",
-        "src/params/*.cpp",
         "src/parsers/smt2/*.cpp",
         "src/parsers/util/*.cpp",
         "src/qe/*.cpp",
-        "src/qe/lite/*.cpp",
-        "src/qe/mbp/*.cpp",
         "src/sat/*.cpp",
         "src/sat/sat_solver/*.cpp",
-        "src/sat/smt/*.cpp",
         "src/sat/tactic/*.cpp",
         "src/smt/*.cpp",
         "src/smt/params/*.cpp",
         "src/smt/proto_model/*.cpp",
         "src/smt/tactic/*.cpp",
         "src/solver/*.cpp",
-        "src/solver/assertions/*.cpp",
         "src/tactic/*.cpp",
         "src/tactic/aig/*.cpp",
         "src/tactic/arith/*.cpp",
@@ -137,10 +129,6 @@ cc_library(
         "src/api/*.hpp",
         "src/ast/*.h",
         "src/ast/*.hpp",
-        "src/ast/converters/*.h",
-        "src/ast/converters/*.hpp",
-        "src/ast/euf/*.h",
-        "src/ast/euf/*.hpp",
         "src/ast/fpa/*.h",
         "src/ast/fpa/*.hpp",
         "src/ast/macros/*.h",
@@ -155,8 +143,6 @@ cc_library(
         "src/ast/rewriter/*.hpp",
         "src/ast/rewriter/bit_blaster/*.h",
         "src/ast/rewriter/bit_blaster/*.hpp",
-        "src/ast/simplifiers/*.h",
-        "src/ast/simplifiers/*.hpp",
         "src/ast/substitution/*.h",
         "src/ast/substitution/*.hpp",
         "src/cmd_context/*.h",
@@ -215,24 +201,16 @@ cc_library(
         "src/nlsat/tactic/*.hpp",
         "src/opt/*.h",
         "src/opt/*.hpp",
-        "src/params/*.h",
-        "src/params/*.hpp",
         "src/parsers/smt2/*.h",
         "src/parsers/smt2/*.hpp",
         "src/parsers/util/*.h",
         "src/parsers/util/*.hpp",
         "src/qe/*.h",
         "src/qe/*.hpp",
-        "src/qe/lite/*.h",
-        "src/qe/lite/*.hpp",
-        "src/qe/mbp/*.h",
-        "src/qe/mbp/*.hpp",
         "src/sat/*.h",
         "src/sat/*.hpp",
         "src/sat/sat_solver/*.h",
         "src/sat/sat_solver/*.hpp",
-        "src/sat/smt/*.h",
-        "src/sat/smt/*.hpp",
         "src/sat/tactic/*.h",
         "src/sat/tactic/*.hpp",
         "src/smt/*.h",
@@ -242,8 +220,6 @@ cc_library(
         "src/smt/tactic/*.hpp",
         "src/solver/*.h",
         "src/solver/*.hpp",
-        "src/solver/assertions/*.h",
-        "src/solver/assertions/*.hpp",
         "src/tactic/*.h",
         "src/tactic/*.hpp",
         "src/tactic/aig/*.h",

diff --git a/dependency_support/z3/mpz_cpp.patch b/dependency_support/z3/mpz_cpp.patch
@@ -0,0 +1,17 @@
+--- src/util/mpz.cpp
++++ src/util/mpz.cpp
+@@ -1460,9 +1460,11 @@ void mpz_manager<SYNCH>::bitwise_xor(mpz const & a, mpz const & b, mpz & c) {
+ template<bool SYNCH>
+ void mpz_manager<SYNCH>::bitwise_not(unsigned sz, mpz const & a, mpz & c) {
+     SASSERT(is_nonneg(a));
+-    if (is_small(a) && sz <= 63) {
+-        int64_t mask = (static_cast<int64_t>(1) << sz) - static_cast<int64_t>(1);
+-        set_i64(c, (~ i64(a)) & mask);
++    if (is_small(a) && sz <= 64) {
++        uint64_t v = ~get_uint64(a);
++        unsigned zero_out = 64 - sz;
++        v = (v << zero_out) >> zero_out;
++        set(c, v);
+     }
+     else {
+         mpz a1, a2, m, tmp;
diff --git a/xls/public/function_builder.h b/xls/public/function_builder.h
@@ -1,4 +1,4 @@
-// Copyright 2021 The XLS Authors
+// Copyright 2023 The XLS Authors
 //
 // Licensed under the Apache License, Version 2.0 (the "License");
 // you may not use this file except in compliance with the License.