From 1452e9319e66e870d4d964e073c975412ae1c3ab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Sep 2013 17:28:39 -0700 Subject: [PATCH] feat(debug): improve lean_assert macro Signed-off-by: Leonardo de Moura --- src/util/debug.h | 72 +++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 68 insertions(+), 4 deletions(-) diff --git a/src/util/debug.h b/src/util/debug.h index b576babdf..c6cc8d9ae 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #ifndef __has_builtin #define __has_builtin(x) 0 @@ -16,9 +17,6 @@ Author: Leonardo de Moura #define DEBUG_CODE(CODE) #endif -#define lean_assert(COND) DEBUG_CODE({if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }}) -#define lean_cond_assert(TAG, COND) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && !(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }}) - #if __has_builtin(__builtin_unreachable) #define lean_unreachable() __builtin_unreachable() #else @@ -31,7 +29,70 @@ Author: Leonardo de Moura #define lean_verify(COND) (COND) #endif -//! Lean namespace +// LEAN_NARG(ARGS...) return the number of arguments. +// This is a hack based on the following stackoverflow post: +// http://stackoverflow.com/questions/11317474/macro-to-count-number-of-arguments +#define LEAN_COMMASEQ_N() 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0 +#define LEAN_RSEQ_N() 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0 +#define LEAN_ARG_N(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, N, ...) N +#define LEAN_NARG_(ARGS...) LEAN_ARG_N(ARGS) +#define LEAN_HASCOMMA(ARGS...) LEAN_NARG_(ARGS, LEAN_COMMASEQ_N()) +#define LEAN_COMMA() , +#define LEAN_NARG_HELPER3_01(N) 0 +#define LEAN_NARG_HELPER3_00(N) 1 +#define LEAN_NARG_HELPER3_11(N) N +#define LEAN_NARG_HELPER2(a, b, N) LEAN_NARG_HELPER3_ ## a ## b(N) +#define LEAN_NARG_HELPER1(a, b, N) LEAN_NARG_HELPER2(a, b, N) +#define LEAN_NARG(ARGS...) LEAN_NARG_HELPER1(LEAN_HASCOMMA(ARGS), LEAN_HASCOMMA(LEAN_COMMA ARGS ()), LEAN_NARG_(ARGS, LEAN_RSEQ_N())) + +// Hack for LEAN_DISPLAY(ARGS...) +// It works for at most 16 arguments. +#define LEAN_DISPLAY1_CORE(V) lean::debug::display_var(#V, V); +#define LEAN_DISPLAY2_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY1_CORE(REST); +#define LEAN_DISPLAY3_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY2_CORE(REST); +#define LEAN_DISPLAY4_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY3_CORE(REST); +#define LEAN_DISPLAY5_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY4_CORE(REST); +#define LEAN_DISPLAY6_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY5_CORE(REST); +#define LEAN_DISPLAY7_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY6_CORE(REST); +#define LEAN_DISPLAY8_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY7_CORE(REST); +#define LEAN_DISPLAY9_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY8_CORE(REST); +#define LEAN_DISPLAY10_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY9_CORE(REST); +#define LEAN_DISPLAY11_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY10_CORE(REST); +#define LEAN_DISPLAY12_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY11_CORE(REST); +#define LEAN_DISPLAY13_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY12_CORE(REST); +#define LEAN_DISPLAY14_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY13_CORE(REST); +#define LEAN_DISPLAY15_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY14_CORE(REST); +#define LEAN_DISPLAY16_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY15_CORE(REST); +#define LEAN_DISPLAY0() +#define LEAN_DISPLAY1(ARG) std::cerr << "Argument\n"; LEAN_DISPLAY1_CORE(ARG); +#define LEAN_DISPLAY2(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY2_CORE(ARGS); +#define LEAN_DISPLAY3(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY3_CORE(ARGS); +#define LEAN_DISPLAY4(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY4_CORE(ARGS); +#define LEAN_DISPLAY5(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY5_CORE(ARGS); +#define LEAN_DISPLAY6(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY6_CORE(ARGS); +#define LEAN_DISPLAY7(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY7_CORE(ARGS); +#define LEAN_DISPLAY8(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY8_CORE(ARGS); +#define LEAN_DISPLAY9(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY9_CORE(ARGS); +#define LEAN_DISPLAY10(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY10_CORE(ARGS); +#define LEAN_DISPLAY11(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY11_CORE(ARGS); +#define LEAN_DISPLAY12(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY12_CORE(ARGS); +#define LEAN_DISPLAY13(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY13_CORE(ARGS); +#define LEAN_DISPLAY14(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY14_CORE(ARGS); +#define LEAN_DISPLAY15(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY15_CORE(ARGS); +#define LEAN_DISPLAY16(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY16_CORE(ARGS); +#define LEAN_JOIN0(A, B) A ## B +#define LEAN_JOIN(A, B) LEAN_JOIN0(A, B) +#define LEAN_DISPLAY(ARGS...) { LEAN_JOIN(LEAN_DISPLAY, LEAN_NARG(ARGS))(ARGS) } + +#define lean_assert(COND, ARGS...) DEBUG_CODE({if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }}) +#define lean_cond_assert(TAG, COND, ARGS...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && !(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }}) + +#define lean_assert_eq(A, B) lean_assert(A == B, A, B) +#define lean_assert_gt(A, B) lean_assert(A > B, A, B) +#define lean_assert_lt(A, B) lean_assert(A < B, A, B) +#define lean_assert_ge(A, B) lean_assert(A >= B, A, B) +#define lean_assert_le(A, B) lean_assert(A <= B, A, B) + namespace lean { void notify_assertion_violation(char const * file_name, int line, char const * condition); void enable_debug(char const * tag); @@ -39,4 +100,7 @@ void disable_debug(char const * tag); bool is_debug_enabled(char const * tag); void invoke_debugger(); bool has_violations(); +namespace debug { +template void display_var(char const * name, T const & value) { std::cerr << name << " := " << value << "\n"; } +} }