diff options
Diffstat (limited to 'lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl')
| -rw-r--r-- | lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl | 215 |
1 files changed, 215 insertions, 0 deletions
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl new file mode 100644 index 0000000000..07243f8d23 --- /dev/null +++ b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl @@ -0,0 +1,215 @@ +%% -*- erlang-indent-level: 2 -*- +%%------------------------------------------------------------------------------ + +%%==================================================================== +%% Types +%%==================================================================== + +%% Code and Monitor servers' info. +-record(svs, { + code :: pid(), + monitor :: pid() +}). + +%% Tags of an AST's node. +-record(tags, { + this = undefined :: cuter_cerl:tag() | undefined, + next = undefined :: cuter_cerl:tag() | undefined +}). + +-type loaded_ret_atoms() :: cover_compiled | preloaded | non_existing. +-type servers() :: #svs{}. +-type ast_tags() :: #tags{}. + +%%==================================================================== +%% Directories +%%==================================================================== + +-define(RELATIVE_TMP_DIR, "temp"). +-define(PYTHON_CALL, ?PYTHON_PATH ++ " -u " ++ ?PRIV ++ "/cuter_interface.py"). + +%%==================================================================== +%% Prefixes +%%==================================================================== + +-define(DEPTH_PREFIX, '__conc_depth'). +-define(EXECUTION_PREFIX, '__conc_prefix'). +-define(SYMBOLIC_PREFIX, '__s'). +-define(CONCOLIC_PREFIX_MSG, '__concm'). +-define(ZIPPED_VALUE_PREFIX, '__czip'). +-define(CONCOLIC_PREFIX_PDICT, '__concp'). +-define(FUNCTION_PREFIX, '__cfunc'). +-define(UNBOUND_VAR_PREFIX, '__uboundvar'). +-define(BRANCH_TAG_PREFIX, '__branch_tag'). +-define(VISITED_TAGS_PREFIX, '__visited_tags'). +-define(EXECUTION_COUNTER_PREFIX, '__exec_counter'). + +%%==================================================================== +%% Flags & Default Values +%%==================================================================== + +-define(LOGGING_FLAG, ok). +-define(DELETE_TRACE, ok). +-define(LOG_UNSUPPORTED_MFAS, ok). +%%-define(VERBOSE_SCHEDULER, ok). +%%-define(VERBOSE_FILE_DELETION, ok). +%%-define(VERBOSE_SOLVING, ok). +%%-define(VERBOSE_MERGING, ok). +%%-define(VERBOSE_REPORTING, ok). +-define(USE_SPECS, ok). + +%%==================================================================== +%% Solver Responses +%%==================================================================== + +-define(RSP_MODEL_DELIMITER_START, <<"model_start">>). +-define(RSP_MODEL_DELIMITER_END, <<"model_end">>). + +%%==================================================================== +%% OpCodes for types in JSON objects +%%==================================================================== + +-define(JSON_TYPE_ANY, 0). +-define(JSON_TYPE_INT, 1). +-define(JSON_TYPE_FLOAT, 2). +-define(JSON_TYPE_ATOM, 3). +-define(JSON_TYPE_LIST, 4). +-define(JSON_TYPE_TUPLE, 5). +-define(JSON_TYPE_PID, 6). +-define(JSON_TYPE_REF, 7). + +%%==================================================================== +%% OpCodes for the commands to the solver +%%==================================================================== + +-define(JSON_CMD_LOAD_TRACE_FILE, 1). +-define(JSON_CMD_SOLVE, 2). +-define(JSON_CMD_GET_MODEL, 3). +-define(JSON_CMD_ADD_AXIOMS, 4). +-define(JSON_CMD_FIX_VARIABLE, 5). +-define(JSON_CMD_RESET_SOLVER, 6). +-define(JSON_CMD_STOP, 42). + +%%==================================================================== +%% OpCodes for constraint types +%%==================================================================== + +-define(CONSTRAINT_TRUE, 1). +-define(CONSTRAINT_FALSE, 2). +-define(NOT_CONSTRAINT, 3). + +-define(CONSTRAINT_TRUE_REPR, 84). %% $T +-define(CONSTRAINT_FALSE_REPR, 70). %% $F + +%%==================================================================== +%% OpCodes of constraints & built-in operations +%%==================================================================== + +%% Empty tag ID +-define(EMPTY_TAG_ID, 0). + +%% MFA's Parameters & Spec definitions. +-define(OP_PARAMS, 1). +-define(OP_SPEC, 2). +%% Constraints. +-define(OP_GUARD_TRUE, 3). +-define(OP_GUARD_FALSE, 4). +-define(OP_MATCH_EQUAL_TRUE, 5). +-define(OP_MATCH_EQUAL_FALSE, 6). +-define(OP_TUPLE_SZ, 7). +-define(OP_TUPLE_NOT_SZ, 8). +-define(OP_TUPLE_NOT_TPL, 9). +-define(OP_LIST_NON_EMPTY, 10). +-define(OP_LIST_EMPTY, 11). +-define(OP_LIST_NOT_LST, 12). +%% Information used for syncing & merging the traces of many processes. +-define(OP_SPAWN, 13). +-define(OP_SPAWNED, 14). +-define(OP_MSG_SEND, 15). +-define(OP_MSG_RECEIVE, 16). +-define(OP_MSG_CONSUME, 17). +%% Necessary operations for the evaluation of Core Erlang. +-define(OP_UNFOLD_TUPLE, 18). +-define(OP_UNFOLD_LIST, 19). +%% Bogus operation (operations interpreted as the identity function). +-define(OP_BOGUS, 48). +%% Type conversions. +-define(OP_FLOAT, 47). +-define(OP_LIST_TO_TUPLE, 52). +-define(OP_TUPLE_TO_LIST, 53). +%% Query types. +-define(OP_IS_INTEGER, 27). +-define(OP_IS_ATOM, 28). +-define(OP_IS_FLOAT, 29). +-define(OP_IS_LIST, 30). +-define(OP_IS_TUPLE, 31). +-define(OP_IS_BOOLEAN, 32). +-define(OP_IS_NUMBER, 33). +%% Arithmetic operations. +-define(OP_PLUS, 34). +-define(OP_MINUS, 35). +-define(OP_TIMES, 36). +-define(OP_RDIV, 37). +-define(OP_IDIV_NAT, 38). +-define(OP_REM_NAT, 39). +-define(OP_UNARY, 40). +%% Operations on atoms. +-define(OP_ATOM_NIL, 49). +-define(OP_ATOM_HEAD, 50). +-define(OP_ATOM_TAIL, 51). +%% Operations on lists. +-define(OP_HD, 25). +-define(OP_TL, 26). +-define(OP_CONS, 56). +%% Operations on tuples. +-define(OP_TCONS, 57). +%% Comparisons. +-define(OP_EQUAL, 41). +-define(OP_UNEQUAL, 42). +-define(OP_LT_INT, 54). +-define(OP_LT_FLOAT, 55). + +%% Maps MFAs to their JSON Opcodes +-define(OPCODE_MAPPING, + dict:from_list([ %% Simulated built-in operations + { {cuter_erlang, atom_to_list_bogus, 1}, ?OP_BOGUS } + , { {cuter_erlang, is_atom_nil, 1}, ?OP_ATOM_NIL } + , { {cuter_erlang, safe_atom_head, 1}, ?OP_ATOM_HEAD } + , { {cuter_erlang, safe_atom_tail, 1}, ?OP_ATOM_TAIL } + , { {cuter_erlang, safe_pos_div, 2}, ?OP_IDIV_NAT } + , { {cuter_erlang, safe_pos_rem, 2}, ?OP_REM_NAT } + , { {cuter_erlang, lt_int, 2}, ?OP_LT_INT } + , { {cuter_erlang, lt_float, 2}, ?OP_LT_FLOAT } + , { {cuter_erlang, safe_plus, 2}, ?OP_PLUS } + , { {cuter_erlang, safe_minus, 2}, ?OP_MINUS } + , { {cuter_erlang, safe_times, 2}, ?OP_TIMES } + , { {cuter_erlang, safe_rdiv, 2}, ?OP_RDIV } + , { {cuter_erlang, safe_float, 1}, ?OP_FLOAT } + , { {cuter_erlang, safe_list_to_tuple, 1}, ?OP_LIST_TO_TUPLE } + , { {cuter_erlang, safe_tuple_to_list, 1}, ?OP_TUPLE_TO_LIST } + , { {bogus_erlang, cons, 2}, ?OP_CONS } + %% Actual erlang BIFs + , { {erlang, hd, 1}, ?OP_HD } + , { {erlang, tl, 1}, ?OP_TL } + , { {erlang, is_integer, 1}, ?OP_IS_INTEGER } + , { {erlang, is_atom, 1}, ?OP_IS_ATOM } + , { {erlang, is_boolean, 1}, ?OP_IS_BOOLEAN } + , { {erlang, is_float, 1}, ?OP_IS_FLOAT } + , { {erlang, is_list, 1}, ?OP_IS_LIST } + , { {erlang, is_tuple, 1}, ?OP_IS_TUPLE } + , { {erlang, is_number, 1}, ?OP_IS_NUMBER } + , { {erlang, '-', 1}, ?OP_UNARY } + , { {erlang, '=:=', 2}, ?OP_EQUAL } + , { {erlang, '=/=', 2}, ?OP_UNEQUAL } + ])). + +%% All the MFAs that are supported for symbolic evaluation. +-define(SUPPORTED_MFAS, gb_sets:from_list(dict:fetch_keys(?OPCODE_MAPPING))). + +-define(UNSUPPORTED_MFAS, + gb_sets:from_list([ {cuter_erlang, unsupported_lt, 2} ])). + +%% The set of all the built-in operations that the solver can try to reverse. +-define (REVERSIBLE_OPERATIONS, + gb_sets:from_list([ ?OP_HD, ?OP_TL + ])). |