potential fix

lib/kernel/pipeline/compiler/analysis/dataflow_analysis.hpp

@@ -5,6 +5,8 @@
 
 namespace kernel {
 
+using z3_int64_t = std::remove_pointer<function_traits<std::function<decltype(Z3_get_numeral_rational_int64)>>::arg<3>::type>::type;
+
 /** ------------------------------------------------------------------------------------------------------------- *
  * @brief identifyHardPartitionConstraints
  ** ------------------------------------------------------------------------------------------------------------- */
@@ -792,15 +794,13 @@ void PipelineAnalysis::computeDataFlowRates() {
             report_fatal_error("Unexpected Z3 error when attempting to obtain value from model!");
         }
 
-        int64_t z3_num, z3_denom;
+        z3_int64_t z3_num, z3_denom;
         if (LLVM_UNLIKELY(Z3_get_numeral_rational_int64(ctx, value, &z3_num, &z3_denom) != Z3_L_TRUE)) {
             report_fatal_error("Unexpected Z3 error when attempting to convert model value to number!");
         }
-        __int64 num = static_cast<__int64>(z3_num);
-        __int64 denom = static_cast<__int64>(z3_denom);
-        assert (num > 0);
+        assert (z3_num > 0);
 
-        const auto r = Rational{num, denom};
+        const auto r = Rational{z3_num, z3_denom};
         for (unsigned bound = LowerBound; bound <= UpperBound; ++bound) {
             current[kernel][bound] = r;
         }
@@ -836,14 +836,12 @@ void PipelineAnalysis::computeDataFlowRates() {
                         report_fatal_error("Unexpected Z3 error when attempting to obtain value from model!");
                     }
 
-                    int64_t z3_num, z3_denom;
+                    z3_int64_t z3_num, z3_denom;
                     if (LLVM_UNLIKELY(Z3_get_numeral_rational_int64(ctx, value, &z3_num, &z3_denom) != Z3_L_TRUE)) {
                         report_fatal_error("Unexpected Z3 error when attempting to convert model value to number!");
                     }
-                    __int64 num = static_cast<__int64>(z3_num);
-                    __int64 denom = static_cast<__int64>(z3_denom);
-                    assert (num > 0);
-                    current[kernel][bound] = Rational{num, denom};
+                    assert (z3_num > 0);
+                    current[kernel][bound] = Rational{z3_num, z3_denom};
                 }
                 Z3_model_dec_ref(ctx, model);
 

lib/kernel/pipeline/compiler/analysis/partitioning_analysis.hpp

@@ -926,14 +926,12 @@ found:  ++i;
         if (LLVM_UNLIKELY(Z3_model_eval(ctx, model, var, Z3_L_TRUE, &value) != Z3_L_TRUE)) {
             report_fatal_error("Unexpected Z3 error when attempting to obtain value from model!");
         }
-        int64_t z3_num;
+        z3_int64_t z3_num;
         if (LLVM_UNLIKELY(Z3_get_numeral_int64(ctx, value, &z3_num) != Z3_L_TRUE)) {
             report_fatal_error("Unexpected Z3 error when attempting to convert model value to number!");
         }
-        __int64 num = static_cast<__int64>(z3_num);
-        assert (num >= 0 && num < static_cast<__int64>(numOfContractedPartitions));
-        assert (partition_order[num] == -1U);
-        partition_order[num] = i;
+        assert (partition_order[z3_num] == -1U);
+        partition_order[z3_num] = i;
     }
     Z3_model_dec_ref(ctx, model);
     END_SCOPED_REGION
@@ -1199,13 +1197,7 @@ found:  ++i;
     }
 
     std::vector<unsigned> ordering(numOfContractedKernels);
-    #ifndef NDEBUG
-    std::vector<__int64> test(numOfKernels);
-    #endif
 
-    #ifndef NDEBUG
-    std::fill_n(ordering.begin(), numOfContractedKernels, -1U);
-    #endif
     const auto model = Z3_optimize_get_model(ctx, solver);
     Z3_model_inc_ref(ctx, model);
     for (unsigned i = 0; i < numOfKernels; ++i) {
@@ -1217,27 +1209,15 @@ found:  ++i;
         if (LLVM_UNLIKELY(Z3_model_eval(ctx, model, var, Z3_L_TRUE, &value) != Z3_L_TRUE)) {
             report_fatal_error("Unexpected Z3 error when attempting to obtain value from model!");
         }
-        int64_t z3_num;
+        z3_int64_t z3_num;
         if (LLVM_UNLIKELY(Z3_get_numeral_int64(ctx, value, &z3_num) != Z3_L_TRUE)) {
             report_fatal_error("Unexpected Z3 error when attempting to convert model value to number!");
         }
-        __int64 num = static_cast<__int64>(z3_num);
-        assert (num >= 0 && num < static_cast<__int64>(numOfContractedKernels));
-        assert (ordering[num] == -1U);
-        ordering[num] = i;
-        #ifndef NDEBUG
-        test[i] = num;
-        #endif
-    }
-    Z3_model_dec_ref(ctx, model);
 
-    #ifndef NDEBUG
-    for (const auto e : make_iterator_range(edges(C))) {
-        const auto u = source(e, C);
-        const auto v = target(e, C);
-        assert (test[u] < test[v]);
+        assert (ordering[z3_num] == -1U);
+        ordering[z3_num] = i;
     }
-    #endif
+    Z3_model_dec_ref(ctx, model);
 
     Z3_optimize_dec_ref(ctx, solver);
     Z3_del_context(ctx);

lib/kernel/pipeline/compiler/common/common.hpp

@@ -5,9 +5,22 @@
 
 namespace kernel {
 
-#ifndef MSC_VER
-typedef long long int __int64;
-#endif
+template<typename T>
+struct function_traits;
+
+template<typename R, typename ...Args>
+struct function_traits<std::function<R(Args...)>>
+{
+    static const size_t nargs = sizeof...(Args);
+
+    typedef R result_type;
+
+    template <size_t i>
+    struct arg
+    {
+        typedef typename std::tuple_element<i, std::tuple<Args...>>::type type;
+    };
+};
 
 template <typename T, unsigned n = 16>
 using Vec = SmallVector<T, n>;