Skip to content

Commit

Permalink
Try to fix Windows build
Browse files Browse the repository at this point in the history
  • Loading branch information
@hermanventer
hermanventer committed Dec 3, 2024
1 parent 68a2400 commit 59177ae
Show file tree
Hide file tree
Showing 7 changed files with 183 additions and 184 deletions.
Binary file modified binaries/summary_store.tar
View file
Binary file not shown.
14 changes: 7 additions & 7 deletions checker/src/call_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@
// This source code is licensed under the MIT license found in the
// LICENSE file in the root directory of this source tree.

use core::f16;
// use std::{f16, f64, f128};
use std::collections::HashMap;
use std::fmt::{Debug, Formatter, Result};
use std::rc::Rc;
use std::{f128, f64};
use std::{f16, f64};

use log_derive::*;

Expand Down Expand Up @@ -2132,11 +2132,11 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx>
let i = unsafe { f64::to_int_unchecked::<i64>(f) };
Rc::new(ConstantDomain::I128(i as i128).into())
}
Expression::CompileTimeConstant(ConstantDomain::F128(v)) => {
let f = f128::from_bits(v);
let i = unsafe { f128::to_int_unchecked::<i128>(f) };
Rc::new(ConstantDomain::I128(i).into())
}
// Expression::CompileTimeConstant(ConstantDomain::F128(v)) => {
// let f = f128::from_bits(v);
// let i = unsafe { f128::to_int_unchecked::<i128>(f) };
// Rc::new(ConstantDomain::I128(i).into())
// }
_ => {
// todo: use a delayed operator that can get specialized away
let target_path = self.block_visitor.visit_rh_place(&self.destination);
Expand Down
1 change: 1 addition & 0 deletions checker/src/cargo_mirai.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -239,6 +239,7 @@ fn call_rustc() {
.unwrap_or_else(|| OsString::from("rustc")),
);
cmd.args(args);
println!("call_rustc with {:?}", cmd);
let exit_status = cmd
.spawn()
.expect("could not run rustc")
Expand Down
243 changes: 121 additions & 122 deletions checker/src/constant_domain.rs
View file

Large diffs are not rendered by default.

61 changes: 29 additions & 32 deletions checker/src/expression.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,13 @@
// This source code is licensed under the MIT license found in the
// LICENSE file in the root directory of this source tree.

use std::collections::HashSet;
use std::fmt::{Debug, Formatter, Result};
use std::rc::Rc;

use log_derive::*;
use serde::{Deserialize, Serialize};

use mirai_annotations::*;
use rustc_middle::ty::{FloatTy, IntTy, Ty, TyCtxt, TyKind, UintTy};
use serde::{Deserialize, Serialize};
use std::collections::HashSet;
use std::fmt::{Debug, Formatter, Result};
use std::rc::Rc;

use crate::abstract_value::{AbstractValue, AbstractValueTrait};
use crate::constant_domain::ConstantDomain;
Expand Down Expand Up @@ -1049,11 +1047,11 @@ impl Expression {
| KnownNames::StdIntrinsicsMinnumf64
| KnownNames::StdIntrinsicsPowf64
| KnownNames::StdIntrinsicsPowif64 => ExpressionType::F64,
KnownNames::StdIntrinsicsCopysignf128
| KnownNames::StdIntrinsicsMaxnumf128
| KnownNames::StdIntrinsicsMinnumf128
| KnownNames::StdIntrinsicsPowf128
| KnownNames::StdIntrinsicsPowif128 => ExpressionType::F128,
// KnownNames::StdIntrinsicsCopysignf128
// | KnownNames::StdIntrinsicsMaxnumf128
// | KnownNames::StdIntrinsicsMinnumf128
// | KnownNames::StdIntrinsicsPowf128
// | KnownNames::StdIntrinsicsPowif128 => ExpressionType::F128,
KnownNames::StdIntrinsicsFaddAlgebraic
| KnownNames::StdIntrinsicsFaddFast
| KnownNames::StdIntrinsicsFdivAlgebraic
Expand Down Expand Up @@ -1140,23 +1138,22 @@ impl Expression {
| KnownNames::StdIntrinsicsSinf64
| KnownNames::StdIntrinsicsSqrtf64
| KnownNames::StdIntrinsicsTruncf64 => ExpressionType::F64,
KnownNames::StdIntrinsicsCeilf128
| KnownNames::StdIntrinsicsCosf128
| KnownNames::StdIntrinsicsFloorf128
| KnownNames::StdIntrinsicsExp2f128
| KnownNames::StdIntrinsicsExpf128
| KnownNames::StdIntrinsicsFabsf128
| KnownNames::StdIntrinsicsLog10f128
| KnownNames::StdIntrinsicsLog2f128
| KnownNames::StdIntrinsicsLogf128
| KnownNames::StdIntrinsicsNearbyintf128
| KnownNames::StdIntrinsicsRintf128
| KnownNames::StdIntrinsicsRoundf128
| KnownNames::StdIntrinsicsRevenf128
| KnownNames::StdIntrinsicsSinf128
| KnownNames::StdIntrinsicsSqrtf128
| KnownNames::StdIntrinsicsTruncf128 => ExpressionType::F128,

// KnownNames::StdIntrinsicsCeilf128
// | KnownNames::StdIntrinsicsCosf128
// | KnownNames::StdIntrinsicsFloorf128
// | KnownNames::StdIntrinsicsExp2f128
// | KnownNames::StdIntrinsicsExpf128
// | KnownNames::StdIntrinsicsFabsf128
// | KnownNames::StdIntrinsicsLog10f128
// | KnownNames::StdIntrinsicsLog2f128
// | KnownNames::StdIntrinsicsLogf128
// | KnownNames::StdIntrinsicsNearbyintf128
// | KnownNames::StdIntrinsicsRintf128
// | KnownNames::StdIntrinsicsRoundf128
// | KnownNames::StdIntrinsicsRevenf128
// | KnownNames::StdIntrinsicsSinf128
// | KnownNames::StdIntrinsicsSqrtf128
// | KnownNames::StdIntrinsicsTruncf128 => ExpressionType::F128,
_ => assume_unreachable!("invalid name {:?} for intrinsic unary", name),
},
Expression::BitXor { left, .. } => left.expression.infer_type(),
Expand Down Expand Up @@ -1421,7 +1418,7 @@ pub enum ExpressionType {
F16,
F32,
F64,
F128,
//F128,
I8,
I16,
I32,
Expand Down Expand Up @@ -1449,7 +1446,7 @@ impl From<&ConstantDomain> for ExpressionType {
ConstantDomain::False => Bool,
ConstantDomain::Function(..) => NonPrimitive,
ConstantDomain::I128(..) => I128,
ConstantDomain::F128(..) => F128,
// ConstantDomain::F128(..) => F128,
ConstantDomain::F64(..) => F64,
ConstantDomain::F32(..) => F32,
ConstantDomain::F16(..) => F16,
Expand Down Expand Up @@ -1509,7 +1506,7 @@ impl ExpressionType {
F16 => tcx.types.f16,
F32 => tcx.types.f32,
F64 => tcx.types.f64,
F128 => tcx.types.f128,
// F128 => tcx.types.f128,
I8 => tcx.types.i8,
I16 => tcx.types.i16,
I32 => tcx.types.i32,
Expand Down Expand Up @@ -1594,7 +1591,7 @@ impl ExpressionType {
F16 => 16,
F32 => 32,
F64 => 64,
F128 => 128,
// F128 => 128,
I8 => 8,
I16 => 16,
I32 => 32,
Expand Down
2 changes: 1 addition & 1 deletion checker/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
#![feature(box_patterns)]
#![feature(core_intrinsics)]
#![feature(f16)]
#![feature(f128)]
//#![feature(f128)]
#![allow(clippy::mutable_key_type)]
#![allow(unexpected_cfgs)]

Expand Down
46 changes: 24 additions & 22 deletions checker/src/z3_solver.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,17 @@
// LICENSE file in the root directory of this source tree.
//

use std::ffi::{CStr, CString};
use std::fmt::{Debug, Formatter, Result};
use std::rc::Rc;
use std::sync::Mutex;

use lazy_static::lazy_static;
use log::debug;
use log_derive::*;

use mirai_annotations::*;

use crate::abstract_value::AbstractValue;
use crate::abstract_value::AbstractValueTrait;
use crate::constant_domain::ConstantDomain;
Expand All @@ -13,15 +24,6 @@ use crate::smt_solver::SmtResult;
use crate::smt_solver::SmtSolver;
use crate::tag_domain::Tag;

use lazy_static::lazy_static;
use log::debug;
use log_derive::*;
use mirai_annotations::*;
use std::ffi::{CStr, CString};
use std::fmt::{Debug, Formatter, Result};
use std::rc::Rc;
use std::sync::Mutex;

pub type Z3ExpressionType = z3_sys::Z3_ast;

lazy_static! {
Expand All @@ -37,7 +39,7 @@ pub struct Z3Solver {
f16_sort: z3_sys::Z3_sort,
f64_sort: z3_sys::Z3_sort,
f32_sort: z3_sys::Z3_sort,
f128_sort: z3_sys::Z3_sort,
//f128_sort: z3_sys::Z3_sort,
nearest_even: z3_sys::Z3_ast,
zero: z3_sys::Z3_ast,
one: z3_sys::Z3_ast,
Expand Down Expand Up @@ -74,7 +76,7 @@ impl Z3Solver {
let f16_sort = z3_sys::Z3_mk_fpa_sort_16(z3_context);
let f32_sort = z3_sys::Z3_mk_fpa_sort_32(z3_context);
let f64_sort = z3_sys::Z3_mk_fpa_sort_64(z3_context);
let f128_sort = z3_sys::Z3_mk_fpa_sort_128(z3_context);
//let f128_sort = z3_sys::Z3_mk_fpa_sort_128(z3_context);
let nearest_even = z3_sys::Z3_mk_fpa_round_nearest_ties_to_even(z3_context);
let zero = z3_sys::Z3_mk_int(z3_context, 0, int_sort);
let one = z3_sys::Z3_mk_int(z3_context, 1, int_sort);
Expand All @@ -100,7 +102,7 @@ impl Z3Solver {
f16_sort,
f32_sort,
f64_sort,
f128_sort,
//f128_sort,
nearest_even,
zero,
one,
Expand Down Expand Up @@ -916,7 +918,7 @@ impl Z3Solver {
F16 => self.f16_sort,
F32 => self.f32_sort,
F64 => self.f64_sort,
F128 => self.f128_sort,
// F128 => self.f128_sort,
NonPrimitive | ThinPointer | Unit => self.any_sort,
}
}
Expand Down Expand Up @@ -985,11 +987,11 @@ impl Z3Solver {
let fv = f64::from_bits(*v);
z3_sys::Z3_mk_fpa_numeral_double(self.z3_context, fv, self.f64_sort)
},
ConstantDomain::F128(v) => unsafe {
let num_str = format!("{}", *v);
let c_string = CString::new(num_str).unwrap();
z3_sys::Z3_mk_numeral(self.z3_context, c_string.into_raw(), self.f128_sort)
},
// ConstantDomain::F128(v) => unsafe {
// let num_str = format!("{}", *v);
// let c_string = CString::new(num_str).unwrap();
// z3_sys::Z3_mk_numeral(self.z3_context, c_string.into_raw(), self.f128_sort)
// },
ConstantDomain::U128(v) => unsafe {
let v64 = u64::try_from(*v);
if let Ok(v64) = v64 {
Expand Down Expand Up @@ -1545,10 +1547,10 @@ impl Z3Solver {
ConstantDomain::Char(..) | ConstantDomain::I128(..) | ConstantDomain::U128(..) => {
(false, self.get_constant_as_ast(const_domain))
}
ConstantDomain::F16(..)
| ConstantDomain::F32(..)
| ConstantDomain::F64(..)
| ConstantDomain::F128(..) => (true, self.get_constant_as_ast(const_domain)),
ConstantDomain::F16(..) | ConstantDomain::F32(..) | ConstantDomain::F64(..) => {
(true, self.get_constant_as_ast(const_domain))
}
//| ConstantDomain::F128(..) => (true, self.get_constant_as_ast(const_domain)),
ConstantDomain::False => unsafe {
(false, z3_sys::Z3_mk_int(self.z3_context, 0, self.int_sort))
},
Expand Down

0 comments on commit 59177ae

Please sign in to comment.