1%%% -*- coding: utf-8; erlang-indent-level: 2 -*- 2%%% ------------------------------------------------------------------- 3%%% Copyright 2010-2021 Manolis Papadakis <manopapad@gmail.com>, 4%%% Eirini Arvaniti <eirinibob@gmail.com>, 5%%% and Kostis Sagonas <kostis@cs.ntua.gr> 6%%% 7%%% This file is part of PropEr. 8%%% 9%%% PropEr is free software: you can redistribute it and/or modify 10%%% it under the terms of the GNU General Public License as published by 11%%% the Free Software Foundation, either version 3 of the License, or 12%%% (at your option) any later version. 13%%% 14%%% PropEr is distributed in the hope that it will be useful, 15%%% but WITHOUT ANY WARRANTY; without even the implied warranty of 16%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 17%%% GNU General Public License for more details. 18%%% 19%%% You should have received a copy of the GNU General Public License 20%%% along with PropEr. If not, see <http://www.gnu.org/licenses/>. 21 22%%% @copyright 2010-2021 Manolis Papadakis, Eirini Arvaniti, and Kostis Sagonas 23%%% @version {@version} 24%%% @author Manolis Papadakis 25 26%%% @doc Symbolic datatypes handling functions. 27%%% 28%%% == Symbolic datatypes == 29%%% When writing properties that involve abstract data types, such as dicts or 30%%% sets, it is usually best to avoid dealing with the ADTs' internal 31%%% representation directly. Working, instead, with a symbolic representation of 32%%% the ADT's construction process (series of API calls) has several benefits: 33%%% <ul> 34%%% <li>Failing testcases are easier to read and understand. Compare: 35%%% ``` {call,sets,from_list,[[1,2,3]]} ''' 36%%% with: 37%%% ``` {set,3,16,16,8,80,48, 38%%% {[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]}, 39%%% {{[],[3],[],[],[],[],[2],[],[],[],[],[1],[],[],[],[]}}} '''</li> 40%%% <li>Failing testcases are easier to shrink.</li> 41%%% <li>It is especially useful when testing the datatype itself: Certain 42%%% implementation errors may depend on some particular selection and 43%%% ordering of API calls, thus it is important to cover the entire ADT 44%%% construction API.</li> 45%%% </ul> 46%%% 47%%% PropEr supports the symbolic representation of datatypes, using the 48%%% following syntax: 49%%% <dl> 50%%% <dt>`{call,Module,Function,Arguments}'</dt> 51%%% <dd>This represents a call to the API function `Module:Function' with 52%%% arguments `Arguments'. Each of the arguments may be a symbolic call itself 53%%% or contain other symbolic calls in lists or tuples of arbitrary 54%%% depth.</dd> 55%%% <dt id="$call">``{'$call',Module,Function,Arguments}''</dt> 56%%% <dd>Identical to the above, but gets evaluated automatically before being 57%%% applied to a property.</dd> 58%%% <dt id="var">`{var,'{@type var_id()}`}'</dt> 59%%% <dd>This contruct serves as a placeholder for values that are not known at 60%%% type construction time. It will be replaced by the actual value of the 61%%% variable during evaluation.</dd> 62%%% </dl> 63%%% 64%%% When including the PropEr header file, all 65%%% <a href="#index">API functions</a> of this module are automatically 66%%% imported, unless `PROPER_NO_IMPORTS' is defined. 67%%% 68%%% == Auto-ADT == 69%%% To simplify the symbolic testing of ADTs, PropEr comes with the Auto-ADT 70%%% subsystem: An opaque native type, if exported from its module, is assumed 71%%% to be an abstract data type, causing PropEr to ignore its internal 72%%% representation and instead construct symbolic instances of the type. The 73%%% API functions used in these symbolic instances are extracted from the ADT's 74%%% defining module, which is expected to contain one or more `-spec'ed and 75%%% exported functions that can be used to construct instances of the ADT. 76%%% Specifically, PropEr will use all functions that return at least one 77%%% instance of the ADT. As with recursive native types, the base case is 78%%% automatically detected (in the case of ADTs, calls to functions like 79%%% `new/0' and `from_list/1' would be considered the base case). The produced 80%%% symbolic calls will be <a href="#$call">`$call' tuples</a>, which are 81%%% automatically evaluated, thus no call to {@link eval/1} is required inside 82%%% the property. Produced instances are guaranteed to evaluate successfully. 83%%% Parametric ADTs are supported, so long as they appear fully instantiated 84%%% inside `?FORALL's. 85%%% 86%%% ADTs hard-coded in the Erlang type system (`array', `dict', `digraph', 87%%% `gb_set', `gb_tree', `queue', and `set') are automatically detected and 88%%% handled as such. PropEr also accepts parametric versions of the above ADTs 89%%% in `?FORALL's (`array/1', `dict/2', `gb_set/1', `gb_tree/2', `queue/1', 90%%% `set/1', also `orddict/2' and `ordset/1'). If you would like to use these 91%%% parametric versions in `-type' and `-spec' declarations as well, to better 92%%% document your code and facilitate spec testing, you can include the 93%%% complementary header file `proper/include/proper_param_adts.hrl', which 94%%% provides the corresponding `-type' definitions. Please note that Dialyzer 95%%% currenty treats these the same way as their non-parametric counterparts. 96%%% 97%%% The use of Auto-ADT is currently subject to the following limitations: 98%%% <ul> 99%%% <li>In the ADT's `-opaque' declaration, as in all types' declarations, 100%%% only type variables should be used as parameters in the LHS. None of 101%%% these variables can be the special `_' variable and no variable should 102%%% appear more than once in the parameters.</li> 103%%% <li>ADTs inside specs can only have simple variables as parameters. These 104%%% variables cannot be bound by any is_subtype constraint. Also, the special 105%%% `_' variable is not allowed in ADT parameters. If this would result in 106%%% singleton variables, as in the specs of functions like `new/0', use 107%%% variable names that begin with an underscore.</li> 108%%% <li>Specs that introduce an implicit binding among the parameters of an 109%%% ADT are rejected, e.g.: 110%%% ``` -spec foo(mydict(T,S),mydict(S,T)) -> mydict(T,S). ''' 111%%% This includes using the same type variable twice in the parameters of 112%%% an ADT.</li> 113%%% <li>While parsing the return type of specs in search of ADT references, 114%%% PropEr only recurses into tuples, unions and lists; all other constructs 115%%% are ignored. This prohibits, among others, indirect references to the ADT 116%%% through other custom types and records.</li> 117%%% <li>When encountering a union in the return type, PropEr will pick the 118%%% first choice that can return an ADT. This choice must be distinguishable 119%%% from the others either by having a unique term structure or by having a 120%%% unique tag (if it's a tagged tuple).</li> 121%%% <li>When parsing multi-clause specs, only the first clause is considered. 122%%% </li> 123%%% <li>The only spec constraints we accept are `is_subtype' constraints whose 124%%% first argument is a simple, non-`_' variable. It is not checked whether or 125%%% not these variables actually appear in the spec. The second argument of an 126%%% `is_subtype' constraint cannot contain any non-`_' variables. Multiple 127%%% constraints for the same variable are not supported.</li> 128%%% <li> Unexported opaques and opaques with no suitable specs to serve as API 129%%% calls are silently discarded. Those will be treated like ordinary types. 130%%% </li> 131%%% <li>Unexported or unspecced functions are silently rejected.</li> 132%%% <li>Functions with unsuitable return values are silently rejected.</li> 133%%% <li>Specs that make bad use of variables are silently rejected.</li> 134%%% </ul> 135%%% 136%%% For an example on how to write Auto-ADT-compatible parametric specs, see 137%%% the `examples/stack' module, which contains a simple implementation of a 138%%% stack, or the `proper/proper_dict module', which wraps the `STDLIB' `dict' 139%%% ADT. 140 141 142-module(proper_symb). 143-export([eval/1, eval/2, defined/1, well_defined/1, pretty_print/1, 144 pretty_print/2]). 145-export([internal_eval/1, internal_well_defined/1]). 146 147-export_type([var_values/0]). 148 149-include("proper_internal.hrl"). 150 151 152%%------------------------------------------------------------------------------ 153%% Types 154%%------------------------------------------------------------------------------ 155 156%% -type symb_call() :: {'call' | '$call',mod_name(),fun_name(),[symb_term()]}. 157%% TODO: only atoms are allowed as variable identifiers? 158 159-type var_id() :: atom() | pos_integer(). 160-type var_values() :: [{var_id(),term()}]. 161-type symb_term() :: term(). 162-type handled_term() :: term(). 163-type caller() :: 'user' | 'system'. 164-type call_handler() :: fun((mod_name(),fun_name(),[handled_term()]) -> 165 handled_term()). 166-type term_handler() :: fun((term()) -> handled_term()). 167-type handle_info() :: {caller(),call_handler(),term_handler()}. 168 169 170%%------------------------------------------------------------------------------ 171%% Evaluation functions 172%%------------------------------------------------------------------------------ 173 174%% @equiv eval([], SymbTerm) 175-spec eval(symb_term()) -> term(). 176eval(SymbTerm) -> 177 eval([], SymbTerm). 178 179%% @doc Intended for use inside the property-testing code, this function 180%% evaluates a symbolic instance `SymbTerm'. It also accepts a proplist 181%% `VarValues' that maps variable names to values, which is used to replace any 182%% <a href="#var">var tuples</a> inside `SymbTerm' before proceeding with its 183%% evaluation. 184-spec eval(var_values(), symb_term()) -> term(). 185eval(VarValues, SymbTerm) -> 186 eval(VarValues, SymbTerm, user). 187 188-spec eval(var_values(), symb_term(), caller()) -> term(). 189eval(VarValues, SymbTerm, Caller) -> 190 HandleInfo = {Caller, fun erlang:apply/3, fun(X) -> X end}, 191 symb_walk(VarValues, SymbTerm, HandleInfo). 192 193%% @private 194-spec internal_eval(symb_term()) -> term(). 195internal_eval(SymbTerm) -> 196 eval([], SymbTerm, system). 197 198%% @doc Returns true if the `SymbTerm' symbolic instance can be successfully 199%% evaluated (its evaluation doesn't raise an error or exception). 200-spec defined(symb_term()) -> boolean(). 201defined(SymbTerm) -> 202 defined(SymbTerm, user). 203 204-spec defined(symb_term(), caller()) -> boolean(). 205defined(SymbTerm, Caller) -> 206 try eval([], SymbTerm, Caller) of 207 _Term -> true 208 catch 209 _Exception:_Reason -> false 210 end. 211 212%% @doc An attribute which can be applied to any symbolic generator `SymbType' 213%% that may produce invalid sequences of operations when called. The resulting 214%% generator is guaranteed to only produce well-defined symbolic instances. 215-spec well_defined(proper_types:raw_type()) -> proper_types:type(). 216well_defined(SymbType) -> 217 well_defined(SymbType, user). 218 219-spec well_defined(proper_types:raw_type(), caller()) -> proper_types:type(). 220well_defined(SymbType, Caller) -> 221 ?SUCHTHAT(X, SymbType, defined(X,Caller)). 222 223%% @private 224-spec internal_well_defined(proper_types:type()) -> proper_types:type(). 225internal_well_defined(SymbType) -> 226 well_defined(SymbType, system). 227 228 229%%------------------------------------------------------------------------------ 230%% Pretty-printing functions 231%%------------------------------------------------------------------------------ 232 233%% @equiv pretty_print([], SymbTerm) 234-spec pretty_print(symb_term()) -> string(). 235pretty_print(SymbTerm) -> 236 pretty_print([], SymbTerm). 237 238%% @doc Similar in calling convention to {@link eval/2}, but returns a string 239%% representation of the call sequence `SymbTerm' instead of evaluating it. 240-spec pretty_print(var_values(), symb_term()) -> string(). 241pretty_print(VarValues, SymbTerm) -> 242 HandleInfo = {user, fun parse_fun/3, fun parse_term/1}, 243 ExprTree = symb_walk(VarValues, SymbTerm, HandleInfo), 244 lists:flatten(erl_pp:expr(ExprTree)). 245 246-spec parse_fun(mod_name(), fun_name(), [abs_expr()]) -> abs_expr(). 247parse_fun(Module, Function, ArgTreeList) -> 248 M = erl_syntax:atom(Module), 249 F = erl_syntax:atom(Function), 250 erl_syntax:revert(erl_syntax:application(M, F, ArgTreeList)). 251 252-spec parse_term(term()) -> abs_expr(). 253parse_term(TreeList) when is_list(TreeList) -> 254 {RestOfList, Acc0} = 255 case proper_arith:cut_improper_tail(TreeList) of 256 {_ProperHead,_ImproperTail} = X -> X; 257 ProperList -> {ProperList, erl_syntax:revert(erl_syntax:nil())} 258 end, 259 lists:foldr(fun(X,Acc) -> erl_syntax:revert(erl_syntax:cons(X,Acc)) end, 260 Acc0, RestOfList); 261parse_term(TreeTuple) when is_tuple(TreeTuple) -> 262 erl_syntax:revert(erl_syntax:tuple(tuple_to_list(TreeTuple))); 263parse_term(Term) -> 264 %% TODO: pid, port, reference, function value? 265 erl_parse:abstract(Term). 266 267 268%%------------------------------------------------------------------------------ 269%% Generic symbolic handler function 270%%------------------------------------------------------------------------------ 271 272-spec symb_walk(var_values(), symb_term(), handle_info()) -> handled_term(). 273symb_walk(VarValues, {call,Mod,Fun,Args}, 274 {user,_HandleCall,_HandleTerm} = HandleInfo) -> 275 symb_walk_call(VarValues, Mod, Fun, Args, HandleInfo); 276symb_walk(VarValues, {'$call',Mod,Fun,Args}, HandleInfo) -> 277 symb_walk_call(VarValues, Mod, Fun, Args, HandleInfo); 278symb_walk(VarValues, {var,VarId}, 279 {user,_HandleCall,HandleTerm} = HandleInfo) -> 280 SymbWalk = fun(X) -> symb_walk(VarValues, X, HandleInfo) end, 281 case lists:keyfind(VarId, 1, VarValues) of 282 {VarId,VarValue} -> 283 %% TODO: this allows symbolic calls and vars inside var values, 284 %% which may result in an infinite loop, as in: 285 %% [{a,{call,m,f,[{var,a}]}}], {var,a} 286 SymbWalk(VarValue); 287 false -> 288 HandleTerm({HandleTerm(var),SymbWalk(VarId)}) 289 end; 290symb_walk(VarValues, SymbTerm, HandleInfo) -> 291 symb_walk_gen(VarValues, SymbTerm, HandleInfo). 292 293-spec symb_walk_call(var_values(), mod_name(), fun_name(), [symb_term()], 294 handle_info()) -> handled_term(). 295symb_walk_call(VarValues, Mod, Fun, Args, 296 {_Caller,HandleCall,_HandleTerm} = HandleInfo) -> 297 SymbWalk = fun(X) -> symb_walk(VarValues, X, HandleInfo) end, 298 HandledArgs = [SymbWalk(A) || A <- Args], 299 HandleCall(Mod, Fun, HandledArgs). 300 301-spec symb_walk_gen(var_values(), symb_term(), handle_info()) -> handled_term(). 302symb_walk_gen(VarValues, SymbTerm, 303 {_Caller,_HandleCall,HandleTerm} = HandleInfo) -> 304 SymbWalk = fun(X) -> symb_walk(VarValues, X, HandleInfo) end, 305 Term = do_symb_walk_gen(SymbWalk, SymbTerm), 306 HandleTerm(Term). 307 308-spec do_symb_walk_gen(fun((T) -> S), maybe_improper_list(T,T | [])) -> 309 maybe_improper_list(S,S | []). 310do_symb_walk_gen(SymbWalk, SymbTerm) when is_map(SymbTerm) -> 311 maps:from_list(proper_arith:safe_map(SymbWalk, maps:to_list(SymbTerm))); 312do_symb_walk_gen(SymbWalk, SymbTerm) when is_list(SymbTerm) -> 313 proper_arith:safe_map(SymbWalk, SymbTerm); 314do_symb_walk_gen(SymbWalk, SymbTerm) when is_tuple(SymbTerm) -> 315 proper_arith:tuple_map(SymbWalk, SymbTerm); 316do_symb_walk_gen(_, SymbTerm) -> 317 SymbTerm. 318