From 12ee1d342c7c4ad36580e5f812dbb8929988d050 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 11 Dec 2015 17:48:40 +0000 Subject: [PATCH 1/4] Improved argument validation in FP API. Fixes #372 --- src/api/api_fpa.cpp | 189 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 189 insertions(+) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index d31d15a1b..daef12d20 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -22,6 +22,30 @@ Notes: #include"api_context.h" #include"fpa_decl_plugin.h" +bool is_fp_sort(Z3_context c, Z3_sort s) { + return mk_c(c)->fpautil().is_float(to_sort(s)); +} + +bool is_fp(Z3_context c, Z3_ast a) { + return mk_c(c)->fpautil().is_float(to_expr(a)); +} + +bool is_rm_sort(Z3_context c, Z3_sort s) { + return mk_c(c)->fpautil().is_rm(to_sort(s)); +} + +bool is_rm(Z3_context c, Z3_ast a) { + return mk_c(c)->fpautil().is_rm(to_expr(a)); +} + +bool is_bv_sort(Z3_context c, Z3_sort s) { + return mk_c(c)->bvutil().is_bv_sort(to_sort(s)); +} + +bool is_bv(Z3_context c, Z3_ast a) { + return mk_c(c)->bvutil().is_bv(to_expr(a)); +} + extern "C" { Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c) { @@ -196,6 +220,11 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_nan(c, s); RESET_ERROR_CODE(); + CHECK_VALID_AST(s, 0); + if (!is_fp_sort(c, s)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_nan(to_sort(s)); ctx->save_ast_trail(a); @@ -207,6 +236,11 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); + CHECK_VALID_AST(s, 0); + if (!is_fp_sort(c, s)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) : ctx->fpautil().mk_pinf(to_sort(s)); @@ -219,6 +253,11 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); + CHECK_VALID_AST(s, 0); + if (!is_fp_sort(c, s)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) : ctx->fpautil().mk_pzero(to_sort(s)); @@ -231,6 +270,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_fp(c, sgn, sig, exp); RESET_ERROR_CODE(); + if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)); ctx->save_ast_trail(a); @@ -242,6 +285,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_numeral_float(c, v, ty); RESET_ERROR_CODE(); + if (!is_fp_sort(c, ty)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, @@ -258,6 +305,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_numeral_double(c, v, ty); RESET_ERROR_CODE(); + if (!is_fp_sort(c, ty)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)), v); @@ -271,6 +322,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_numeral_int(c, v, ty); RESET_ERROR_CODE(); + if (!is_fp_sort(c, ty)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, @@ -287,6 +342,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty); RESET_ERROR_CODE(); + if (!is_fp_sort(c, ty)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, @@ -303,6 +362,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty); RESET_ERROR_CODE(); + if (!is_fp_sort(c, ty)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, @@ -319,6 +382,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_abs(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_abs(to_expr(t)); ctx->save_ast_trail(a); @@ -330,6 +397,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_neg(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_neg(to_expr(t)); ctx->save_ast_trail(a); @@ -341,6 +412,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -352,6 +427,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -363,6 +442,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -374,6 +457,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -385,6 +472,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2) || !is_fp(c, t3)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)); ctx->save_ast_trail(a); @@ -396,6 +487,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_sqrt(c, rm, t); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t)); ctx->save_ast_trail(a); @@ -407,6 +502,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_rem(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -418,6 +517,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_round_to_integral(c, rm, t); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t)); ctx->save_ast_trail(a); @@ -429,6 +532,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_min(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_min(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -440,6 +547,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_max(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_max(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -451,6 +562,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_leq(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_le(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -462,6 +577,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_lt(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -473,6 +592,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_geq(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -484,6 +607,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_gt(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -495,6 +622,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_eq(c, t1, t2); RESET_ERROR_CODE(); + if (!is_fp(c, t1) || !is_fp(c, t2)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2)); ctx->save_ast_trail(a); @@ -506,6 +637,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_is_normal(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_is_normal(to_expr(t)); ctx->save_ast_trail(a); @@ -517,6 +652,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_is_subnormal(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_is_subnormal(to_expr(t)); ctx->save_ast_trail(a); @@ -528,6 +667,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_is_zero(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_is_zero(to_expr(t)); ctx->save_ast_trail(a); @@ -539,6 +682,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_is_infinite(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_is_inf(to_expr(t)); ctx->save_ast_trail(a); @@ -550,6 +697,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_is_nan(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_is_nan(to_expr(t)); ctx->save_ast_trail(a); @@ -561,6 +712,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_is_negative(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_is_negative(to_expr(t)); ctx->save_ast_trail(a); @@ -572,6 +727,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_is_positive(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_is_positive(to_expr(t)); ctx->save_ast_trail(a); @@ -584,6 +743,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_to_fp_bv(c, bv, s); RESET_ERROR_CODE(); + if (!is_bv(c, bv) || !is_fp_sort(c, s)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!ctx->bvutil().is_bv(to_expr(bv)) || @@ -673,6 +836,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz); ctx->save_ast_trail(a); @@ -684,6 +851,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz); RESET_ERROR_CODE(); + if (!is_rm(c, rm) || !is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz); ctx->save_ast_trail(a); @@ -695,6 +866,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_to_real(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); expr * a = ctx->fpautil().mk_to_real(to_expr(t)); ctx->save_ast_trail(a); @@ -707,6 +882,11 @@ extern "C" { LOG_Z3_fpa_get_ebits(c, s); RESET_ERROR_CODE(); CHECK_NON_NULL(s, 0); + CHECK_VALID_AST(s, 0); + if (!is_fp_sort(c, s)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } return mk_c(c)->fpautil().get_ebits(to_sort(s)); Z3_CATCH_RETURN(0); } @@ -716,6 +896,11 @@ extern "C" { LOG_Z3_fpa_get_sbits(c, s); RESET_ERROR_CODE(); CHECK_NON_NULL(s, 0); + CHECK_VALID_AST(s, 0); + if (!is_fp_sort(c, s)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } return mk_c(c)->fpautil().get_sbits(to_sort(s)); Z3_CATCH_RETURN(0); } @@ -838,6 +1023,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fpa_to_ieee_bv(c, t); RESET_ERROR_CODE(); + if (!is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } api::context * ctx = mk_c(c); Z3_ast r = of_ast(ctx->fpautil().mk_to_ieee_bv(to_expr(t))); RETURN_Z3(r); From 3388e1e628af3d69d55ec53c976429c9c889c51a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 11 Dec 2015 18:00:38 +0000 Subject: [PATCH 2/4] Removed superfluous file. --- mk-2013.cmd | 4 ---- 1 file changed, 4 deletions(-) delete mode 100644 mk-2013.cmd diff --git a/mk-2013.cmd b/mk-2013.cmd deleted file mode 100644 index a760b9001..000000000 --- a/mk-2013.cmd +++ /dev/null @@ -1,4 +0,0 @@ -@echo off - -rem Ocaml is VS2013, so need VS2013 command prompt for it to work! -python scripts/mk_make.py -b bld_dbg_2013 --java --ml --debug --vs --parallel=12 From ef06da8c2c09390b84d3846f83d4b500a2a0bc46 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 11 Dec 2015 18:14:14 +0000 Subject: [PATCH 3/4] fix build with gcc --- src/smt/smt_theory.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index f48d75b2e..96a7ac84c 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -22,6 +22,7 @@ Revision History: #include"smt_enode.h" #include"obj_hashtable.h" #include"statistics.h" +#include namespace smt { class model_generator; From 39ca5480d7480ce1462d2d326ef920ce0d0d5973 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 11 Dec 2015 18:18:09 +0000 Subject: [PATCH 4/4] ensure that formula is skolemized in the smt solver when using MBQI Reviewed by Nikolaj Signed-off-by: Nuno Lopes --- src/smt/asserted_formulas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index fa0ec62d4..b66e15cb2 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -259,7 +259,7 @@ void asserted_formulas::reduce() { INVOKE(m_params.m_propagate_booleans, propagate_booleans()); INVOKE(m_params.m_propagate_values, propagate_values()); INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros()); - INVOKE(m_params.m_nnf_cnf, nnf_cnf()); + INVOKE(m_params.m_nnf_cnf || (m_params.m_mbqi && has_quantifiers()), nnf_cnf()); INVOKE(m_params.m_eliminate_and, eliminate_and()); INVOKE(m_params.m_pull_cheap_ite_trees, pull_cheap_ite_trees()); INVOKE(m_params.m_pull_nested_quantifiers && has_quantifiers(), pull_nested_quantifiers());