1%% -*- erlang-indent-level: 2 -*- 2%% 3%% Licensed under the Apache License, Version 2.0 (the "License"); 4%% you may not use this file except in compliance with the License. 5%% You may obtain a copy of the License at 6%% 7%% http://www.apache.org/licenses/LICENSE-2.0 8%% 9%% Unless required by applicable law or agreed to in writing, software 10%% distributed under the License is distributed on an "AS IS" BASIS, 11%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12%% See the License for the specific language governing permissions and 13%% limitations under the License. 14 15%%%------------------------------------------------------------------- 16%%% File : dialyzer_typesig.erl 17%%% Author : Tobias Lindahl <tobiasl@it.uu.se> 18%%% Description : 19%%% 20%%% Created : 25 Apr 2005 by Tobias Lindahl <tobiasl@it.uu.se> 21%%%------------------------------------------------------------------- 22 23-module(dialyzer_typesig). 24 25-export([analyze_scc/7]). 26-export([get_safe_underapprox/2]). 27 28%%-import(helper, %% 'helper' could be any module doing sanity checks... 29-import(erl_types, 30 [t_has_var/1, t_inf/2, t_is_equal/2, t_is_subtype/2, 31 t_subtract/2, t_subtract_list/2, t_sup/1, t_sup/2,t_unify/2]). 32 33-import(erl_types, 34 [t_any/0, t_atom/0, t_atom_vals/1, 35 t_binary/0, t_bitstr/0, t_bitstr/2, t_bitstr_concat/1, t_boolean/0, 36 t_collect_vars/1, t_cons/2, t_cons_hd/1, t_cons_tl/1, 37 t_float/0, t_from_range/2, t_from_term/1, 38 t_fun/0, t_fun/2, t_fun_args/1, t_fun_range/1, 39 t_integer/0, 40 t_is_any/1, t_is_atom/1, t_is_any_atom/2, t_is_cons/1, 41 t_is_float/1, t_is_fun/1, 42 t_is_integer/1, t_non_neg_integer/0, 43 t_is_list/1, t_is_nil/1, t_is_none/1, t_is_number/1, 44 t_is_singleton/1, t_is_none_or_unit/1, 45 46 t_limit/2, t_list/0, t_list/1, 47 t_list_elements/1, t_nonempty_list/1, t_maybe_improper_list/0, 48 t_module/0, t_number/0, t_number_vals/1, 49 t_pid/0, t_port/0, t_product/1, t_reference/0, 50 t_subst/2, 51 t_timeout/0, t_tuple/0, t_tuple/1, 52 t_var/1, t_var_name/1, 53 t_none/0, t_unit/0, 54 t_map/0, t_map/1, t_map_get/2, t_map_put/2 55 ]). 56 57-include("dialyzer.hrl"). 58 59%%----------------------------------------------------------------------------- 60 61-type dep() :: integer(). %% type variable names used as constraint ids 62-type deps() :: ordsets:ordset(dep()). 63 64-type type_var() :: erl_types:erl_type(). %% actually: {'c','var',_,_} 65 66-record(fun_var, {'fun' :: fun((_) -> erl_types:erl_type()), deps :: deps(), 67 origin :: integer() | 'undefined'}). 68 69-type constr_op() :: 'eq' | 'sub'. 70-type fvar_or_type() :: #fun_var{} | erl_types:erl_type(). 71 72-record(constraint, {lhs :: erl_types:erl_type(), 73 op :: constr_op(), 74 rhs :: fvar_or_type(), 75 deps :: deps()}). 76 77-type constraint() :: #constraint{}. 78 79-type mask() :: ordsets:ordset(non_neg_integer()). 80 81-record(constraint_list, {type :: 'conj' | 'disj', 82 list :: [constr()], 83 deps :: deps(), 84 masks :: #{dep() => mask()} | 'undefined', 85 id :: {'list', dep()} | 'undefined'}). 86 87-type constraint_list() :: #constraint_list{}. 88 89-record(constraint_ref, {id :: type_var(), deps :: deps()}). 90 91-type constraint_ref() :: #constraint_ref{}. 92 93-type constr() :: constraint() | constraint_list() | constraint_ref(). 94 95-type types() :: erl_types:type_table(). 96 97-type typesig_funmap() :: #{type_var() => type_var()}. 98 99-type prop_types() :: orddict:orddict(label(), erl_types:erl_type()). 100-type dict_prop_types() :: dict:dict(label(), erl_types:erl_type()). 101 102-record(state, {callgraph :: dialyzer_callgraph:callgraph() 103 | 'undefined', 104 cserver :: dialyzer_codeserver:codeserver(), 105 cs = [] :: [constr()], 106 cmap = maps:new() :: #{type_var() => constr()}, 107 fun_map = maps:new() :: typesig_funmap(), 108 fun_arities = maps:new() :: #{type_var() => arity()}, 109 in_match = false :: boolean(), 110 in_guard = false :: boolean(), 111 module :: module(), 112 name_map = maps:new() :: #{mfa() => cerl:c_fun()}, 113 next_label = 0 :: label(), 114 self_rec :: 'false' | erl_types:erl_type(), 115 plt :: dialyzer_plt:plt() 116 | 'undefined', 117 prop_types = dict:new() :: dict_prop_types(), 118 mod_records = [] :: [{module(), types()}], 119 scc = [] :: ordsets:ordset(type_var()), 120 mfas :: [mfa()], 121 solvers = [] :: [solver()] 122 }). 123 124-type state() :: #state{}. 125 126%%----------------------------------------------------------------------------- 127 128-define(TYPE_LIMIT, 4). 129-define(INTERNAL_TYPE_LIMIT, 5). 130 131%%-define(DEBUG, true). 132%%-define(DEBUG_CONSTRAINTS, true). 133-ifdef(DEBUG). 134-define(DEBUG_NAME_MAP, true). 135-define(DEBUG_LOOP_DETECTION, true). 136-endif. 137%%-define(DEBUG_NAME_MAP, true). 138%%-define(DEBUG_LOOP_DETECTION, true). 139 140-ifdef(DEBUG). 141-define(debug(__String, __Args), io:format(__String, __Args)). 142-define(mk_fun_var(Fun, Vars), mk_fun_var(?LINE, Fun, Vars)). 143-define(pp_map(S, M), pp_map(S, M)). 144-else. 145-define(debug(__String, __Args), ok). 146-define(mk_fun_var(Fun, Vars), mk_fun_var(Fun, Vars)). 147-define(pp_map(S, M), ok). 148-endif. 149 150%% ============================================================================ 151%% 152%% The analysis. 153%% 154%% ============================================================================ 155 156%%----------------------------------------------------------------------------- 157%% Analysis of strongly connected components. 158%% 159%% analyze_scc(SCC, NextLabel, CallGraph, CodeServer, 160%% PLT, PropTypes, Solvers) -> FunTypes 161%% 162%% SCC - [{MFA}] 163%% NextLabel - An integer that is higher than any label in the code. 164%% CallGraph - A callgraph as produced by dialyzer_callgraph.erl 165%% Note: The callgraph must have been built with all the 166%% code that the SCC is a part of. 167%% PLT - A dialyzer PLT. This PLT should contain available information 168%% about functions that can be called by this SCC. 169%% PropTypes - A dictionary. 170%% FunTypes - A dictionary. 171%% Solvers - User specified solvers. 172%%----------------------------------------------------------------------------- 173 174-spec analyze_scc([mfa()], label(), 175 dialyzer_callgraph:callgraph(), 176 dialyzer_codeserver:codeserver(), 177 dialyzer_plt:plt(), prop_types(), [solver()]) -> prop_types(). 178 179analyze_scc(SCC, NextLabel, CallGraph, CServer, Plt, PropTypes, Solvers0) -> 180 Solvers = solvers(Solvers0), 181 State1 = new_state(SCC, NextLabel, CallGraph, CServer, Plt, PropTypes, 182 Solvers), 183 DefSet = add_def_list(maps:values(State1#state.name_map), sets:new()), 184 State2 = traverse_scc(SCC, CServer, DefSet, State1), 185 State3 = state__finalize(State2), 186 Funs = state__scc(State3), 187 pp_constrs_scc(Funs, State3), 188 constraints_to_dot_scc(Funs, State3), 189 T = solve(Funs, State3), 190 orddict:from_list(maps:to_list(T)). 191 192solvers([]) -> [v2]; 193solvers(Solvers) -> Solvers. 194 195%% ============================================================================ 196%% 197%% Gets the constraints by traversing the code. 198%% 199%% ============================================================================ 200 201traverse_scc([{M,_,_}=MFA|Left], Codeserver, DefSet, AccState) -> 202 TmpState1 = state__set_module(AccState, M), 203 Def = dialyzer_codeserver:lookup_mfa_code(MFA, Codeserver), 204 DummyLetrec = cerl:c_letrec([Def], cerl:c_atom(foo)), 205 TmpState2 = state__new_constraint_context(TmpState1), 206 {NewAccState, _} = traverse(DummyLetrec, DefSet, TmpState2), 207 traverse_scc(Left, Codeserver, DefSet, NewAccState); 208traverse_scc([], _Codeserver, _DefSet, AccState) -> 209 AccState. 210 211traverse(Tree, DefinedVars, State) -> 212 ?debug("Handling ~p\n", [cerl:type(Tree)]), 213 case cerl:type(Tree) of 214 alias -> 215 Var = cerl:alias_var(Tree), 216 Pat = cerl:alias_pat(Tree), 217 DefinedVars1 = add_def(Var, DefinedVars), 218 {State1, PatVar} = traverse(Pat, DefinedVars1, State), 219 State2 = state__store_conj(mk_var(Var), eq, PatVar, State1), 220 {State2, PatVar}; 221 apply -> 222 Args = cerl:apply_args(Tree), 223 Arity = length(Args), 224 Op = cerl:apply_op(Tree), 225 {State0, ArgTypes} = traverse_list(Args, DefinedVars, State), 226 {State1, OpType} = traverse(Op, DefinedVars, State0), 227 {State2, FunType} = state__get_fun_prototype(OpType, Arity, State1), 228 State3 = state__store_conj(FunType, eq, OpType, State2), 229 State4 = state__store_conj(mk_var(Tree), sub, t_fun_range(FunType), 230 State3), 231 State5 = state__store_conj_lists(ArgTypes, sub, t_fun_args(FunType), 232 State4), 233 case state__lookup_apply(Tree, State) of 234 unknown -> 235 {State5, mk_var(Tree)}; 236 FunLabels -> 237 case get_apply_constr(FunLabels, mk_var(Tree), ArgTypes, State5) of 238 error -> {State5, mk_var(Tree)}; 239 {ok, State6} -> {State6, mk_var(Tree)} 240 end 241 end; 242 binary -> 243 {State1, SegTypes} = traverse_list(cerl:binary_segments(Tree), 244 DefinedVars, State), 245 Type = ?mk_fun_var(fun(Map) -> 246 TmpSegTypes = lookup_type_list(SegTypes, Map), 247 t_bitstr_concat(TmpSegTypes) 248 end, SegTypes), 249 {state__store_conj(mk_var(Tree), sub, Type, State1), mk_var(Tree)}; 250 bitstr -> 251 Size = cerl:bitstr_size(Tree), 252 UnitVal = cerl:int_val(cerl:bitstr_unit(Tree)), 253 Val = cerl:bitstr_val(Tree), 254 {State1, [SizeType, ValType]} = 255 traverse_list([Size, Val], DefinedVars, State), 256 {State2, TypeConstr, BinValTypeConstr} = 257 case cerl:bitstr_bitsize(Tree) of 258 all -> 259 T = t_bitstr(UnitVal, 0), 260 {State1, T, T}; 261 utf -> 262 %% contains an integer number of bytes 263 T = t_binary(), 264 {State1, T, T}; 265 N when is_integer(N) -> 266 {State1, t_bitstr(0, N), t_bitstr(1, N)}; 267 any -> % Size is not a literal 268 T1 = ?mk_fun_var(bitstr_constr(SizeType, UnitVal), [SizeType]), 269 T2 = 270 ?mk_fun_var(bitstr_constr(SizeType, UnitVal, match), [SizeType]), 271 {state__store_conj(SizeType, sub, t_non_neg_integer(), State1), 272 T1, T2} 273 end, 274 ValTypeConstr = 275 case cerl:concrete(cerl:bitstr_type(Tree)) of 276 binary -> BinValTypeConstr; 277 float -> 278 case state__is_in_match(State1) of 279 true -> t_float(); 280 false -> t_number() 281 end; 282 integer -> 283 case state__is_in_match(State1) of 284 true -> 285 Flags = cerl:concrete(cerl:bitstr_flags(Tree)), 286 ?mk_fun_var(bitstr_val_constr(SizeType, UnitVal, Flags), 287 [SizeType]); 288 false -> t_integer() 289 end; 290 utf8 -> t_integer(); 291 utf16 -> t_integer(); 292 utf32 -> t_integer() 293 end, 294 State3 = state__store_conj(ValType, sub, ValTypeConstr, State2), 295 State4 = state__store_conj(mk_var(Tree), sub, TypeConstr, State3), 296 {State4, mk_var(Tree)}; 297 'case' -> 298 Arg = cerl:case_arg(Tree), 299 Clauses = cerl:case_clauses(Tree), 300 {State1, ArgVar} = traverse(Arg, DefinedVars, State), 301 handle_clauses(Clauses, mk_var(Tree), ArgVar, DefinedVars, State1); 302 call -> 303 handle_call(Tree, DefinedVars, State); 304 'catch' -> 305 %% XXX: Perhaps there is something to say about this. 306 {State, mk_var(Tree)}; 307 cons -> 308 Hd = cerl:cons_hd(Tree), 309 Tl = cerl:cons_tl(Tree), 310 {State1, [HdVar, TlVar]} = traverse_list([Hd, Tl], DefinedVars, State), 311 case cerl:is_literal(fold_literal_maybe_match(Tree, State)) of 312 true -> 313 %% We do not need to do anything more here. 314 {State, t_cons(HdVar, TlVar)}; 315 false -> 316 ConsVar = mk_var(Tree), 317 ConsType = ?mk_fun_var(fun(Map) -> 318 t_cons(lookup_type(HdVar, Map), 319 lookup_type(TlVar, Map)) 320 end, [HdVar, TlVar]), 321 HdType = ?mk_fun_var(fun(Map) -> 322 Cons = lookup_type(ConsVar, Map), 323 case t_is_cons(Cons) of 324 false -> t_any(); 325 true -> t_cons_hd(Cons) 326 end 327 end, [ConsVar]), 328 TlType = ?mk_fun_var(fun(Map) -> 329 Cons = lookup_type(ConsVar, Map), 330 case t_is_cons(Cons) of 331 false -> t_any(); 332 true -> t_cons_tl(Cons) 333 end 334 end, [ConsVar]), 335 State2 = state__store_conj_lists([HdVar, TlVar, ConsVar], sub, 336 [HdType, TlType, ConsType], 337 State1), 338 {State2, ConsVar} 339 end; 340 'fun' -> 341 Body = cerl:fun_body(Tree), 342 Vars = cerl:fun_vars(Tree), 343 DefinedVars1 = add_def_list(Vars, DefinedVars), 344 State0 = state__new_constraint_context(State), 345 FunFailType = 346 case state__prop_domain(cerl_trees:get_label(Tree), State0) of 347 error -> t_fun(length(Vars), t_none()); 348 {ok, Dom} -> t_fun(Dom, t_none()) 349 end, 350 TreeVar = mk_var(Tree), 351 State2 = 352 try 353 State1 = case state__add_prop_constrs(Tree, State0) of 354 not_called -> State0; 355 PropState -> PropState 356 end, 357 {BodyState, BodyVar} = traverse(Body, DefinedVars1, State1), 358 state__store_conj(TreeVar, eq, 359 t_fun(mk_var_list(Vars), BodyVar), BodyState) 360 catch 361 throw:error -> 362 state__store_conj(TreeVar, eq, FunFailType, State0) 363 end, 364 Cs = state__cs(State2), 365 State3 = state__store_constrs(TreeVar, Cs, State2), 366 Ref = mk_constraint_ref(TreeVar, get_deps(Cs)), 367 OldCs = state__cs(State), 368 State4 = state__new_constraint_context(State3), 369 State5 = state__store_conj_list([OldCs, Ref], State4), 370 State6 = state__store_fun_arity(Tree, State5), 371 State7 = state__add_fun_to_scc(TreeVar, State6), 372 {State7, TreeVar}; 373 'let' -> 374 Vars = cerl:let_vars(Tree), 375 Arg = cerl:let_arg(Tree), 376 Body = cerl:let_body(Tree), 377 {State1, ArgVars} = traverse(Arg, DefinedVars, State), 378 State2 = state__store_conj(t_product(mk_var_list(Vars)), eq, 379 ArgVars, State1), 380 DefinedVars1 = add_def_list(Vars, DefinedVars), 381 traverse(Body, DefinedVars1, State2); 382 letrec -> 383 Defs = cerl:letrec_defs(Tree), 384 Body = cerl:letrec_body(Tree), 385 Funs = [Fun || {_Var, Fun} <- Defs], 386 Vars = [Var || {Var, _Fun} <- Defs], 387 State1 = state__store_funs(Vars, Funs, State), 388 DefinedVars1 = add_def_list(Vars, DefinedVars), 389 {State2, _} = traverse_list(Funs, DefinedVars1, State1), 390 traverse(Body, DefinedVars1, State2); 391 literal -> 392 %% Maps are special; a literal pattern matches more than just the value 393 %% constructed by the literal. For example #{} constructs the empty map, 394 %% but matches every map. 395 case state__is_in_match(State) of 396 true -> 397 Tree1 = dialyzer_utils:refold_pattern(Tree), 398 case cerl:is_literal(Tree1) of 399 false -> traverse(Tree1, DefinedVars, State); 400 true -> {State, t_from_term(cerl:concrete(Tree))} 401 end; 402 _ -> {State, t_from_term(cerl:concrete(Tree))} 403 end; 404 module -> 405 Defs = cerl:module_defs(Tree), 406 Funs = [Fun || {_Var, Fun} <- Defs], 407 Vars = [Var || {Var, _Fun} <- Defs], 408 DefinedVars1 = add_def_list(Vars, DefinedVars), 409 State1 = state__store_funs(Vars, Funs, State), 410 FoldFun = fun(Fun, AccState) -> 411 {S, _} = traverse(Fun, DefinedVars1, 412 state__new_constraint_context(AccState)), 413 S 414 end, 415 lists:foldl(FoldFun, State1, Funs); 416 primop -> 417 case cerl:atom_val(cerl:primop_name(Tree)) of 418 match_fail -> throw(error); 419 raise -> throw(error); 420 bs_init_writable -> {State, t_from_term(<<>>)}; 421 build_stacktrace -> 422 V = mk_var(Tree), 423 Type = erl_bif_types:type(erlang, build_stacktrace, 0), 424 State1 = state__store_conj(V, sub, Type, State), 425 {State1, V}; 426 dialyzer_unknown -> 427 %% See dialyzer_clean_core:clean_letrec/1. 428 {State, mk_var(Tree)}; 429 recv_peek_message -> 430 {State1, Vars} = state__mk_vars(2, State), 431 {State1, t_product(Vars)}; 432 recv_wait_timeout -> 433 [Timeout] = cerl:primop_args(Tree), 434 case cerl:is_c_atom(Timeout) andalso 435 cerl:atom_val(Timeout) =:= infinity of 436 true -> 437 {State, t_none()}; 438 false -> 439 {State1, TimeoutVar} = traverse(Timeout, DefinedVars, State), 440 State2 = state__store_conj(TimeoutVar, sub, t_timeout(), State1), 441 {State2, mk_var(Tree)} 442 end; 443 remove_message -> 444 {State, t_any()}; 445 timeout -> 446 {State, t_any()}; 447 Other -> erlang:error({'Unsupported primop', Other}) 448 end; 449 'receive' -> 450 Clauses = cerl:receive_clauses(Tree), 451 Timeout = cerl:receive_timeout(Tree), 452 case (cerl:is_c_atom(Timeout) andalso 453 (cerl:atom_val(Timeout) =:= infinity)) of 454 true -> 455 handle_clauses(Clauses, mk_var(Tree), [], DefinedVars, State); 456 false -> 457 Action = cerl:receive_action(Tree), 458 {State1, TimeoutVar} = traverse(Timeout, DefinedVars, State), 459 State2 = state__store_conj(TimeoutVar, sub, t_timeout(), State1), 460 handle_clauses(Clauses, mk_var(Tree), [], Action, DefinedVars, State2) 461 end; 462 seq -> 463 Body = cerl:seq_body(Tree), 464 Arg = cerl:seq_arg(Tree), 465 {State1, _} = traverse(Arg, DefinedVars, State), 466 traverse(Body, DefinedVars, State1); 467 'try' -> 468 handle_try(Tree, DefinedVars, State); 469 tuple -> 470 Elements = cerl:tuple_es(Tree), 471 {State1, EVars} = traverse_list(Elements, DefinedVars, State), 472 {State2, TupleType} = 473 case cerl:is_literal(fold_literal_maybe_match(Tree, State1)) of 474 true -> 475 %% We do not need to do anything more here. 476 {State, t_tuple(EVars)}; 477 false -> 478 %% We have the same basic problem as in products, but we want to 479 %% make sure that everything that can be used as tags for the 480 %% disjoint unions stays in the tuple. 481 Fun = fun(Var, AccState) -> 482 case t_has_var(Var) of 483 true -> 484 {AccState1, NewVar} = state__mk_var(AccState), 485 {NewVar, 486 state__store_conj(Var, eq, NewVar, AccState1)}; 487 false -> 488 {Var, AccState} 489 end 490 end, 491 {NewEvars, TmpState} = lists:mapfoldl(Fun, State1, EVars), 492 {TmpState, t_tuple(NewEvars)} 493 end, 494 case Elements of 495 [Tag|Fields] -> 496 case cerl:is_c_atom(Tag) andalso is_literal_record(Tree) of 497 true -> 498 %% Check if a record is constructed. 499 Arity = length(Fields), 500 case lookup_record(State2, cerl:atom_val(Tag), Arity) of 501 {error, State3} -> {State3, TupleType}; 502 {ok, RecType, State3} -> 503 State4 = state__store_conj(TupleType, sub, RecType, State3), 504 {State4, TupleType} 505 end; 506 false -> {State2, TupleType} 507 end; 508 [] -> {State2, TupleType} 509 end; 510 map -> 511 Entries = cerl:map_es(Tree), 512 MapFoldFun = fun(Entry, AccState) -> 513 AccState1 = state__set_in_match(AccState, false), 514 {AccState2, KeyVar} = traverse(cerl:map_pair_key(Entry), 515 DefinedVars, AccState1), 516 AccState3 = state__set_in_match( 517 AccState2, state__is_in_match(AccState)), 518 {AccState4, ValVar} = traverse(cerl:map_pair_val(Entry), 519 DefinedVars, AccState3), 520 {{KeyVar, ValVar}, AccState4} 521 end, 522 {Pairs, State1} = lists:mapfoldl(MapFoldFun, State, Entries), 523 %% We mustn't recurse into map arguments to matches. Not only are they 524 %% syntactically only allowed to be the literal #{}, but that would also 525 %% cause an infinite recursion, since traverse/3 unfolds literals with 526 %% maps in them using dialyzer_utils:reflow_pattern/1. 527 {State2, ArgVar} = 528 case state__is_in_match(State) of 529 false -> traverse(cerl:map_arg(Tree), DefinedVars, State1); 530 true -> {State1, t_map()} 531 end, 532 MapVar = mk_var(Tree), 533 MapType = ?mk_fun_var( 534 fun(Map) -> 535 lists:foldl( 536 fun({K,V}, TypeAcc) -> 537 t_map_put({lookup_type(K, Map), 538 lookup_type(V, Map)}, 539 TypeAcc) 540 end, t_inf(t_map(), lookup_type(ArgVar, Map)), 541 Pairs) 542 end, [ArgVar | lists:append([[K,V] || {K,V} <- Pairs])]), 543 %% TODO: does the "same element appearing several times" problem apply 544 %% here too? 545 Fun = 546 fun({KeyVar, ValVar}, {AccState, ShadowKeys}) -> 547 %% If Val is known to be the last association of Key (i.e. Key 548 %% is not in ShadowKeys), Val must be a subtype of what is 549 %% associated to Key in Tree 550 TypeFun = 551 fun(Map) -> 552 KeyType = lookup_type(KeyVar, Map), 553 case t_is_singleton(KeyType) of 554 false -> t_any(); 555 true -> 556 MT = t_inf(lookup_type(MapVar, Map), t_map()), 557 case t_is_none_or_unit(MT) of 558 true -> t_none(); 559 false -> 560 DisjointFromKeyType = 561 fun(ShadowKey) -> 562 ST = t_inf(lookup_type(ShadowKey, Map), 563 KeyType), 564 t_is_none_or_unit(ST) 565 end, 566 case lists:all(DisjointFromKeyType, ShadowKeys) of 567 true -> t_map_get(KeyType, MT); 568 %% A later association might shadow this one 569 false -> t_any() 570 end 571 end 572 end 573 end, 574 ValType = ?mk_fun_var(TypeFun, [KeyVar, MapVar | ShadowKeys]), 575 {state__store_conj(ValVar, sub, ValType, AccState), 576 [KeyVar | ShadowKeys]} 577 end, 578 %% Accumulate shadowing keys right-to-left 579 {State3, _} = lists:foldr(Fun, {State2, []}, Pairs), 580 %% In a map expression, Arg must contain all keys that are inserted with 581 %% the exact (:=) operator, and are known (i.e. are not in ShadowedKeys) 582 %% to not have been introduced by a previous association 583 State4 = 584 case state__is_in_match(State) of 585 true -> State3; 586 false -> 587 ArgFun = 588 fun(Map) -> 589 FoldFun = 590 fun({{KeyVar, _}, Entry}, {AccType, ShadowedKeys}) -> 591 OpTree = cerl:map_pair_op(Entry), 592 KeyType = lookup_type(KeyVar, Map), 593 AccType1 = 594 case cerl:is_literal(OpTree) andalso 595 cerl:concrete(OpTree) =:= exact of 596 true -> 597 ST = t_inf(ShadowedKeys, KeyType), 598 case t_is_none_or_unit(ST) of 599 true -> 600 t_map_put({KeyType, t_any()}, AccType); 601 false -> 602 AccType 603 end; 604 false -> 605 AccType 606 end, 607 {AccType1, t_sup(KeyType, ShadowedKeys)} 608 end, 609 %% Accumulate shadowed keys left-to-right 610 {ResType, _} = lists:foldl(FoldFun, {t_map(), t_none()}, 611 lists:zip(Pairs, Entries)), 612 ResType 613 end, 614 ArgType = ?mk_fun_var(ArgFun, [KeyVar || {KeyVar, _} <- Pairs]), 615 state__store_conj(ArgVar, sub, ArgType, State3) 616 end, 617 {state__store_conj(MapVar, sub, MapType, State4), MapVar}; 618 values -> 619 %% We can get into trouble when unifying products that have the 620 %% same element appearing several times. Handle these cases by 621 %% introducing fresh variables and constraining them to be equal 622 %% to the original ones. This is similar to what happens in 623 %% pattern matching where the matching is done on fresh 624 %% variables and guards assert that the matching is correct. 625 Elements = cerl:values_es(Tree), 626 {State1, EVars} = traverse_list(Elements, DefinedVars, State), 627 Arity = length(EVars), 628 Unique = length(ordsets:from_list(EVars)), 629 case Arity =:= Unique of 630 true -> {State1, t_product(EVars)}; 631 false -> 632 {State2, Vars} = state__mk_vars(Arity, State1), 633 State3 = state__store_conj_lists(Vars, eq, EVars, State2), 634 {State3, t_product(Vars)} 635 end; 636 var -> 637 case is_def(Tree, DefinedVars) of 638 true -> {State, mk_var(Tree)}; 639 false -> 640 %% If we are analyzing SCCs this can be a function variable. 641 case state__lookup_undef_var(Tree, State) of 642 error -> erlang:error({'Undefined variable', Tree}); 643 {ok, Type} -> 644 {State1, NewVar} = state__mk_var(State), 645 {state__store_conj(NewVar, sub, Type, State1), NewVar} 646 end 647 end; 648 Other -> 649 erlang:error({'Unsupported type', Other}) 650 end. 651 652traverse_list(Trees, DefinedVars, State) -> 653 traverse_list(Trees, DefinedVars, State, []). 654 655traverse_list([Tree|Tail], DefinedVars, State, Acc) -> 656 {State1, Var} = traverse(Tree, DefinedVars, State), 657 traverse_list(Tail, DefinedVars, State1, [Var|Acc]); 658traverse_list([], _DefinedVars, State, Acc) -> 659 {State, lists:reverse(Acc)}. 660 661add_def(Var, Set) -> 662 sets:add_element(cerl_trees:get_label(Var), Set). 663 664add_def_list([H|T], Set) -> 665 add_def_list(T, add_def(H, Set)); 666add_def_list([], Set) -> 667 Set. 668 669add_def_from_tree(T, DefinedVars) -> 670 Vars = cerl_trees:fold(fun(X, Acc) -> 671 case cerl:is_c_var(X) of 672 true -> [X|Acc]; 673 false -> Acc 674 end 675 end, [], T), 676 add_def_list(Vars, DefinedVars). 677 678add_def_from_tree_list([H|T], DefinedVars) -> 679 add_def_from_tree_list(T, add_def_from_tree(H, DefinedVars)); 680add_def_from_tree_list([], DefinedVars) -> 681 DefinedVars. 682 683is_def(Var, Set) -> 684 sets:is_element(cerl_trees:get_label(Var), Set). 685 686%%---------------------------------------- 687%% Try 688%% 689 690handle_try(Tree, DefinedVars, State) -> 691 Arg = cerl:try_arg(Tree), 692 Vars = cerl:try_vars(Tree), 693 EVars = cerl:try_evars(Tree), 694 Body = cerl:try_body(Tree), 695 Handler = cerl:try_handler(Tree), 696 State1 = state__new_constraint_context(State), 697 {ArgBodyState, BodyVar} = 698 try 699 {State2, ArgVar} = traverse(Arg, DefinedVars, State1), 700 DefinedVars1 = add_def_list(Vars, DefinedVars), 701 {State3, BodyVar1} = traverse(Body, DefinedVars1, State2), 702 State4 = state__store_conj(t_product(mk_var_list(Vars)), eq, ArgVar, 703 State3), 704 {State4, BodyVar1} 705 catch 706 throw:error -> 707 {State1, t_none()} 708 end, 709 State6 = state__new_constraint_context(ArgBodyState), 710 {HandlerState, HandlerVar} = 711 try 712 DefinedVars2 = add_def_list([X || X <- EVars, cerl:is_c_var(X)], 713 DefinedVars), 714 traverse(Handler, DefinedVars2, State6) 715 catch 716 throw:error -> 717 {State6, t_none()} 718 end, 719 ArgBodyCs = state__cs(ArgBodyState), 720 HandlerCs = state__cs(HandlerState), 721 TreeVar = mk_var(Tree), 722 OldCs = state__cs(State), 723 case state__is_in_guard(State) of 724 true -> 725 Conj1 = mk_conj_constraint_list([ArgBodyCs, 726 mk_constraint(BodyVar, 727 eq, 728 TreeVar)]), 729 Disj = mk_disj_constraint_list([Conj1, 730 mk_constraint(HandlerVar, 731 eq, 732 TreeVar)]), 733 NewState1 = state__new_constraint_context(HandlerState), 734 Conj2 = mk_conj_constraint_list([OldCs, Disj]), 735 NewState2 = state__store_conj(Conj2, NewState1), 736 {NewState2, TreeVar}; 737 false -> 738 {NewCs, ReturnVar} = 739 case {t_is_none(BodyVar), t_is_none(HandlerVar)} of 740 {false, false} -> 741 Conj1 = 742 mk_conj_constraint_list([ArgBodyCs, 743 mk_constraint(TreeVar, 744 eq, 745 BodyVar)]), 746 Conj2 = 747 mk_conj_constraint_list([HandlerCs, 748 mk_constraint(TreeVar, 749 eq, 750 HandlerVar)]), 751 Disj = mk_disj_constraint_list([Conj1, Conj2]), 752 {Disj, TreeVar}; 753 {false, true} -> 754 {mk_conj_constraint_list([ArgBodyCs, 755 mk_constraint(TreeVar, 756 eq, 757 BodyVar)]), 758 BodyVar}; 759 {true, false} -> 760 {mk_conj_constraint_list([HandlerCs, 761 mk_constraint(TreeVar, 762 eq, 763 HandlerVar)]), 764 HandlerVar}; 765 {true, true} -> 766 ?debug("Throw failed\n", []), 767 throw(error) 768 end, 769 Conj = mk_conj_constraint_list([OldCs, NewCs]), 770 NewState1 = state__new_constraint_context(HandlerState), 771 NewState2 = state__store_conj(Conj, NewState1), 772 {NewState2, ReturnVar} 773 end. 774 775%%---------------------------------------- 776%% Call 777%% 778 779handle_call(Call, DefinedVars, State) -> 780 Args = cerl:call_args(Call), 781 Mod = cerl:call_module(Call), 782 Fun = cerl:call_name(Call), 783 Dst = mk_var(Call), 784 case cerl:is_c_atom(Mod) andalso cerl:is_c_atom(Fun) of 785 true -> 786 M = cerl:atom_val(Mod), 787 F = cerl:atom_val(Fun), 788 A = length(Args), 789 MFA = {M, F, A}, 790 {State1, ArgVars} = traverse_list(Args, DefinedVars, State), 791 case state__lookup_rec_var_in_scope(MFA, State) of 792 error -> 793 case get_bif_constr(MFA, Dst, ArgVars, State1) of 794 none -> 795 {get_plt_constr(MFA, Dst, ArgVars, State1), Dst}; 796 C -> 797 {state__store_conj(C, State1), Dst} 798 end; 799 {ok, Var} -> 800 %% This is part of the SCC currently analyzed. 801 %% Intercept and change this to an apply instead. 802 ?debug("Found the call to ~tw\n", [MFA]), 803 Label = cerl_trees:get_label(Call), 804 Apply = cerl:ann_c_apply([{label, Label}], Var, Args), 805 traverse(Apply, DefinedVars, State) 806 end; 807 false -> 808 {State1, MF} = traverse_list([Mod, Fun], DefinedVars, State), 809 {state__store_conj_lists(MF, sub, [t_module(), t_atom()], State1), Dst} 810 end. 811 812get_plt_constr(MFA, Dst, ArgVars, State) -> 813 Plt = state__plt(State), 814 PltRes = dialyzer_plt:lookup(Plt, MFA), 815 SCCMFAs = State#state.mfas, 816 Contract = 817 case lists:member(MFA, SCCMFAs) of 818 true -> none; 819 false -> dialyzer_plt:lookup_contract(Plt, MFA) 820 end, 821 case Contract of 822 none -> 823 case PltRes of 824 none -> State; 825 {value, {PltRetType, PltArgTypes}} -> 826 state__store_conj_lists([Dst|ArgVars], sub, 827 [PltRetType|PltArgTypes], State) 828 end; 829 {value, #contract{args = GenArgs} = C} -> 830 {RetType, ArgCs} = 831 case PltRes of 832 none -> 833 {?mk_fun_var(fun(Map) -> 834 ArgTypes = lookup_type_list(ArgVars, Map), 835 get_contract_return(C, ArgTypes) 836 end, ArgVars), GenArgs}; 837 {value, {PltRetType, PltArgTypes}} -> 838 %% Need to combine the contract with the success typing. 839 {?mk_fun_var( 840 fun(Map) -> 841 ArgTypes = lookup_type_list(ArgVars, Map), 842 CRet = get_contract_return(C, ArgTypes), 843 t_inf(CRet, PltRetType) 844 end, ArgVars), 845 [t_inf(X, Y) || {X, Y} <- lists:zip(GenArgs, PltArgTypes)]} 846 end, 847 state__store_conj_lists([Dst|ArgVars], sub, [RetType|ArgCs], State) 848 end. 849 850get_contract_return(C, ArgTypes) -> 851 dialyzer_contracts:get_contract_return(C, ArgTypes). 852 853%% If there is a significant number of clauses, we cannot apply the 854%% list subtraction scheme since it causes the analysis to be too 855%% slow. Typically, this only affects automatically generated files. 856%% The dataflow analysis doesn't suffer from this, so we will get some 857%% information anyway. 858-define(MAX_NOF_CLAUSES, 15). 859 860handle_clauses(Clauses, TopVar, Arg, DefinedVars, State) -> 861 handle_clauses(Clauses, TopVar, Arg, none, DefinedVars, State). 862 863handle_clauses([], _, _, Action, DefinedVars, State) when Action =/= none -> 864 %% Can happen when a receive has no clauses, see filter_match_fail. 865 traverse(Action, DefinedVars, State); 866handle_clauses(Clauses, TopVar, Arg, Action, DefinedVars, State) -> 867 SubtrTypeList = 868 if length(Clauses) > ?MAX_NOF_CLAUSES -> overflow; 869 true -> [] 870 end, 871 {State1, CList} = handle_clauses_1(Clauses, TopVar, Arg, DefinedVars, 872 State, SubtrTypeList, []), 873 {NewCs, NewState} = 874 case Action of 875 none -> 876 if CList =:= [] -> throw(error); 877 true -> {CList, State1} 878 end; 879 _ -> 880 try 881 {State2, ActionVar} = traverse(Action, DefinedVars, State1), 882 TmpC = mk_constraint(TopVar, eq, ActionVar), 883 ActionCs = mk_conj_constraint_list([state__cs(State2),TmpC]), 884 {[ActionCs|CList], State2} 885 catch 886 throw:error -> 887 if CList =:= [] -> throw(error); 888 true -> {CList, State1} 889 end 890 end 891 end, 892 OldCs = state__cs(State), 893 NewCList = mk_disj_constraint_list(NewCs), 894 FinalState = state__new_constraint_context(NewState), 895 {state__store_conj_list([OldCs, NewCList], FinalState), TopVar}. 896 897handle_clauses_1([Clause|Tail], TopVar, Arg, DefinedVars, 898 State, SubtrTypes, Acc) -> 899 State0 = state__new_constraint_context(State), 900 Pats = cerl:clause_pats(Clause), 901 Guard = cerl:clause_guard(Clause), 902 Body = cerl:clause_body(Clause), 903 NewSubtrTypes = 904 case SubtrTypes =:= overflow of 905 true -> overflow; 906 false -> 907 ordsets:add_element(get_safe_underapprox(Pats, Guard), SubtrTypes) 908 end, 909 try 910 DefinedVars1 = add_def_from_tree_list(Pats, DefinedVars), 911 State1 = state__set_in_match(State0, true), 912 {State2, PatVars} = traverse_list(Pats, DefinedVars1, State1), 913 State3 = 914 case Arg =:= [] of 915 true -> State2; 916 false -> 917 S = state__store_conj(Arg, eq, t_product(PatVars), State2), 918 case SubtrTypes =:= overflow of 919 true -> S; 920 false -> 921 SubtrPatVar = ?mk_fun_var(fun(Map) -> 922 TmpType = lookup_type(Arg, Map), 923 t_subtract_list(TmpType, SubtrTypes) 924 end, [Arg]), 925 state__store_conj(Arg, sub, SubtrPatVar, S) 926 end 927 end, 928 State4 = handle_guard(Guard, DefinedVars1, State3), 929 {State5, BodyVar} = traverse(Body, DefinedVars1, 930 state__set_in_match(State4, false)), 931 State6 = state__store_conj(TopVar, eq, BodyVar, State5), 932 Cs = state__cs(State6), 933 handle_clauses_1(Tail, TopVar, Arg, DefinedVars, State6, 934 NewSubtrTypes, [Cs|Acc]) 935 catch 936 throw:error -> 937 handle_clauses_1(Tail, TopVar, Arg, DefinedVars, 938 State, NewSubtrTypes, Acc) 939 end; 940handle_clauses_1([], _TopVar, _Arg, _DefinedVars, State, _SubtrType, Acc) -> 941 {state__new_constraint_context(State), Acc}. 942 943-spec get_safe_underapprox([cerl:c_values()], cerl:cerl()) -> erl_types:erl_type(). 944 945get_safe_underapprox(Pats, Guard) -> 946 try 947 Map1 = cerl_trees:fold(fun(X, Acc) -> 948 case cerl:is_c_var(X) of 949 true -> 950 maps:put(cerl_trees:get_label(X), t_any(), 951 Acc); 952 false -> Acc 953 end 954 end, maps:new(), cerl:c_values(Pats)), 955 {Type, Map2} = get_underapprox_from_guard(Guard, Map1), 956 Map3 = case t_is_none(t_inf(t_from_term(true), Type)) of 957 true -> throw(dont_know); 958 false -> 959 case cerl:is_c_var(Guard) of 960 false -> Map2; 961 true -> 962 maps:put(cerl_trees:get_label(Guard), 963 t_from_term(true), Map2) 964 end 965 end, 966 {Ts, _Map4} = get_safe_underapprox_1(Pats, [], Map3), 967 t_product(Ts) 968 catch 969 throw:dont_know -> t_none() 970 end. 971 972get_underapprox_from_guard(Tree, Map) -> 973 True = t_from_term(true), 974 case cerl:type(Tree) of 975 call -> 976 case {cerl:concrete(cerl:call_module(Tree)), 977 cerl:concrete(cerl:call_name(Tree)), 978 length(cerl:call_args(Tree))} of 979 {erlang, is_function, 2} -> 980 [Fun, Arity] = cerl:call_args(Tree), 981 case cerl:is_c_int(Arity) of 982 false -> throw(dont_know); 983 true -> 984 {FunType, Map1} = get_underapprox_from_guard(Fun, Map), 985 Inf = t_inf(FunType, t_fun(cerl:int_val(Arity), t_any())), 986 case t_is_none(Inf) of 987 true -> throw(dont_know); 988 false -> 989 {True, maps:put(cerl_trees:get_label(Fun), Inf, Map1)} 990 end 991 end; 992 MFA -> 993 case get_type_test(MFA) of 994 {ok, Type} -> 995 [Arg0] = cerl:call_args(Tree), 996 Arg = cerl:fold_literal(Arg0), 997 {ArgType, Map1} = get_underapprox_from_guard(Arg, Map), 998 Inf = t_inf(Type, ArgType), 999 case t_is_none(Inf) of 1000 true -> throw(dont_know); 1001 false -> 1002 case cerl:is_literal(Arg) of 1003 true -> {True, Map1}; 1004 false -> 1005 {True, maps:put(cerl_trees:get_label(Arg), Inf, Map1)} 1006 end 1007 end; 1008 error -> 1009 case MFA of 1010 {erlang, '=:=', 2} -> throw(dont_know); 1011 {erlang, '==', 2} -> throw(dont_know); 1012 {erlang, 'and', 2} -> 1013 [Arg1_0, Arg2_0] = cerl:call_args(Tree), 1014 Arg1 = cerl:fold_literal(Arg1_0), 1015 Arg2 = cerl:fold_literal(Arg2_0), 1016 case ((cerl:is_c_var(Arg1) orelse cerl:is_literal(Arg1)) 1017 andalso 1018 (cerl:is_c_var(Arg2) orelse cerl:is_literal(Arg2))) of 1019 true -> 1020 {Arg1Type, _} = get_underapprox_from_guard(Arg1, Map), 1021 {Arg2Type, _} = get_underapprox_from_guard(Arg2, Map), 1022 case (t_is_equal(True, Arg1Type) andalso 1023 t_is_equal(True, Arg2Type)) of 1024 true -> {True, Map}; 1025 false -> throw(dont_know) 1026 end; 1027 false -> 1028 throw(dont_know) 1029 end; 1030 {erlang, 'or', 2} -> throw(dont_know); 1031 _ -> throw(dont_know) 1032 end 1033 end 1034 end; 1035 var -> 1036 Type = 1037 case maps:find(cerl_trees:get_label(Tree), Map) of 1038 error -> throw(dont_know); 1039 {ok, T} -> T 1040 end, 1041 {Type, Map}; 1042 literal -> 1043 case cerl:unfold_literal(Tree) of 1044 Tree -> 1045 Type = 1046 case cerl:concrete(Tree) of 1047 Int when is_integer(Int) -> t_from_term(Int); 1048 Atom when is_atom(Atom) -> t_from_term(Atom); 1049 _Other -> throw(dont_know) 1050 end, 1051 {Type, Map}; 1052 OtherTree -> 1053 get_underapprox_from_guard(OtherTree, Map) 1054 end; 1055 _ -> 1056 throw(dont_know) 1057 end. 1058 1059%% 1060%% The guard test {erlang, is_function, 2} is handled specially by the 1061%% function get_underapprox_from_guard/2 1062%% 1063get_type_test({erlang, is_atom, 1}) -> {ok, t_atom()}; 1064get_type_test({erlang, is_boolean, 1}) -> {ok, t_boolean()}; 1065get_type_test({erlang, is_binary, 1}) -> {ok, t_binary()}; 1066get_type_test({erlang, is_bitstring, 1}) -> {ok, t_bitstr()}; 1067get_type_test({erlang, is_float, 1}) -> {ok, t_float()}; 1068get_type_test({erlang, is_function, 1}) -> {ok, t_fun()}; 1069get_type_test({erlang, is_integer, 1}) -> {ok, t_integer()}; 1070get_type_test({erlang, is_list, 1}) -> {ok, t_list()}; 1071get_type_test({erlang, is_map, 1}) -> {ok, t_map()}; 1072get_type_test({erlang, is_number, 1}) -> {ok, t_number()}; 1073get_type_test({erlang, is_pid, 1}) -> {ok, t_pid()}; 1074get_type_test({erlang, is_port, 1}) -> {ok, t_port()}; 1075%% get_type_test({erlang, is_record, 2}) -> {ok, t_tuple()}; 1076%% get_type_test({erlang, is_record, 3}) -> {ok, t_tuple()}; 1077get_type_test({erlang, is_reference, 1}) -> {ok, t_reference()}; 1078get_type_test({erlang, is_tuple, 1}) -> {ok, t_tuple()}; 1079get_type_test({M, F, A}) when is_atom(M), is_atom(F), is_integer(A) -> error. 1080 1081bitstr_constr(SizeType, UnitVal) -> 1082 bitstr_constr(SizeType, UnitVal, construct). 1083 1084bitstr_constr(SizeType, UnitVal, ConstructOrMatch) -> 1085 Unit = 1086 case ConstructOrMatch of 1087 construct -> 0; 1088 match -> 1 1089 end, 1090 fun(Map) -> 1091 TmpSizeType = lookup_type(SizeType, Map), 1092 case t_is_subtype(TmpSizeType, t_non_neg_integer()) of 1093 true -> 1094 case t_number_vals(TmpSizeType) of 1095 [OneSize] -> t_bitstr(Unit, OneSize * UnitVal); 1096 _ -> 1097 MinSize = erl_types:number_min(TmpSizeType), 1098 t_bitstr(UnitVal, MinSize * UnitVal) 1099 end; 1100 false -> 1101 t_bitstr(UnitVal, 0) 1102 end 1103 end. 1104 1105bitstr_val_constr(SizeType, UnitVal, Flags) -> 1106 fun(Map) -> 1107 TmpSizeType = lookup_type(SizeType, Map), 1108 case t_is_subtype(TmpSizeType, t_non_neg_integer()) of 1109 true -> 1110 case erl_types:number_max(TmpSizeType) of 1111 N when is_integer(N), N < 128 -> %% Avoid illegal arithmetic 1112 TotalSizeVal = N * UnitVal, 1113 {RangeMin, RangeMax} = 1114 case lists:member(signed, Flags) of 1115 true -> {-(1 bsl (TotalSizeVal - 1)), 1116 1 bsl (TotalSizeVal - 1) - 1}; 1117 false -> {0, 1 bsl TotalSizeVal - 1} 1118 end, 1119 t_from_range(RangeMin, RangeMax); 1120 _ -> 1121 t_integer() 1122 end; 1123 false -> 1124 t_integer() 1125 end 1126 end. 1127 1128get_safe_underapprox_1([Pat0|Left], Acc, Map) -> 1129 %% Maps should be treated as patterns, not as literals 1130 Pat = dialyzer_utils:refold_pattern(Pat0), 1131 case cerl:type(Pat) of 1132 alias -> 1133 APat = cerl:alias_pat(Pat), 1134 AVar = cerl:alias_var(Pat), 1135 {[VarType], Map1} = get_safe_underapprox_1([AVar], [], Map), 1136 {[PatType], Map2} = get_safe_underapprox_1([APat], [], Map1), 1137 Inf = t_inf(VarType, PatType), 1138 case t_is_none(Inf) of 1139 true -> throw(dont_know); 1140 false -> 1141 Map3 = maps:put(cerl_trees:get_label(AVar), Inf, Map2), 1142 get_safe_underapprox_1(Left, [Inf|Acc], Map3) 1143 end; 1144 binary -> 1145 %% TODO: Can maybe do something here 1146 throw(dont_know); 1147 cons -> 1148 {[Hd, Tl], Map1} = 1149 get_safe_underapprox_1([cerl:cons_hd(Pat), cerl:cons_tl(Pat)], [], Map), 1150 case t_is_any(Tl) of 1151 true -> get_safe_underapprox_1(Left, [t_nonempty_list(Hd)|Acc], Map1); 1152 false -> throw(dont_know) 1153 end; 1154 literal -> 1155 case cerl:unfold_literal(Pat) of 1156 Pat -> 1157 Type = 1158 case cerl:concrete(Pat) of 1159 Int when is_integer(Int) -> t_from_term(Int); 1160 Atom when is_atom(Atom) -> t_from_term(Atom); 1161 [] -> t_from_term([]); 1162 _Other -> throw(dont_know) 1163 end, 1164 get_safe_underapprox_1(Left, [Type|Acc], Map); 1165 OtherPat -> 1166 get_safe_underapprox_1([OtherPat|Left], Acc, Map) 1167 end; 1168 tuple -> 1169 Es = cerl:tuple_es(Pat), 1170 {Ts, Map1} = get_safe_underapprox_1(Es, [], Map), 1171 Type = t_tuple(Ts), 1172 get_safe_underapprox_1(Left, [Type|Acc], Map1); 1173 map -> 1174 %% Some assertions in case the syntax gets more premissive in the future 1175 true = #{} =:= cerl:concrete(cerl:map_arg(Pat)), 1176 true = lists:all(fun(P) -> 1177 cerl:is_literal(Op = cerl:map_pair_op(P)) andalso 1178 exact =:= cerl:concrete(Op) 1179 end, cerl:map_es(Pat)), 1180 KeyTrees = lists:map(fun cerl:map_pair_key/1, cerl:map_es(Pat)), 1181 ValTrees = lists:map(fun cerl:map_pair_val/1, cerl:map_es(Pat)), 1182 %% Keys must not be underapproximated. Overapproximations are safe. 1183 Keys = get_safe_overapprox(KeyTrees), 1184 {Vals, Map1} = get_safe_underapprox_1(ValTrees, [], Map), 1185 case lists:all(fun erl_types:t_is_singleton/1, Keys) of 1186 false -> throw(dont_know); 1187 true -> ok 1188 end, 1189 SortedPairs = lists:sort(lists:zip(Keys, Vals)), 1190 %% We need to deal with duplicates ourselves 1191 SquashDuplicates = 1192 fun SquashDuplicates([{K,First},{K,Second}|List]) -> 1193 case t_is_none(Inf = t_inf(First, Second)) of 1194 true -> throw(dont_know); 1195 false -> [{K, Inf}|SquashDuplicates(List)] 1196 end; 1197 SquashDuplicates([Good|Rest]) -> 1198 [Good|SquashDuplicates(Rest)]; 1199 SquashDuplicates([]) -> [] 1200 end, 1201 Type = t_map(SquashDuplicates(SortedPairs)), 1202 get_safe_underapprox_1(Left, [Type|Acc], Map1); 1203 values -> 1204 Es = cerl:values_es(Pat), 1205 {Ts, Map1} = get_safe_underapprox_1(Es, [], Map), 1206 Type = t_product(Ts), 1207 get_safe_underapprox_1(Left, [Type|Acc], Map1); 1208 var -> 1209 case maps:find(cerl_trees:get_label(Pat), Map) of 1210 error -> throw(dont_know); 1211 {ok, VarType} -> get_safe_underapprox_1(Left, [VarType|Acc], Map) 1212 end 1213 end; 1214get_safe_underapprox_1([], Acc, Map) -> 1215 {lists:reverse(Acc), Map}. 1216 1217get_safe_overapprox(Pats) -> 1218 lists:map(fun get_safe_overapprox_1/1, Pats). 1219 1220get_safe_overapprox_1(Pat) -> 1221 case cerl:is_literal(Lit = cerl:fold_literal(Pat)) of 1222 true -> t_from_term(cerl:concrete(Lit)); 1223 false -> t_any() 1224 end. 1225 1226%%---------------------------------------- 1227%% Guards 1228%% 1229 1230handle_guard(Guard, DefinedVars, State) -> 1231 True = t_from_term(true), 1232 State1 = state__set_in_guard(State, true), 1233 State2 = state__new_constraint_context(State1), 1234 {State3, Return} = traverse(Guard, DefinedVars, State2), 1235 State4 = state__store_conj(Return, eq, True, State3), 1236 Cs = state__cs(State4), 1237 NewCs = mk_disj_norm_form(Cs), 1238 OldCs = state__cs(State), 1239 State5 = state__set_in_guard(State4, state__is_in_guard(State)), 1240 State6 = state__new_constraint_context(State5), 1241 state__store_conj(mk_conj_constraint_list([OldCs, NewCs]), State6). 1242 1243%%============================================================================= 1244%% 1245%% BIF constraints 1246%% 1247%%============================================================================= 1248 1249get_bif_constr({erlang, Op, 2}, Dst, Args = [Arg1, Arg2], _State) 1250 when Op =:= '+'; Op =:= '-'; Op =:= '*' -> 1251 ReturnType = ?mk_fun_var(fun(Map) -> 1252 TmpArgTypes = lookup_type_list(Args, Map), 1253 bif_return(erlang, Op, 2, TmpArgTypes) 1254 end, Args), 1255 ArgFun = 1256 fun(A, Pos) -> 1257 F = 1258 fun(Map) -> 1259 DstType = lookup_type(Dst, Map), 1260 AType = lookup_type(A, Map), 1261 case t_is_integer(DstType) of 1262 true -> 1263 case t_is_integer(AType) of 1264 true -> 1265 eval_inv_arith(Op, Pos, DstType, AType); 1266 false -> 1267 %% This must be temporary. 1268 t_integer() 1269 end; 1270 false -> 1271 case t_is_float(DstType) of 1272 true -> 1273 case t_is_integer(AType) of 1274 true -> t_float(); 1275 false -> t_number() 1276 end; 1277 false -> 1278 t_number() 1279 end 1280 end 1281 end, 1282 ?mk_fun_var(F, [Dst, A]) 1283 end, 1284 Arg1FunVar = ArgFun(Arg2, 2), 1285 Arg2FunVar = ArgFun(Arg1, 1), 1286 mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType), 1287 mk_constraint(Arg1, sub, Arg1FunVar), 1288 mk_constraint(Arg2, sub, Arg2FunVar)]); 1289get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State) 1290 when Op =:= '<'; Op =:= '=<'; Op =:= '>'; Op =:= '>=' -> 1291 ArgFun = 1292 fun(LocalArg1, LocalArg2, LocalOp) -> 1293 fun(Map) -> 1294 DstType = lookup_type(Dst, Map), 1295 IsTrue = t_is_any_atom(true, DstType), 1296 IsFalse = t_is_any_atom(false, DstType), 1297 case IsTrue orelse IsFalse of 1298 true -> 1299 Arg1Type = lookup_type(LocalArg1, Map), 1300 Arg2Type = lookup_type(LocalArg2, Map), 1301 case t_is_integer(Arg1Type) andalso t_is_integer(Arg2Type) of 1302 true -> 1303 Max1 = erl_types:number_max(Arg1Type), 1304 Min1 = erl_types:number_min(Arg1Type), 1305 Max2 = erl_types:number_max(Arg2Type), 1306 Min2 = erl_types:number_min(Arg2Type), 1307 case LocalOp of 1308 '=<' -> 1309 if IsTrue -> t_from_range(Min1, Max2); 1310 IsFalse -> t_from_range(range_inc(Min2), Max1) 1311 end; 1312 '<' -> 1313 if IsTrue -> t_from_range(Min1, range_dec(Max2)); 1314 IsFalse -> t_from_range(Min2, Max1) 1315 end; 1316 '>=' -> 1317 if IsTrue -> t_from_range(Min2, Max1); 1318 IsFalse -> t_from_range(Min1, range_dec(Max2)) 1319 end; 1320 '>' -> 1321 if IsTrue -> t_from_range(range_inc(Min2), Max1); 1322 IsFalse -> t_from_range(Min1, Max2) 1323 end 1324 end; 1325 false -> t_any() 1326 end; 1327 false -> t_any() 1328 end 1329 end 1330 end, 1331 {Arg1Fun, Arg2Fun} = 1332 case Op of 1333 '<' -> {ArgFun(Arg1, Arg2, '<'), ArgFun(Arg2, Arg1, '>=')}; 1334 '=<' -> {ArgFun(Arg1, Arg2, '=<'), ArgFun(Arg2, Arg1, '>=')}; 1335 '>' -> {ArgFun(Arg1, Arg2, '>'), ArgFun(Arg2, Arg1, '<')}; 1336 '>=' -> {ArgFun(Arg1, Arg2, '>='), ArgFun(Arg2, Arg1, '=<')} 1337 end, 1338 DstArgs = [Dst, Arg1, Arg2], 1339 Arg1Var = ?mk_fun_var(Arg1Fun, DstArgs), 1340 Arg2Var = ?mk_fun_var(Arg2Fun, DstArgs), 1341 DstVar = ?mk_fun_var(fun(Map) -> 1342 TmpArgTypes = lookup_type_list(Args, Map), 1343 bif_return(erlang, Op, 2, TmpArgTypes) 1344 end, Args), 1345 mk_conj_constraint_list([mk_constraint(Dst, sub, DstVar), 1346 mk_constraint(Arg1, sub, Arg1Var), 1347 mk_constraint(Arg2, sub, Arg2Var)]); 1348get_bif_constr({erlang, '++', 2}, Dst, [Hd, Tl] = Args, _State) -> 1349 HdFun = fun(Map) -> 1350 DstType = lookup_type(Dst, Map), 1351 case t_is_cons(DstType) of 1352 true -> t_list(t_cons_hd(DstType)); 1353 false -> 1354 case t_is_list(DstType) of 1355 true -> 1356 case t_is_nil(DstType) of 1357 true -> DstType; 1358 false -> t_list(t_list_elements(DstType)) 1359 end; 1360 false -> t_list() 1361 end 1362 end 1363 end, 1364 TlFun = fun(Map) -> 1365 DstType = lookup_type(Dst, Map), 1366 case t_is_cons(DstType) of 1367 true -> t_sup(t_cons_tl(DstType), DstType); 1368 false -> 1369 case t_is_list(DstType) of 1370 true -> 1371 case t_is_nil(DstType) of 1372 true -> DstType; 1373 false -> t_list(t_list_elements(DstType)) 1374 end; 1375 false -> t_any() 1376 end 1377 end 1378 end, 1379 DstL = [Dst], 1380 HdVar = ?mk_fun_var(HdFun, DstL), 1381 TlVar = ?mk_fun_var(TlFun, DstL), 1382 ArgTypes = erl_bif_types:arg_types(erlang, '++', 2), 1383 ReturnType = ?mk_fun_var(fun(Map) -> 1384 TmpArgTypes = lookup_type_list(Args, Map), 1385 bif_return(erlang, '++', 2, TmpArgTypes) 1386 end, Args), 1387 Cs = mk_constraints(Args, sub, ArgTypes), 1388 mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType), 1389 mk_constraint(Hd, sub, HdVar), 1390 mk_constraint(Tl, sub, TlVar) 1391 |Cs]); 1392get_bif_constr({erlang, is_atom, 1}, Dst, [Arg], State) -> 1393 get_bif_test_constr(Dst, Arg, t_atom(), State); 1394get_bif_constr({erlang, is_binary, 1}, Dst, [Arg], State) -> 1395 get_bif_test_constr(Dst, Arg, t_binary(), State); 1396get_bif_constr({erlang, is_bitstring, 1}, Dst, [Arg], State) -> 1397 get_bif_test_constr(Dst, Arg, t_bitstr(), State); 1398get_bif_constr({erlang, is_boolean, 1}, Dst, [Arg], State) -> 1399 get_bif_test_constr(Dst, Arg, t_boolean(), State); 1400get_bif_constr({erlang, is_float, 1}, Dst, [Arg], State) -> 1401 get_bif_test_constr(Dst, Arg, t_float(), State); 1402get_bif_constr({erlang, is_function, 1}, Dst, [Arg], State) -> 1403 get_bif_test_constr(Dst, Arg, t_fun(), State); 1404get_bif_constr({erlang, is_function, 2}, Dst, [Fun, Arity], _State) -> 1405 ArgFun = fun(Map) -> 1406 DstType = lookup_type(Dst, Map), 1407 case t_is_any_atom(true, DstType) of 1408 true -> 1409 ArityType = lookup_type(Arity, Map), 1410 case t_number_vals(ArityType) of 1411 unknown -> t_fun(); 1412 Vals -> t_sup([t_fun(X, t_any()) || X <- Vals]) 1413 end; 1414 false -> t_any() 1415 end 1416 end, 1417 ArgV = ?mk_fun_var(ArgFun, [Dst, Arity]), 1418 mk_conj_constraint_list([mk_constraint(Dst, sub, t_boolean()), 1419 mk_constraint(Arity, sub, t_integer()), 1420 mk_constraint(Fun, sub, ArgV)]); 1421get_bif_constr({erlang, is_integer, 1}, Dst, [Arg], State) -> 1422 get_bif_test_constr(Dst, Arg, t_integer(), State); 1423get_bif_constr({erlang, is_list, 1}, Dst, [Arg], State) -> 1424 get_bif_test_constr(Dst, Arg, t_maybe_improper_list(), State); 1425get_bif_constr({erlang, is_map, 1}, Dst, [Arg], State) -> 1426 get_bif_test_constr(Dst, Arg, t_map(), State); 1427get_bif_constr({erlang, is_number, 1}, Dst, [Arg], State) -> 1428 get_bif_test_constr(Dst, Arg, t_number(), State); 1429get_bif_constr({erlang, is_pid, 1}, Dst, [Arg], State) -> 1430 get_bif_test_constr(Dst, Arg, t_pid(), State); 1431get_bif_constr({erlang, is_port, 1}, Dst, [Arg], State) -> 1432 get_bif_test_constr(Dst, Arg, t_port(), State); 1433get_bif_constr({erlang, is_reference, 1}, Dst, [Arg], State) -> 1434 get_bif_test_constr(Dst, Arg, t_reference(), State); 1435get_bif_constr({erlang, is_record, 2}, Dst, [Var, Tag] = Args, _State) -> 1436 ArgFun = fun(Map) -> 1437 case t_is_any_atom(true, lookup_type(Dst, Map)) of 1438 true -> t_tuple(); 1439 false -> t_any() 1440 end 1441 end, 1442 ArgV = ?mk_fun_var(ArgFun, [Dst]), 1443 DstFun = fun(Map) -> 1444 TmpArgTypes = lookup_type_list(Args, Map), 1445 bif_return(erlang, is_record, 2, TmpArgTypes) 1446 end, 1447 DstV = ?mk_fun_var(DstFun, Args), 1448 mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), 1449 mk_constraint(Tag, sub, t_atom()), 1450 mk_constraint(Var, sub, ArgV)]); 1451get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) -> 1452 %% TODO: Revise this to make it precise for Tag and Arity. 1453 ArgFun = 1454 fun(Map) -> 1455 case t_is_any_atom(true, lookup_type(Dst, Map)) of 1456 true -> 1457 ArityType = lookup_type(Arity, Map), 1458 case t_is_integer(ArityType) of 1459 true -> 1460 case t_number_vals(ArityType) of 1461 [ArityVal] -> 1462 TagType = lookup_type(Tag, Map), 1463 case t_is_atom(TagType) of 1464 true -> 1465 AnyElems = lists:duplicate(ArityVal-1, t_any()), 1466 GenRecord = t_tuple([TagType|AnyElems]), 1467 case t_atom_vals(TagType) of 1468 [TagVal] -> 1469 case lookup_record(State, TagVal, ArityVal - 1) of 1470 {ok, Type, _NewState} -> 1471 Type; 1472 {error, _NewState} -> GenRecord 1473 end; 1474 _ -> GenRecord 1475 end; 1476 false -> t_tuple(ArityVal) 1477 end; 1478 _ -> t_tuple() 1479 end; 1480 false -> t_tuple() 1481 end; 1482 false -> t_any() 1483 end 1484 end, 1485 ArgV = ?mk_fun_var(ArgFun, [Tag, Arity, Dst]), 1486 DstFun = fun(Map) -> 1487 [TmpVar, TmpTag, TmpArity] = lookup_type_list(Args, Map), 1488 TmpArgTypes = [TmpVar,TmpTag,TmpArity], 1489 bif_return(erlang, is_record, 3, TmpArgTypes) 1490 end, 1491 DstV = ?mk_fun_var(DstFun, Args), 1492 mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), 1493 mk_constraint(Arity, sub, t_integer()), 1494 mk_constraint(Tag, sub, t_atom()), 1495 mk_constraint(Var, sub, ArgV)]); 1496get_bif_constr({erlang, is_tuple, 1}, Dst, [Arg], State) -> 1497 get_bif_test_constr(Dst, Arg, t_tuple(), State); 1498get_bif_constr({erlang, 'and', 2}, Dst, [Arg1, Arg2] = Args, _State) -> 1499 True = t_from_term(true), 1500 False = t_from_term(false), 1501 ArgFun = fun(Var) -> 1502 fun(Map) -> 1503 DstType = lookup_type(Dst, Map), 1504 case t_is_any_atom(true, DstType) of 1505 true -> True; 1506 false -> 1507 case t_is_any_atom(false, DstType) of 1508 true -> 1509 case 1510 t_is_any_atom(true, lookup_type(Var, Map)) 1511 of 1512 true -> False; 1513 false -> t_boolean() 1514 end; 1515 false -> 1516 t_boolean() 1517 end 1518 end 1519 end 1520 end, 1521 DstFun = fun(Map) -> 1522 Arg1Type = lookup_type(Arg1, Map), 1523 case t_is_any_atom(false, Arg1Type) of 1524 true -> False; 1525 false -> 1526 Arg2Type = lookup_type(Arg2, Map), 1527 case t_is_any_atom(false, Arg2Type) of 1528 true -> False; 1529 false -> 1530 case (t_is_any_atom(true, Arg1Type) 1531 andalso t_is_any_atom(true, Arg2Type)) of 1532 true -> True; 1533 false -> t_boolean() 1534 end 1535 end 1536 end 1537 end, 1538 ArgV1 = ?mk_fun_var(ArgFun(Arg2), [Arg2, Dst]), 1539 ArgV2 = ?mk_fun_var(ArgFun(Arg1), [Arg1, Dst]), 1540 DstV = ?mk_fun_var(DstFun, Args), 1541 mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), 1542 mk_constraint(Arg1, sub, ArgV1), 1543 mk_constraint(Arg2, sub, ArgV2)]); 1544get_bif_constr({erlang, 'or', 2}, Dst, [Arg1, Arg2] = Args, _State) -> 1545 True = t_from_term(true), 1546 False = t_from_term(false), 1547 ArgFun = fun(Var) -> 1548 fun(Map) -> 1549 DstType = lookup_type(Dst, Map), 1550 case t_is_any_atom(false, DstType) of 1551 true -> False; 1552 false -> 1553 case t_is_any_atom(true, DstType) of 1554 true -> 1555 case 1556 t_is_any_atom(false, lookup_type(Var, Map)) 1557 of 1558 true -> True; 1559 false -> t_boolean() 1560 end; 1561 false -> 1562 t_boolean() 1563 end 1564 end 1565 end 1566 end, 1567 DstFun = fun(Map) -> 1568 Arg1Type = lookup_type(Arg1, Map), 1569 case t_is_any_atom(true, Arg1Type) of 1570 true -> True; 1571 false -> 1572 Arg2Type = lookup_type(Arg2, Map), 1573 case t_is_any_atom(true, Arg2Type) of 1574 true -> True; 1575 false -> 1576 case (t_is_any_atom(false, Arg1Type) 1577 andalso t_is_any_atom(false, Arg2Type)) of 1578 true -> False; 1579 false -> t_boolean() 1580 end 1581 end 1582 end 1583 end, 1584 ArgV1 = ?mk_fun_var(ArgFun(Arg2), [Arg2, Dst]), 1585 ArgV2 = ?mk_fun_var(ArgFun(Arg1), [Arg1, Dst]), 1586 DstV = ?mk_fun_var(DstFun, Args), 1587 F = fun(A) -> 1588 try [mk_constraint(A, sub, True)] 1589 catch throw:error -> [] 1590 end 1591 end, 1592 Constrs = F(Arg1) ++ F(Arg2), 1593 Disj = mk_disj_constraint_list([mk_constraint(Dst, sub, False)|Constrs]), 1594 mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), 1595 mk_constraint(Arg1, sub, ArgV1), 1596 mk_constraint(Arg2, sub, ArgV2), 1597 Disj]); 1598get_bif_constr({erlang, 'not', 1}, Dst, [Arg] = Args, _State) -> 1599 True = t_from_term(true), 1600 False = t_from_term(false), 1601 Fun = fun(Var) -> 1602 fun(Map) -> 1603 Type = lookup_type(Var, Map), 1604 case t_is_any_atom(true, Type) of 1605 true -> False; 1606 false -> 1607 case t_is_any_atom(false, Type) of 1608 true -> True; 1609 false -> t_boolean() 1610 end 1611 end 1612 end 1613 end, 1614 ArgV = ?mk_fun_var(Fun(Dst), [Dst]), 1615 DstV = ?mk_fun_var(Fun(Arg), Args), 1616 mk_conj_constraint_list([mk_constraint(Arg, sub, ArgV), 1617 mk_constraint(Dst, sub, DstV)]); 1618get_bif_constr({erlang, '=:=', 2}, Dst, [Arg1, Arg2] = Args, _State) -> 1619 ArgFun = 1620 fun(Self, OtherVar) -> 1621 fun(Map) -> 1622 DstType = lookup_type(Dst, Map), 1623 OtherVarType = lookup_type(OtherVar, Map), 1624 case t_is_any_atom(true, DstType) of 1625 true -> OtherVarType; 1626 false -> 1627 case t_is_any_atom(false, DstType) of 1628 true -> 1629 case is_singleton_type(OtherVarType) of 1630 true -> t_subtract(lookup_type(Self, Map), OtherVarType); 1631 false -> t_any() 1632 end; 1633 false -> 1634 t_any() 1635 end 1636 end 1637 end 1638 end, 1639 DstFun = fun(Map) -> 1640 ArgType1 = lookup_type(Arg1, Map), 1641 ArgType2 = lookup_type(Arg2, Map), 1642 case t_is_none(t_inf(ArgType1, ArgType2)) of 1643 true -> t_from_term(false); 1644 false -> t_boolean() 1645 end 1646 end, 1647 DstArgs = [Dst, Arg1, Arg2], 1648 ArgV1 = ?mk_fun_var(ArgFun(Arg1, Arg2), DstArgs), 1649 ArgV2 = ?mk_fun_var(ArgFun(Arg2, Arg1), DstArgs), 1650 DstV = ?mk_fun_var(DstFun, Args), 1651 mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), 1652 mk_constraint(Arg1, sub, ArgV1), 1653 mk_constraint(Arg2, sub, ArgV2)]); 1654get_bif_constr({erlang, '==', 2}, Dst, [Arg1, Arg2] = Args, _State) -> 1655 DstFun = fun(Map) -> 1656 TmpArgTypes = lookup_type_list(Args, Map), 1657 bif_return(erlang, '==', 2, TmpArgTypes) 1658 end, 1659 ArgFun = 1660 fun(Var, Self) -> 1661 fun(Map) -> 1662 VarType = lookup_type(Var, Map), 1663 DstType = lookup_type(Dst, Map), 1664 case is_singleton_non_number_type(VarType) of 1665 true -> 1666 case t_is_any_atom(true, DstType) of 1667 true -> VarType; 1668 false -> 1669 case t_is_any_atom(false, DstType) of 1670 true -> t_subtract(lookup_type(Self, Map), VarType); 1671 false -> t_any() 1672 end 1673 end; 1674 false -> 1675 case t_is_any_atom(true, DstType) of 1676 true -> 1677 case t_is_number(VarType) of 1678 true -> t_number(); 1679 false -> 1680 case t_is_atom(VarType) of 1681 true -> VarType; 1682 false -> t_any() 1683 end 1684 end; 1685 false -> 1686 t_any() 1687 end 1688 end 1689 end 1690 end, 1691 DstV = ?mk_fun_var(DstFun, Args), 1692 ArgL = [Arg1, Arg2, Dst], 1693 ArgV1 = ?mk_fun_var(ArgFun(Arg2, Arg1), ArgL), 1694 ArgV2 = ?mk_fun_var(ArgFun(Arg1, Arg2), ArgL), 1695 mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), 1696 mk_constraint(Arg1, sub, ArgV1), 1697 mk_constraint(Arg2, sub, ArgV2)]); 1698get_bif_constr({erlang, element, 2} = _BIF, Dst, Args, 1699 #state{cs = Constrs}) -> 1700 GenType = erl_bif_types:type(erlang, element, 2), 1701 case t_is_none(GenType) of 1702 true -> ?debug("Bif: ~w failed\n", [_BIF]), throw(error); 1703 false -> 1704 Fun = fun(Map) -> 1705 ATs2 = lookup_type_list(Args, Map), 1706 bif_return(erlang, element, 2, ATs2) 1707 end, 1708 ReturnType = ?mk_fun_var(Fun, Args), 1709 ArgTypes = erl_bif_types:arg_types(erlang, element, 2), 1710 Cs = mk_constraints(Args, sub, ArgTypes), 1711 NewCs = 1712 case find_element(Args, Constrs) of 1713 'unknown' -> Cs; 1714 Elem -> [mk_constraint(Dst, eq, Elem)|Cs] 1715 end, 1716 mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType)|NewCs]) 1717 end; 1718get_bif_constr({M, F, A} = _BIF, Dst, Args, _State) -> 1719 GenType = erl_bif_types:type(M, F, A), 1720 case t_is_none(GenType) of 1721 true -> ?debug("Bif: ~w failed\n", [_BIF]), throw(error); 1722 false -> 1723 ReturnType = ?mk_fun_var(fun(Map) -> 1724 TmpArgTypes = lookup_type_list(Args, Map), 1725 bif_return(M, F, A, TmpArgTypes) 1726 end, Args), 1727 case erl_bif_types:is_known(M, F, A) of 1728 false -> 1729 case t_is_any(GenType) of 1730 true -> 1731 none; 1732 false -> 1733 mk_constraint(Dst, sub, ReturnType) 1734 end; 1735 true -> 1736 ArgTypes = erl_bif_types:arg_types(M, F, A), 1737 Cs = mk_constraints(Args, sub, ArgTypes), 1738 mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType)|Cs]) 1739 end 1740 end. 1741 1742eval_inv_arith('+', _Pos, Dst, Arg) -> 1743 bif_return(erlang, '-', 2, [Dst, Arg]); 1744eval_inv_arith('*', _Pos, Dst, Arg) -> 1745 Zero = t_from_term(0), 1746 case t_is_none(t_inf(Arg, Zero)) of 1747 false -> t_integer(); 1748 true -> 1749 TmpRet = bif_return(erlang, 'div', 2, [Dst, Arg]), 1750 %% If 0 is not part of the result, it cannot be part of the argument. 1751 case t_is_subtype(Zero, Dst) of 1752 false -> t_subtract(TmpRet, Zero); 1753 true -> TmpRet 1754 end 1755 end; 1756eval_inv_arith('-', 1, Dst, Arg) -> 1757 bif_return(erlang, '-', 2, [Arg, Dst]); 1758eval_inv_arith('-', 2, Dst, Arg) -> 1759 bif_return(erlang, '+', 2, [Arg, Dst]). 1760 1761range_inc(neg_inf) -> neg_inf; 1762range_inc(pos_inf) -> pos_inf; 1763range_inc(Int) when is_integer(Int) -> Int + 1. 1764 1765range_dec(neg_inf) -> neg_inf; 1766range_dec(pos_inf) -> pos_inf; 1767range_dec(Int) when is_integer(Int) -> Int - 1. 1768 1769get_bif_test_constr(Dst, Arg, Type, _State) -> 1770 ArgFun = fun(Map) -> 1771 DstType = lookup_type(Dst, Map), 1772 case t_is_any_atom(true, DstType) of 1773 true -> Type; 1774 false -> t_any() 1775 end 1776 end, 1777 ArgV = ?mk_fun_var(ArgFun, [Dst]), 1778 DstFun = fun(Map) -> 1779 ArgType = lookup_type(Arg, Map), 1780 case t_is_none(t_inf(ArgType, Type)) of 1781 true -> 1782 t_from_term(false); 1783 false -> 1784 case t_is_subtype(ArgType, Type) of 1785 true -> t_from_term(true); 1786 false -> t_boolean() 1787 end 1788 end 1789 end, 1790 DstV = ?mk_fun_var(DstFun, [Arg]), 1791 mk_conj_constraint_list([mk_constraint(Dst, sub, DstV), 1792 mk_constraint(Arg, sub, ArgV)]). 1793 1794%%============================================================================= 1795%% 1796%% Constraint solver. 1797%% 1798%%============================================================================= 1799 1800solve([Fun], State) -> 1801 ?debug("============ Analyzing Fun: ~tw ===========\n", 1802 [debug_lookup_name(Fun)]), 1803 solve_fun(Fun, map_new(), State); 1804solve([_|_] = SCC, State) -> 1805 ?debug("============ Analyzing SCC: ~tw ===========\n", 1806 [[debug_lookup_name(F) || F <- SCC]]), 1807 Users = comp_users(SCC, State), 1808 solve_scc(SCC, map_new(), State, Users, _ToSolve=SCC, false). 1809 1810comp_users(SCC, State) -> 1811 Vars0 = [{Fun, state__get_rec_var(Fun, State)} || Fun <- SCC], 1812 Vars = lists:sort([t_var_name(Var) || {_, {ok, Var}} <- Vars0]), 1813 family([{t_var(V), F} || 1814 F <- SCC, 1815 V <- ordsets:intersection(get_deps(state__get_cs(F, State)), 1816 Vars)]). 1817 1818solve_fun(Fun, FunMap, State) -> 1819 Cs = state__get_cs(Fun, State), 1820 Deps = get_deps(Cs), 1821 Ref = mk_constraint_ref(Fun, Deps), 1822 %% Note that functions are always considered to succeed. 1823 NewMap = solve(Fun, Ref, FunMap, State), 1824 NewType = lookup_type(Fun, NewMap), 1825 NewFunMap1 = case state__get_rec_var(Fun, State) of 1826 error -> FunMap; 1827 {ok, Var} -> enter_type(Var, NewType, FunMap) 1828 end, 1829 enter_type(Fun, NewType, NewFunMap1). 1830 1831solve_scc(SCC, Map, State, Users, ToSolve, TryingUnit) -> 1832 Vars0 = [{Fun, state__get_rec_var(Fun, State)} || Fun <- SCC], 1833 Vars = [Var || {_, {ok, Var}} <- Vars0], 1834 Funs = [Fun || {Fun, {ok, _}} <- Vars0], 1835 Types = unsafe_lookup_type_list(Funs, Map), 1836 RecTypes = [t_limit(Type, ?TYPE_LIMIT) || Type <- Types], 1837 CleanMap = lists:foldl(fun(Fun, AccFunMap) -> 1838 erase_type(t_var_name(Fun), AccFunMap) 1839 end, Map, ToSolve), 1840 Map1 = enter_type_lists(Vars, RecTypes, CleanMap), 1841 ?debug("Checking SCC: ~tw\n", [[debug_lookup_name(F) || F <- SCC]]), 1842 SolveFun = fun(X, Y) -> scc_fold_fun(X, Y, State) end, 1843 Map2 = lists:foldl(SolveFun, Map1, ToSolve), 1844 Updated = updated_vars_only(Vars, Map, Map2), 1845 case Updated =:= [] of 1846 true -> 1847 ?debug("SCC ~tw reached fixpoint\n", [SCC]), 1848 NewTypes = unsafe_lookup_type_list(Funs, Map2), 1849 case erl_types:any_none([t_fun_range(T) || T <- NewTypes]) 1850 andalso TryingUnit =:= false of 1851 true -> 1852 UnitTypes = 1853 [case t_is_none(t_fun_range(T)) of 1854 false -> T; 1855 true -> t_fun(t_fun_args(T), t_unit()) 1856 end || T <- NewTypes], 1857 Map3 = enter_type_lists(Funs, UnitTypes, Map2), 1858 solve_scc(SCC, Map3, State, Users, SCC, true); 1859 false -> 1860 Map2 1861 end; 1862 false -> 1863 ?debug("SCC ~tw did not reach fixpoint\n", [SCC]), 1864 ToSolve1 = affected(Updated, Users), 1865 solve_scc(SCC, Map2, State, Users, ToSolve1, TryingUnit) 1866 end. 1867 1868affected(Updated, Users) -> 1869 lists:umerge([case lists:keyfind(V, 1, Users) of 1870 {V, Vs} -> Vs; 1871 false -> [] 1872 end || V <- Updated]). 1873 1874scc_fold_fun(F, FunMap, State) -> 1875 Deps = get_deps(state__get_cs(F, State)), 1876 Cs = mk_constraint_ref(F, Deps), 1877 %% Note that functions are always considered to succeed. 1878 Map = solve(F, Cs, FunMap, State), 1879 NewType0 = unsafe_lookup_type(F, Map), 1880 NewType = t_limit(NewType0, ?TYPE_LIMIT), 1881 NewFunMap = case state__get_rec_var(F, State) of 1882 {ok, R} -> 1883 enter_type(R, NewType, enter_type(F, NewType, FunMap)); 1884 error -> 1885 enter_type(F, NewType, FunMap) 1886 end, 1887 ?debug("Done solving for function ~tw :: ~ts\n", [debug_lookup_name(F), 1888 format_type(NewType)]), 1889 NewFunMap. 1890 1891solve(Fun, Cs, FunMap, State) -> 1892 Solvers = State#state.solvers, 1893 R = [solver(S, solve_fun(S, Fun, Cs, FunMap, State)) || S <- Solvers], 1894 check_solutions(R, Fun, no_solver, no_map). 1895 1896solver(Solver, SolveFun) -> 1897 ?debug("Start solver ~w\n", [Solver]), 1898 try timer:tc(SolveFun) of 1899 {Time, {ok, Map}} -> 1900 ?debug("End solver ~w (~w microsecs)\n", [Solver, Time]), 1901 {Solver, Map, Time}; 1902 {_, _R} -> 1903 ?debug("Solver ~w returned unexpected result:\n ~P\n", 1904 [Solver, _R, 60]), 1905 throw(error) 1906 catch E:R:S -> 1907 io:format("Solver ~w failed: ~w:~p\n ~tp\n", [Solver, E, R, S]), 1908 throw(error) 1909 end. 1910 1911solve_fun(v1, _Fun, Cs, FunMap, State) -> 1912 fun() -> 1913 {ok, _MapDict, NewMap} = solve_ref_or_list(Cs, FunMap, map_new(), State), 1914 {ok, NewMap} 1915 end; 1916solve_fun(v2, Fun, _Cs, FunMap, State) -> 1917 fun() -> v2_solve_ref(Fun, FunMap, State) end. 1918 1919check_solutions([], _Fun, _S, Map) -> 1920 Map; 1921check_solutions([{S1,Map1,_Time1}|Maps], Fun, S, Map) -> 1922 ?debug("Solver ~w needed ~w microsecs\n", [S1, _Time1]), 1923 case Map =:= no_map orelse sane_maps(Map, Map1, [Fun], S, S1) of 1924 true -> 1925 check_solutions(Maps, Fun, S1, Map1); 1926 false -> 1927 ?debug("Constraint solvers do not agree on ~w\n", [Fun]), 1928 ?pp_map(atom_to_list(S), Map), 1929 ?pp_map(atom_to_list(S1), Map1), 1930 io:format("A bug was found. Please report it, and use the option " 1931 "`--solver v1' until the bug has been fixed.\n"), 1932 throw(error) 1933 end. 1934 1935sane_maps(Map1, Map2, Keys, _S1, _S2) -> 1936 lists:all(fun(Key) -> 1937 V1 = unsafe_lookup_type(Key, Map1), 1938 V2 = unsafe_lookup_type(Key, Map2), 1939 case t_is_equal(V1, V2) of 1940 true -> true; 1941 false -> 1942 ?debug("Constraint solvers do not agree on ~w\n", [Key]), 1943 ?debug("~w: ~ts\n", 1944 [_S1, format_type(unsafe_lookup_type(Key, Map1))]), 1945 ?debug("~w: ~ts\n", 1946 [_S2, format_type(unsafe_lookup_type(Key, Map2))]), 1947 false 1948 end 1949 end, Keys). 1950 1951%% Solver v2 1952 1953-record(v2_state, {constr_data = maps:new() :: map(), 1954 state :: state()}). 1955 1956v2_solve_ref(Fun, Map, State) -> 1957 V2State = #v2_state{state = State}, 1958 {ok, NewMap, _, _} = v2_solve_reference(Fun, Map, V2State), 1959 {ok, NewMap}. 1960 1961v2_solve(#constraint{}=C, Map, V2State) -> 1962 case solve_one_c(C, Map) of 1963 error -> 1964 report_failed_constraint(C, Map), 1965 {error, V2State}; 1966 {ok, {NewMap, U}} -> 1967 {ok, NewMap, V2State, U} 1968 end; 1969v2_solve(#constraint_list{type = disj}=C, Map, V2State) -> 1970 v2_solve_disjunct(C, Map, V2State); 1971v2_solve(#constraint_list{type = conj}=C, Map, V2State) -> 1972 v2_solve_conjunct(C, Map, V2State); 1973v2_solve(#constraint_ref{id = Id}, Map, V2State) -> 1974 v2_solve_reference(Id, Map, V2State). 1975 1976v2_solve_reference(Id, Map, V2State0) -> 1977 ?debug("Checking ref to fun: ~tw\n", [debug_lookup_name(Id)]), 1978 ?pp_map("Map", Map), 1979 pp_constr_data("solve_ref", V2State0), 1980 Map1 = restore_local_map(V2State0, Id, Map), 1981 State = V2State0#v2_state.state, 1982 Cs = state__get_cs(Id, State), 1983 Res = 1984 case state__is_self_rec(Id, State) of 1985 true -> v2_solve_self_recursive(Cs, Map1, Id, t_none(), V2State0); 1986 false -> v2_solve(Cs, Map1, V2State0) 1987 end, 1988 {FunType, V2State} = 1989 case Res of 1990 {error, V2State1} -> 1991 ?debug("Error solving for function ~tp\n", [debug_lookup_name(Id)]), 1992 Arity = state__fun_arity(Id, State), 1993 FunType0 = 1994 case state__prop_domain(t_var_name(Id), State) of 1995 error -> t_fun(Arity, t_none()); 1996 {ok, Dom} -> t_fun(Dom, t_none()) 1997 end, 1998 {FunType0, V2State1}; 1999 {ok, NewMap, V2State1, U} -> 2000 ?debug("Done solving fun: ~tp\n", [debug_lookup_name(Id)]), 2001 FunType0 = lookup_type(Id, NewMap), 2002 V2State2 = save_local_map(V2State1, Id, U, NewMap), 2003 {FunType0, V2State2} 2004 end, 2005 ?debug("ref Id=~w Assigned ~ts\n", [Id, format_type(FunType)]), 2006 {NewMap1, U1} = enter_var_type(Id, FunType, Map), 2007 {NewMap2, U2} = 2008 case state__get_rec_var(Id, State) of 2009 {ok, Var} -> enter_var_type(Var, FunType, NewMap1); 2010 error -> {NewMap1, []} 2011 end, 2012 {ok, NewMap2, V2State, lists:umerge(U1, U2)}. 2013 2014v2_solve_self_recursive(Cs, Map, Id, RecType0, V2State0) -> 2015 ?debug("Solving self recursive ~tw\n", [debug_lookup_name(Id)]), 2016 State = V2State0#v2_state.state, 2017 {ok, RecVar} = state__get_rec_var(Id, State), 2018 ?debug("OldRecType ~ts\n", [format_type(RecType0)]), 2019 RecType = t_limit(RecType0, ?TYPE_LIMIT), 2020 {Map1, U0} = enter_var_type(RecVar, RecType, Map), 2021 V2State1 = save_updated_vars1(V2State0, Cs, U0), % Probably not necessary 2022 case v2_solve(Cs, Map1, V2State1) of 2023 {error, _V2State}=Error -> 2024 case t_is_none(RecType0) of 2025 true -> 2026 %% Try again and assume that this is a non-terminating function. 2027 Arity = state__fun_arity(Id, State), 2028 NewRecType = t_fun(lists:duplicate(Arity, t_any()), t_unit()), 2029 v2_solve_self_recursive(Cs, Map, Id, NewRecType, V2State0); 2030 false -> 2031 Error 2032 end; 2033 {ok, NewMap, V2State, U} -> 2034 ?pp_map("recursive finished", NewMap), 2035 NewRecType = unsafe_lookup_type(Id, NewMap), 2036 case is_equal(NewRecType, RecType0) of 2037 true -> 2038 {NewMap2, U1} = enter_var_type(RecVar, NewRecType, NewMap), 2039 {ok, NewMap2, V2State, lists:umerge(U, U1)}; 2040 false -> 2041 v2_solve_self_recursive(Cs, Map, Id, NewRecType, V2State0) 2042 end 2043 end. 2044 2045enter_var_type(Var, Type, Map0) -> 2046 {Map, Vs} = enter_type2(Var, Type, Map0), 2047 {Map, [t_var_name(V) || V <- Vs]}. 2048 2049v2_solve_disjunct(Disj, Map, V2State0) -> 2050 #constraint_list{type = disj, id = _Id, list = Cs, masks = Masks} = Disj, 2051 ?debug("disjunct Id=~w~n", [_Id]), 2052 ?pp_map("Map", Map), 2053 pp_constr_data("disjunct", V2State0), 2054 case get_flags(V2State0, Disj) of 2055 {V2State1, failed_list} -> {error, V2State1}; % cannot happen 2056 {V2State1, Flags} when Flags =/= [] -> 2057 {ok, V2State, Eval, UL, MapL0, Uneval, Failed} = 2058 v2_solve_disj(Flags, Cs, 1, Map, V2State1, [], [], [], [], false), 2059 ?debug("disj ending _Id=~w Eval=~w, |Uneval|=~w |UL|=~w~n", 2060 [_Id, Eval, length(Uneval), length(UL)]), 2061 if Eval =:= [], Uneval =:= [] -> 2062 {error, failed_list(Disj, V2State0)}; 2063 true -> 2064 {Is0, UnIds} = lists:unzip(Uneval), 2065 MapL = [restore_local_map(V2State, Id, Map) || 2066 Id <- UnIds] ++ MapL0, 2067 %% If some branch has just failed every variable of the 2068 %% non-failed branches need to be checked, not just the 2069 %% updated ones. 2070 U0 = case Failed of 2071 false -> lists:umerge(UL); 2072 true -> constrained_keys(MapL) 2073 end, 2074 if U0 =:= [] -> {ok, Map, V2State, []}; 2075 true -> 2076 NotFailed = lists:umerge(Is0, Eval), 2077 U1 = [V || V <- U0, 2078 var_occurs_everywhere(V, Masks, NotFailed)], 2079 NewMap = join_maps(U1, MapL, Map), 2080 ?pp_map("NewMap", NewMap), 2081 U = updated_vars_only(U1, Map, NewMap), 2082 ?debug("disjunct finished _Id=~w\n", [_Id]), 2083 {ok, NewMap, V2State, U} 2084 end 2085 end 2086 end. 2087 2088var_occurs_everywhere(V, Masks, NotFailed) -> 2089 ordsets:is_subset(NotFailed, get_mask(V, Masks)). 2090 2091v2_solve_disj([I|Is], [C|Cs], I, Map0, V2State0, UL, MapL, Eval, Uneval, 2092 Failed0) -> 2093 Id = C#constraint_list.id, 2094 Map1 = restore_local_map(V2State0, Id, Map0), 2095 case v2_solve(C, Map1, V2State0) of 2096 {error, V2State} -> 2097 ?debug("disj error I=~w~n", [I]), 2098 Failed = Failed0 orelse not is_failed_list(C, V2State0), 2099 v2_solve_disj(Is, Cs, I+1, Map0, V2State, UL, MapL, Eval, Uneval, Failed); 2100 {ok, Map, V2State1, U} -> 2101 ?debug("disj I=~w U=~w~n", [I, U]), 2102 V2State = save_local_map(V2State1, Id, U, Map), 2103 ?pp_map("DMap", Map), 2104 v2_solve_disj(Is, Cs, I+1, Map0, V2State, [U|UL], [Map|MapL], 2105 [I|Eval], Uneval, Failed0) 2106 end; 2107v2_solve_disj([], [], _I, _Map, V2State, UL, MapL, Eval, Uneval, Failed) -> 2108 {ok, V2State, lists:reverse(Eval), UL, MapL, lists:reverse(Uneval), Failed}; 2109v2_solve_disj([every_i], Cs, I, Map, V2State, UL, MapL, Eval, Uneval, Failed) -> 2110 NewIs = case Cs of 2111 [] -> []; 2112 _ -> [I, every_i] 2113 end, 2114 v2_solve_disj(NewIs, Cs, I, Map, V2State, UL, MapL, Eval, Uneval, Failed); 2115v2_solve_disj(Is, [C|Cs], I, Map, V2State, UL, MapL, Eval, Uneval0, Failed) -> 2116 Uneval = [{I,C#constraint_list.id} || 2117 not is_failed_list(C, V2State)] ++ Uneval0, 2118 v2_solve_disj(Is, Cs, I+1, Map, V2State, UL, MapL, Eval, Uneval, Failed). 2119 2120save_local_map(#v2_state{constr_data = ConData}=V2State, Id, U, Map) -> 2121 Part0 = [{V,maps:get(V, Map)} || V <- U], 2122 Part1 = 2123 case maps:find(Id, ConData) of 2124 error -> []; % cannot happen 2125 {ok, {Part2,[]}} -> Part2 2126 end, 2127 ?debug("save local map Id=~w:\n", [Id]), 2128 Part = lists:ukeymerge(1, lists:keysort(1, Part0), Part1), 2129 ?pp_map("New Part", maps:from_list(Part0)), 2130 ?pp_map("Old Part", maps:from_list(Part1)), 2131 ?pp_map(" => Part", maps:from_list(Part)), 2132 V2State#v2_state{constr_data = maps:put(Id, {Part,[]}, ConData)}. 2133 2134restore_local_map(#v2_state{constr_data = ConData}, Id, Map0) -> 2135 case maps:find(Id, ConData) of 2136 error -> Map0; 2137 {ok, failed} -> Map0; 2138 {ok, {[],_}} -> Map0; 2139 {ok, {Part0,U}} -> 2140 Part = [KV || {K,_V} = KV <- Part0, not lists:member(K, U)], 2141 ?debug("restore local map Id=~w U=~w\n", [Id, U]), 2142 ?pp_map("Part", maps:from_list(Part)), 2143 ?pp_map("Map0", Map0), 2144 Map = lists:foldl(fun({K,V}, D) -> maps:put(K, V, D) end, Map0, Part), 2145 ?pp_map("Map", Map), 2146 Map 2147 end. 2148 2149v2_solve_conjunct(Conj, Map, V2State0) -> 2150 #constraint_list{type = conj, list = Cs} = Conj, 2151 ?debug("conjunct Id=~w~n", [Conj#constraint_list.id]), 2152 IsFlat = case Cs of [#constraint{}|_] -> true; _ -> false end, 2153 case get_flags(V2State0, Conj) of 2154 {V2State, failed_list} -> {error, V2State}; 2155 {V2State, Flags} -> 2156 v2_solve_conj(Flags, Cs, 1, Map, Conj, IsFlat, V2State, [], [], [], 2157 Map, Flags) 2158 end. 2159 2160%% LastMap and LastFlags are used for loop detection. 2161v2_solve_conj([I|Is], [Cs|Tail], I, Map0, Conj, IsFlat, V2State0, 2162 UL, NewFs0, VarsUp, LastMap, LastFlags) -> 2163 ?debug("conj Id=~w I=~w~n", [Conj#constraint_list.id, I]), 2164 true = IsFlat =:= is_record(Cs, constraint), 2165 pp_constr_data("conj", V2State0), 2166 case v2_solve(Cs, Map0, V2State0) of 2167 {error, V2State1} -> {error, failed_list(Conj, V2State1)}; 2168 {ok, Map, V2State1, []} -> 2169 v2_solve_conj(Is, Tail, I+1, Map, Conj, IsFlat, V2State1, 2170 UL, NewFs0, VarsUp, LastMap, LastFlags); 2171 {ok, Map, V2State1, U} when IsFlat -> % optimization 2172 %% It is ensured by enumerate_constraints() that every 2173 %% #constraint{} has a conjunct as parent, and that such a 2174 %% parent has nothing but #constraint{}:s as children, a fact 2175 %% which is used here to simplify the flag calculation. 2176 Mask = lists:umerge([get_mask(V, Conj#constraint_list.masks) || V <- U]), 2177 {Is1, NewF} = add_mask_to_flags(Is, Mask, I, []), 2178 NewFs = [NewF|NewFs0], 2179 v2_solve_conj(Is1, Tail, I+1, Map, Conj, IsFlat, V2State1, 2180 [U|UL], NewFs, VarsUp, LastMap, LastFlags); 2181 {ok, Map, V2State1, U} -> 2182 #constraint_list{masks = Masks, list = AllCs} = Conj, 2183 M = lists:keydelete(I, 1, vars_per_child(U, Masks)), 2184 {V2State2, NewF0} = save_updated_vars_list(AllCs, M, V2State1), 2185 {NewF, F} = lists:splitwith(fun(J) -> J < I end, NewF0), 2186 Is1 = umerge_mask(Is, F), 2187 NewFs = [NewF|NewFs0], 2188 v2_solve_conj(Is1, Tail, I+1, Map, Conj, IsFlat, V2State2, 2189 [U|UL], NewFs, VarsUp, LastMap, LastFlags) 2190 end; 2191v2_solve_conj([], _Cs, _I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp, 2192 LastMap, LastFlags) -> 2193 U = lists:umerge(UL), 2194 case lists:umerge(NewFs) of 2195 [] -> 2196 ?debug("conjunct finished Id=~w\n", [Conj#constraint_list.id]), 2197 {ok, Map, V2State, lists:umerge([U|VarsUp])}; 2198 NewFlags when NewFlags =:= LastFlags, Map =:= LastMap -> 2199 %% A loop was detected! The cause is some bug, possibly in erl_types. 2200 %% The evaluation continues, but the results can be wrong. 2201 report_detected_loop(Conj), 2202 {ok, Map, V2State, lists:umerge([U|VarsUp])}; 2203 NewFlags -> 2204 #constraint_list{type = conj, list = Cs} = Conj, 2205 v2_solve_conj(NewFlags, Cs, 1, Map, Conj, IsFlat, V2State, 2206 [], [], [U|VarsUp], Map, NewFlags) 2207 end; 2208v2_solve_conj([every_i], Cs, I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp, 2209 LastMap, LastFlags) -> 2210 NewIs = case Cs of 2211 [] -> []; 2212 _ -> [I, every_i] 2213 end, 2214 v2_solve_conj(NewIs, Cs, I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp, 2215 LastMap, LastFlags); 2216v2_solve_conj(Is, [_|Tail], I, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp, 2217 LastMap, LastFlags) -> 2218 v2_solve_conj(Is, Tail, I+1, Map, Conj, IsFlat, V2State, UL, NewFs, VarsUp, 2219 LastMap, LastFlags). 2220 2221-ifdef(DEBUG_LOOP_DETECTION). 2222report_detected_loop(Conj) -> 2223 io:format("A loop was detected in ~w\n", [Conj#constraint_list.id]). 2224-else. 2225report_detected_loop(_) -> 2226 ok. 2227-endif. 2228 2229add_mask_to_flags(Flags, [Im|M], I, L) when I > Im -> 2230 add_mask_to_flags(Flags, M, I, [Im|L]); 2231add_mask_to_flags(Flags, [_|M], _I, L) -> 2232 {umerge_mask(Flags, M), lists:reverse(L)}. 2233 2234umerge_mask([every_i]=Is, _F) -> 2235 Is; 2236umerge_mask(Is, F) -> 2237 lists:umerge(Is, F). 2238 2239get_mask(V, Masks) -> 2240 case maps:find(V, Masks) of 2241 error -> []; 2242 {ok, M} -> M 2243 end. 2244 2245get_flags(#v2_state{constr_data = ConData}=V2State0, C) -> 2246 #constraint_list{id = Id, list = Cs, masks = Masks} = C, 2247 case maps:find(Id, ConData) of 2248 error -> 2249 ?debug("get_flags Id=~w Flags=all ~w\n", [Id, length(Cs)]), 2250 V2State = V2State0#v2_state{constr_data = maps:put(Id, {[],[]}, ConData)}, 2251 {V2State, [every_i]}; 2252 {ok, failed} -> 2253 {V2State0, failed_list}; 2254 {ok, {Part,U}} when U =/= [] -> 2255 ?debug("get_flags Id=~w U=~w\n", [Id, U]), 2256 V2State = V2State0#v2_state{constr_data = maps:put(Id, {Part,[]}, ConData)}, 2257 save_updated_vars_list(Cs, vars_per_child(U, Masks), V2State) 2258 end. 2259 2260vars_per_child(U, Masks) -> 2261 family([{I, V} || V <- lists:usort(U), I <- get_mask(V, Masks)]). 2262 2263save_updated_vars_list(Cs, IU, V2State) -> 2264 save_updated_vars_list1(Cs, IU, V2State, 1, []). 2265 2266save_updated_vars_list1([C|Cs], [{I,U}|IU], V2State0, I, Is) -> 2267 V2State = save_updated_vars(C, U, V2State0), 2268 save_updated_vars_list1(Cs, IU, V2State, I+1, [I|Is]); 2269save_updated_vars_list1([], [], V2State, _I, Is) -> 2270 {V2State, lists:reverse(Is)}; 2271save_updated_vars_list1([_|Cs], IU, V2State, I, Is) -> 2272 save_updated_vars_list1(Cs, IU, V2State, I+1, Is). 2273 2274save_updated_vars(#constraint{}, _, V2State) -> 2275 V2State; 2276save_updated_vars(#constraint_list{}=C, U, V2State0) -> 2277 save_updated_vars1(V2State0, C, U); 2278save_updated_vars(#constraint_ref{id = Id}, U, V2State) -> 2279 Cs = state__get_cs(Id, V2State#v2_state.state), 2280 save_updated_vars(Cs, U, V2State). 2281 2282save_updated_vars1(V2State, C, U) -> 2283 #v2_state{constr_data = ConData} = V2State, 2284 #constraint_list{id = Id} = C, 2285 case maps:find(Id, ConData) of 2286 error -> V2State; % error means everything is flagged 2287 {ok, failed} -> V2State; 2288 {ok, {Part,U0}} -> 2289 %% Duplicates are not so common; let masks/2 remove them. 2290 U1 = U ++ U0, 2291 V2State#v2_state{constr_data = maps:put(Id, {Part,U1}, ConData)} 2292 end. 2293 2294-ifdef(DEBUG). 2295pp_constr_data(_Tag, #v2_state{constr_data = D}) -> 2296 io:format("Constr data at ~p\n", [_Tag]), 2297 _ = [begin 2298 case _PartU of 2299 {_Part, _U} -> 2300 io:format("Id: ~w Vars: ~w\n", [_Id, _U]), 2301 [?pp_map("Part", maps:from_list(_Part)) || _Part =/= []]; 2302 failed -> 2303 io:format("Id: ~w failed list\n", [_Id]) 2304 end 2305 end || 2306 {_Id, _PartU} <- lists:keysort(1, maps:to_list(D))], 2307 ok. 2308 2309-else. 2310pp_constr_data(_Tag, _V2State) -> 2311 ok. 2312-endif. 2313 2314failed_list(#constraint_list{id = Id}, #v2_state{constr_data = D}=V2State) -> 2315 ?debug("error list ~w~n", [Id]), 2316 V2State#v2_state{constr_data = maps:put(Id, failed, D)}. 2317 2318is_failed_list(#constraint_list{id = Id}, #v2_state{constr_data = D}) -> 2319 maps:find(Id, D) =:= {ok, failed}. 2320 2321%% Solver v1 2322 2323solve_ref_or_list(#constraint_ref{id = Id, deps = Deps}, 2324 Map, MapDict, State) -> 2325 {OldLocalMap, Check} = 2326 case maps:find(Id, MapDict) of 2327 error -> {map_new(), false}; 2328 {ok, M} -> {M, true} 2329 end, 2330 ?debug("Checking ref to fun: ~tw\n", [debug_lookup_name(Id)]), 2331 %% Note: mk_constraint_ref() has already removed Id from Deps. The 2332 %% reason for doing it there is that it makes it easy for 2333 %% calculate_masks() to make the corresponding adjustment for 2334 %% version v2. 2335 CheckDeps = ordsets:del_element(t_var_name(Id), Deps), 2336 true = CheckDeps =:= Deps, 2337 case Check andalso maps_are_equal(OldLocalMap, Map, CheckDeps) of 2338 true -> 2339 ?debug("Equal\n", []), 2340 {ok, MapDict, Map}; 2341 false -> 2342 ?debug("Not equal. Solving\n", []), 2343 Cs = state__get_cs(Id, State), 2344 Res = 2345 case state__is_self_rec(Id, State) of 2346 true -> solve_self_recursive(Cs, Map, MapDict, Id, t_none(), State); 2347 false -> solve_ref_or_list(Cs, Map, MapDict, State) 2348 end, 2349 {NewMapDict, FunType} = 2350 case Res of 2351 {error, NewMapDict0} -> 2352 ?debug("Error solving for function ~tp\n", [debug_lookup_name(Id)]), 2353 Arity = state__fun_arity(Id, State), 2354 FunType0 = 2355 case state__prop_domain(t_var_name(Id), State) of 2356 error -> t_fun(Arity, t_none()); 2357 {ok, Dom} -> t_fun(Dom, t_none()) 2358 end, 2359 {NewMapDict0, FunType0}; 2360 {ok, NewMapDict0, NewMap} -> 2361 ?debug("Done solving fun: ~tp\n", [debug_lookup_name(Id)]), 2362 FunType0 = lookup_type(Id, NewMap), 2363 {NewMapDict0, FunType0} 2364 end, 2365 ?debug(" Id=~w Assigned ~ts\n", [Id, format_type(FunType)]), 2366 NewMap1 = enter_type(Id, FunType, Map), 2367 NewMap2 = 2368 case state__get_rec_var(Id, State) of 2369 {ok, Var} -> enter_type(Var, FunType, NewMap1); 2370 error -> NewMap1 2371 end, 2372 {ok, maps:put(Id, NewMap2, NewMapDict), NewMap2} 2373 end; 2374solve_ref_or_list(#constraint_list{type=Type, list = Cs, deps = Deps, id = Id}, 2375 Map, MapDict, State) -> 2376 {OldLocalMap, Check} = 2377 case maps:find(Id, MapDict) of 2378 error -> {map_new(), false}; 2379 {ok, M} -> {M, true} 2380 end, 2381 ?debug("Checking ref to list: ~w\n", [Id]), 2382 if 2383 OldLocalMap =:= error -> {error, MapDict}; 2384 true -> 2385 case Check andalso maps_are_equal(OldLocalMap, Map, Deps) of 2386 true -> 2387 ?debug("~tw equal ~w\n", [Type, Id]), 2388 {ok, MapDict, Map}; 2389 false -> 2390 ?debug("~tw not equal: ~w. Solving\n", [Type, Id]), 2391 solve_clist(Cs, Type, Id, Deps, MapDict, Map, State) 2392 end 2393 end. 2394 2395solve_self_recursive(Cs, Map, MapDict, Id, RecType0, State) -> 2396 ?debug("Solving self recursive ~tw\n", [debug_lookup_name(Id)]), 2397 {ok, RecVar} = state__get_rec_var(Id, State), 2398 ?debug("OldRecType ~ts\n", [format_type(RecType0)]), 2399 RecType = t_limit(RecType0, ?TYPE_LIMIT), 2400 Map1 = enter_type(RecVar, RecType, erase_type(t_var_name(Id), Map)), 2401 ?pp_map("Map1", Map1), 2402 case solve_ref_or_list(Cs, Map1, MapDict, State) of 2403 {error, _} = Error -> 2404 case t_is_none(RecType0) of 2405 true -> 2406 %% Try again and assume that this is a non-terminating function. 2407 Arity = state__fun_arity(Id, State), 2408 NewRecType = t_fun(lists:duplicate(Arity, t_any()), t_unit()), 2409 solve_self_recursive(Cs, Map, MapDict, Id, NewRecType, State); 2410 false -> 2411 Error 2412 end; 2413 {ok, NewMapDict, NewMap} -> 2414 ?pp_map("NewMap", NewMap), 2415 NewRecType = unsafe_lookup_type(Id, NewMap), 2416 case is_equal(NewRecType, RecType0) of 2417 true -> 2418 {ok, NewMapDict, enter_type(RecVar, NewRecType, NewMap)}; 2419 false -> 2420 solve_self_recursive(Cs, Map, MapDict, Id, NewRecType, State) 2421 end 2422 end. 2423 2424solve_clist(Cs, conj, Id, Deps, MapDict, Map, State) -> 2425 case solve_cs(Cs, Map, MapDict, State) of 2426 {error, NewMapDict} -> 2427 {error, maps:put(Id, error, NewMapDict)}; 2428 {ok, NewMapDict, NewMap} = Ret -> 2429 case Cs of 2430 [_] -> 2431 %% Just a special case for one conjunctive constraint. 2432 Ret; 2433 _ -> 2434 case maps_are_equal(Map, NewMap, Deps) of 2435 true -> {ok, maps:put(Id, NewMap, NewMapDict), NewMap}; 2436 false -> solve_clist(Cs, conj, Id, Deps, NewMapDict, NewMap, State) 2437 end 2438 end 2439 end; 2440solve_clist(Cs, disj, Id, _Deps, MapDict, Map, State) -> 2441 Fun = fun(C, Dict) -> 2442 case solve_ref_or_list(C, Map, Dict, State) of 2443 {ok, NewDict, NewMap} -> {{ok, NewMap}, NewDict}; 2444 {error, _NewDict} = Error -> Error 2445 end 2446 end, 2447 {Maps, NewMapDict} = lists:mapfoldl(Fun, MapDict, Cs), 2448 case [X || {ok, X} <- Maps] of 2449 [] -> {error, maps:put(Id, error, NewMapDict)}; 2450 MapList -> 2451 NewMap = join_maps(MapList), 2452 {ok, maps:put(Id, NewMap, NewMapDict), NewMap} 2453 end. 2454 2455solve_cs([#constraint_ref{} = C|Tail], Map, MapDict, State) -> 2456 case solve_ref_or_list(C, Map, MapDict, State) of 2457 {ok, NewMapDict, Map1} -> solve_cs(Tail, Map1, NewMapDict, State); 2458 {error, _NewMapDict} = Error -> Error 2459 end; 2460solve_cs([#constraint_list{} = C|Tail], Map, MapDict, State) -> 2461 case solve_ref_or_list(C, Map, MapDict, State) of 2462 {ok, NewMapDict, Map1} -> solve_cs(Tail, Map1, NewMapDict, State); 2463 {error, _NewMapDict} = Error -> Error 2464 end; 2465solve_cs([#constraint{} = C|Tail], Map, MapDict, State) -> 2466 case solve_one_c(C, Map) of 2467 error -> 2468 report_failed_constraint(C, Map), 2469 {error, MapDict}; 2470 {ok, {NewMap, _U}} -> 2471 solve_cs(Tail, NewMap, MapDict, State) 2472 end; 2473solve_cs([], Map, MapDict, _State) -> 2474 {ok, MapDict, Map}. 2475 2476solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map) -> 2477 LhsType = lookup_type(Lhs, Map), 2478 RhsType = lookup_type(Rhs, Map), 2479 Inf = t_inf(LhsType, RhsType), 2480 ?debug("Solving: ~ts :: ~ts ~w ~ts :: ~ts\n\tInf: ~ts\n", 2481 [format_type(Lhs), format_type(LhsType), Op, 2482 format_type(Rhs), format_type(RhsType), format_type(Inf)]), 2483 case t_is_none(Inf) of 2484 true -> error; 2485 false -> 2486 case Op of 2487 sub -> solve_subtype(Lhs, Inf, Map); 2488 eq -> 2489 case solve_subtype(Lhs, Inf, Map) of 2490 error -> error; 2491 {ok, {Map1, U1}} -> 2492 case solve_subtype(Rhs, Inf, Map1) of 2493 error -> error; 2494 {ok, {Map2, U2}} -> {ok, {Map2, lists:umerge(U1, U2)}} 2495 end 2496 end 2497 end 2498 end. 2499 2500solve_subtype(Type, Inf, Map) -> 2501 %% case cerl:is_literal(Type) of 2502 %% true -> 2503 %% case t_is_subtype(t_from_term(cerl:concrete(Type)), Inf) of 2504 %% true -> {ok, Map}; 2505 %% false -> error 2506 %% end; 2507 %% false -> 2508 try t_unify(Type, Inf) of 2509 {_, List} -> {ok, enter_type_list(List, Map)} 2510 catch 2511 throw:{mismatch, _T1, _T2} -> 2512 ?debug("Mismatch between ~ts and ~ts\n", 2513 [format_type(_T1), format_type(_T2)]), 2514 error 2515 end. 2516 %% end. 2517 2518report_failed_constraint(_C, _Map) -> 2519 ?debug("+++++++++++\nFailed: ~ts :: ~ts ~w ~ts :: ~ts\n+++++++++++\n", 2520 [format_type(_C#constraint.lhs), 2521 format_type(lookup_type(_C#constraint.lhs, _Map)), 2522 _C#constraint.op, 2523 format_type(_C#constraint.rhs), 2524 format_type(lookup_type(_C#constraint.rhs, _Map))]). 2525 2526%% ============================================================================ 2527%% 2528%% Maps and types. 2529%% 2530%% ============================================================================ 2531 2532map_new() -> 2533 maps:new(). 2534 2535join_maps([Map]) -> 2536 Map; 2537join_maps(Maps) -> 2538 Keys = constrained_keys(Maps), 2539 join_maps(Keys, Maps, map_new()). 2540 2541constrained_keys(Maps) -> 2542 lists:foldl(fun(TmpMap, AccKeys) -> 2543 [Key || Key <- AccKeys, maps:is_key(Key, TmpMap)] 2544 end, 2545 maps:keys(hd(Maps)), tl(Maps)). 2546 2547join_maps([Key|Left], Maps = [Map|MapsLeft], AccMap) -> 2548 NewType = join_one_key(Key, MapsLeft, lookup_type(Key, Map)), 2549 NewAccMap = enter_type(Key, NewType, AccMap), 2550 join_maps(Left, Maps, NewAccMap); 2551join_maps([], _Maps, AccMap) -> 2552 AccMap. 2553 2554join_one_key(Key, [Map|Maps], Type) -> 2555 case t_is_any(Type) of 2556 true -> Type; 2557 false -> 2558 NewType = lookup_type(Key, Map), 2559 case is_equal(NewType, Type) of 2560 true -> join_one_key(Key, Maps, Type); 2561 false -> join_one_key(Key, Maps, t_sup(NewType, Type)) 2562 end 2563 end; 2564join_one_key(_Key, [], Type) -> 2565 Type. 2566 2567maps_are_equal(Map1, Map2, Deps) -> 2568 NewDeps = prune_keys(Map1, Map2, Deps), 2569 maps_are_equal_1(Map1, Map2, NewDeps). 2570 2571maps_are_equal_1(Map1, Map2, [H|Tail]) -> 2572 T1 = lookup_type(H, Map1), 2573 T2 = lookup_type(H, Map2), 2574 case is_equal(T1, T2) of 2575 true -> maps_are_equal_1(Map1, Map2, Tail); 2576 false -> 2577 ?debug("~w: ~ts =/= ~ts\n", [H, format_type(T1), format_type(T2)]), 2578 false 2579 end; 2580maps_are_equal_1(_Map1, _Map2, []) -> 2581 true. 2582 2583-define(PRUNE_LIMIT, 100). 2584 2585prune_keys(Map1, Map2, Deps) -> 2586 %% This is only worthwhile if the number of deps is reasonably large, 2587 %% and also bigger than the number of elements in the maps. 2588 NofDeps = length(Deps), 2589 case NofDeps > ?PRUNE_LIMIT of 2590 true -> 2591 Keys1 = maps:keys(Map1), 2592 case length(Keys1) > NofDeps of 2593 true -> 2594 Set1 = lists:sort(Keys1), 2595 Set2 = lists:sort(maps:keys(Map2)), 2596 ordsets:intersection(ordsets:union(Set1, Set2), Deps); 2597 false -> 2598 Deps 2599 end; 2600 false -> 2601 Deps 2602 end. 2603 2604enter_type(Key, Val, Map) when is_integer(Key) -> 2605 ?debug("Entering ~ts :: ~ts\n", [format_type(t_var(Key)), format_type(Val)]), 2606 %% Keep any() in the map if it is opaque: 2607 case is_equal(Val, t_any()) of 2608 true -> 2609 erase_type(Key, Map); 2610 false -> 2611 LimitedVal = t_limit(Val, ?INTERNAL_TYPE_LIMIT), 2612 case is_equal(LimitedVal, Val) of 2613 true -> ok; 2614 false -> ?debug("LimitedVal ~ts\n", [format_type(LimitedVal)]) 2615 end, 2616 case maps:find(Key, Map) of 2617 {ok, Value} -> 2618 case is_equal(Value, LimitedVal) of 2619 true -> Map; 2620 false -> map_store(Key, LimitedVal, Map) 2621 end; 2622 error -> map_store(Key, LimitedVal, Map) 2623 end 2624 end; 2625enter_type(Key, Val, Map) -> 2626 KeyName = t_var_name(Key), 2627 enter_type(KeyName, Val, Map). 2628 2629enter_type_lists([Key|KeyTail], [Val|ValTail], Map) -> 2630 Map1 = enter_type(Key, Val, Map), 2631 enter_type_lists(KeyTail, ValTail, Map1); 2632enter_type_lists([], [], Map) -> 2633 Map. 2634 2635enter_type_list(KeyVals, Map) -> 2636 enter_type_list(KeyVals, Map, []). 2637 2638enter_type_list([{Key, Val}|Tail], Map, U0) -> 2639 {Map1,U1} = enter_type2(Key, Val, Map), 2640 enter_type_list(Tail, Map1, U1++U0); 2641enter_type_list([], Map, U) -> 2642 {Map, ordsets:from_list(U)}. 2643 2644enter_type2(Key, Val, Map) -> 2645 Map1 = enter_type(Key, Val, Map), 2646 {Map1, [Key || not is_same(Key, Map, Map1)]}. 2647 2648map_store(Key, Val, Map) -> 2649 ?debug("Storing ~tw :: ~ts\n", [Key, format_type(Val)]), 2650 maps:put(Key, Val, Map). 2651 2652erase_type(Key, Map) -> 2653 maps:remove(Key, Map). 2654 2655lookup_type_list(List, Map) -> 2656 [lookup_type(X, Map) || X <- List]. 2657 2658unsafe_lookup_type(Key, Map) -> 2659 case maps:find(t_var_name(Key), Map) of 2660 {ok, Type} -> Type; 2661 error -> t_none() 2662 end. 2663 2664unsafe_lookup_type_list(List, Map) -> 2665 [unsafe_lookup_type(X, Map) || X <- List]. 2666 2667lookup_type(Key, Map) when is_integer(Key) -> 2668 case maps:find(Key, Map) of 2669 error -> t_any(); 2670 {ok, Val} -> Val 2671 end; 2672lookup_type(#fun_var{'fun' = Fun}, Map) -> 2673 Fun(Map); 2674lookup_type(Key, Map) -> 2675 %% Seems unused and dialyzer complains about it -- commented out. 2676 %% case cerl:is_literal(Key) of 2677 %% true -> t_from_term(cerl:concrete(Key)); 2678 %% false -> 2679 t_subst(Key, Map). 2680 %% end. 2681 2682mk_var(Var) -> 2683 case cerl:is_literal(Var) of 2684 true -> Var; 2685 false -> 2686 case cerl:is_c_values(Var) of 2687 true -> t_product(mk_var_no_lit_list(cerl:values_es(Var))); 2688 false -> t_var(cerl_trees:get_label(Var)) 2689 end 2690 end. 2691 2692mk_var_list(List) -> 2693 [mk_var(X) || X <- List]. 2694 2695mk_var_no_lit(Var) -> 2696 case cerl:is_literal(Var) of 2697 true -> t_from_term(cerl:concrete(Var)); 2698 false -> mk_var(Var) 2699 end. 2700 2701mk_var_no_lit_list(List) -> 2702 [mk_var_no_lit(X) || X <- List]. 2703 2704updated_vars_only(U, OldMap, NewMap) -> 2705 [V || V <- U, not is_same(V, OldMap, NewMap)]. 2706 2707is_same(Key, Map1, Map2) -> 2708 is_equal(lookup_type(Key, Map1), lookup_type(Key, Map2)). 2709 2710is_equal(Type1, Type2) -> 2711 t_is_equal(Type1, Type2). 2712 2713%% ============================================================================ 2714%% 2715%% The State. 2716%% 2717%% ============================================================================ 2718 2719new_state(MFAs, NextLabel, CallGraph, CServer, Plt, PropTypes0, Solvers) -> 2720 List_SCC = 2721 [begin 2722 {Var, Label} = dialyzer_codeserver:lookup_mfa_var_label(MFA, CServer), 2723 {{MFA, Var}, t_var(Label)} 2724 end || MFA <- MFAs], 2725 {List, SCC} = lists:unzip(List_SCC), 2726 NameMap = maps:from_list(List), 2727 SelfRec = 2728 case SCC of 2729 [OneF] -> 2730 Label = t_var_name(OneF), 2731 case dialyzer_callgraph:is_self_rec(Label, CallGraph) of 2732 true -> OneF; 2733 false -> false 2734 end; 2735 _Many -> false 2736 end, 2737 PropTypes = dict:from_list(PropTypes0), 2738 #state{callgraph = CallGraph, name_map = NameMap, next_label = NextLabel, 2739 prop_types = PropTypes, plt = Plt, scc = ordsets:from_list(SCC), 2740 mfas = MFAs, self_rec = SelfRec, solvers = Solvers, 2741 cserver = CServer}. 2742 2743state__set_module(State, Module) -> 2744 State#state{module = Module}. 2745 2746state__set_in_match(State, Bool) -> 2747 State#state{in_match = Bool}. 2748 2749state__is_in_match(#state{in_match = Bool}) -> 2750 Bool. 2751 2752state__set_in_guard(State, Bool) -> 2753 State#state{in_guard = Bool}. 2754 2755state__is_in_guard(#state{in_guard = Bool}) -> 2756 Bool. 2757 2758state__get_fun_prototype(Op, Arity, State) -> 2759 case t_is_fun(Op) of 2760 true -> {State, Op}; 2761 false -> 2762 {State1, [Ret|Args]} = state__mk_vars(Arity+1, State), 2763 Fun = t_fun(Args, Ret), 2764 {State1, Fun} 2765 end. 2766 2767state__lookup_rec_var_in_scope(MFA, #state{name_map = NameMap}) -> 2768 maps:find(MFA, NameMap). 2769 2770state__store_fun_arity(Tree, #state{fun_arities = Map} = State) -> 2771 Arity = length(cerl:fun_vars(Tree)), 2772 Id = mk_var(Tree), 2773 State#state{fun_arities = maps:put(Id, Arity, Map)}. 2774 2775state__fun_arity(Id, #state{fun_arities = Map}) -> 2776 maps:get(Id, Map). 2777 2778state__lookup_undef_var(Tree, #state{callgraph = CG, plt = Plt}) -> 2779 Label = cerl_trees:get_label(Tree), 2780 case dialyzer_callgraph:lookup_rec_var(Label, CG) of 2781 error -> error; 2782 {ok, MFA} -> 2783 case dialyzer_plt:lookup(Plt, MFA) of 2784 none -> error; 2785 {value, {RetType, ArgTypes}} -> 2786 {ok, t_fun(ArgTypes, RetType)} 2787 end 2788 end. 2789 2790state__lookup_apply(Tree, #state{callgraph = Callgraph}) -> 2791 Apply = cerl_trees:get_label(Tree), 2792 case dialyzer_callgraph:lookup_call_site(Apply, Callgraph) of 2793 error -> 2794 unknown; 2795 {ok, List} -> 2796 case lists:member(external, List) of 2797 true -> unknown; 2798 false -> List 2799 end 2800 end. 2801 2802get_apply_constr(FunLabels, Dst, ArgTypes, #state{callgraph = CG} = State) -> 2803 MFAs = [dialyzer_callgraph:lookup_name(Label, CG) || Label <- FunLabels], 2804 case lists:member(error, MFAs) of 2805 true -> error; 2806 false -> 2807 Constrs0 = 2808 [begin 2809 State1 = state__new_constraint_context(State), 2810 try get_plt_constr(MFA, Dst, ArgTypes, State1) of 2811 State2 -> state__cs(State2) 2812 catch 2813 throw:error -> error 2814 end 2815 end || {ok, MFA} <- MFAs], 2816 case [C || C <- Constrs0, C =/= error] of 2817 [] -> throw(error); 2818 Constrs -> 2819 ApplyConstr = mk_disj_constraint_list(Constrs), 2820 {ok, state__store_conj(ApplyConstr, State)} 2821 end 2822 end. 2823 2824state__scc(#state{scc = SCC}) -> 2825 SCC. 2826 2827state__add_fun_to_scc(Fun, #state{scc = SCC} = State) -> 2828 State#state{scc = ordsets:add_element(Fun, SCC)}. 2829 2830state__plt(#state{plt = PLT}) -> 2831 PLT. 2832 2833state__new_constraint_context(State) -> 2834 State#state{cs = []}. 2835 2836state__prop_domain(FunLabel, #state{prop_types = PropTypes}) -> 2837 case dict:find(FunLabel, PropTypes) of 2838 error -> error; 2839 {ok, {_Range_Fun, Dom}} -> {ok, Dom}; 2840 {ok, FunType} -> {ok, t_fun_args(FunType)} 2841 end. 2842 2843state__add_prop_constrs(Tree, #state{prop_types = PropTypes} = State) -> 2844 Label = cerl_trees:get_label(Tree), 2845 case dict:find(Label, PropTypes) of 2846 error -> State; 2847 {ok, FunType} -> 2848 case t_fun_args(FunType) of 2849 unknown -> State; 2850 ArgTypes -> 2851 case erl_types:any_none(ArgTypes) of 2852 true -> not_called; 2853 false -> 2854 ?debug("Adding propagated constr: ~ts for function ~tw\n", 2855 [format_type(FunType), debug_lookup_name(mk_var(Tree))]), 2856 FunVar = mk_var(Tree), 2857 state__store_conj(FunVar, sub, FunType, State) 2858 end 2859 end 2860 end. 2861 2862state__cs(#state{cs = Cs}) -> 2863 mk_conj_constraint_list(Cs). 2864 2865state__store_conj(C, #state{cs = Cs} = State) -> 2866 State#state{cs = [C|Cs]}. 2867 2868state__store_conj_list([H|T], State) -> 2869 State1 = state__store_conj(H, State), 2870 state__store_conj_list(T, State1); 2871state__store_conj_list([], State) -> 2872 State. 2873 2874state__store_conj(Lhs, Op, Rhs, #state{cs = Cs} = State) -> 2875 State#state{cs = [mk_constraint(Lhs, Op, Rhs)|Cs]}. 2876 2877state__store_conj_lists(List1, Op, List2, State) -> 2878 {NewList1, NewList2} = strip_of_any_constrs(List1, List2), 2879 state__store_conj_lists_1(NewList1, Op, NewList2, State). 2880 2881strip_of_any_constrs(List1, List2) -> 2882 strip_of_any_constrs(List1, List2, [], []). 2883 2884strip_of_any_constrs([T1|Left1], [T2|Left2], Acc1, Acc2) -> 2885 case t_is_any(T1) orelse constraint_opnd_is_any(T2) of 2886 true -> strip_of_any_constrs(Left1, Left2, Acc1, Acc2); 2887 false -> strip_of_any_constrs(Left1, Left2, [T1|Acc1], [T2|Acc2]) 2888 end; 2889strip_of_any_constrs([], [], Acc1, Acc2) -> 2890 {Acc1, Acc2}. 2891 2892state__store_conj_lists_1([Arg1|Arg1Tail], Op, [Arg2|Arg2Tail], State) -> 2893 State1 = state__store_conj(Arg1, Op, Arg2, State), 2894 state__store_conj_lists_1(Arg1Tail, Op, Arg2Tail, State1); 2895state__store_conj_lists_1([], _Op, [], State) -> 2896 State. 2897 2898state__mk_var(#state{next_label = NL} = State) -> 2899 {State#state{next_label = NL+1}, t_var(NL)}. 2900 2901state__mk_vars(N, #state{next_label = NL} = State) -> 2902 NewLabel = NL + N, 2903 Vars = [t_var(X) || X <- lists:seq(NL, NewLabel-1)], 2904 {State#state{next_label = NewLabel}, Vars}. 2905 2906state__store_constrs(Id, Cs, #state{cmap = Map} = State) -> 2907 NewMap = maps:put(Id, Cs, Map), 2908 State#state{cmap = NewMap}. 2909 2910state__get_cs(Var, #state{cmap = Map}) -> 2911 maps:get(Var, Map). 2912 2913state__is_self_rec(Fun, #state{self_rec = SelfRec}) -> 2914 not (SelfRec =:= 'false') andalso is_equal(Fun, SelfRec). 2915 2916state__store_funs(Vars0, Funs0, #state{fun_map = Map} = State) -> 2917 debug_make_name_map(Vars0, Funs0), 2918 Vars = mk_var_list(Vars0), 2919 Funs = mk_var_list(Funs0), 2920 NewMap = lists:foldl(fun({Var, Fun}, MP) -> maps:put(Fun, Var, MP) end, 2921 Map, lists:zip(Vars, Funs)), 2922 State#state{fun_map = NewMap}. 2923 2924state__get_rec_var(Fun, #state{fun_map = Map}) -> 2925 maps:find(Fun, Map). 2926 2927state__finalize(State) -> 2928 State1 = state__new_constraint_context(State), 2929 State2 = enumerate_constraints(State1), 2930 order_fun_constraints(State2). 2931 2932%% ============================================================================ 2933%% 2934%% Constraints 2935%% 2936%% ============================================================================ 2937 2938-spec mk_constraint(erl_types:erl_type(), 2939 constr_op(), 2940 fvar_or_type()) -> #constraint{}. 2941 2942mk_constraint(Lhs, Op, Rhs) -> 2943 case t_is_any(Lhs) orelse constraint_opnd_is_any(Rhs) of 2944 false -> 2945 Deps = find_constraint_deps([Lhs, Rhs]), 2946 C = mk_constraint_1(Lhs, Op, Rhs, Deps), 2947 case Deps =:= [] of 2948 true -> 2949 %% This constraint is constant. Solve it immediately. 2950 case solve_one_c(C, map_new()) of 2951 error -> throw(error); 2952 _R -> 2953 %% This is always true, keep it anyway for logistic reasons 2954 C 2955 end; 2956 false -> 2957 C 2958 end; 2959 true -> 2960 mk_constraint_any(Op) 2961 end. 2962 2963mk_constraint_any(Op) -> 2964 mk_constraint_1(t_any(), Op, t_any(), []). 2965 2966%% the following function is used so that we do not call 2967%% erl_types:t_is_any/1 with a term other than an erl_type() 2968-spec constraint_opnd_is_any(fvar_or_type()) -> boolean(). 2969 2970constraint_opnd_is_any(#fun_var{}) -> false; 2971constraint_opnd_is_any(Type) -> t_is_any(Type). 2972 2973-ifdef(DEBUG). 2974 2975-spec mk_fun_var(integer(), 2976 fun((_) -> erl_types:erl_type()), 2977 [erl_types:erl_type()]) -> #fun_var{}. 2978 2979mk_fun_var(Line, Fun, Types) -> 2980 Deps = [t_var_name(Var) || Var <- t_collect_vars(t_product(Types))], 2981 #fun_var{'fun' = Fun, deps = ordsets:from_list(Deps), origin = Line}. 2982 2983pp_map(S, Map) -> 2984 ?debug("\t~s: ~p\n", 2985 [S, [{X, lists:flatten(format_type(Y))} || 2986 {X, Y} <- lists:keysort(1, maps:to_list(Map))]]). 2987 2988-else. 2989 2990-spec mk_fun_var(fun((_) -> erl_types:erl_type()), [erl_types:erl_type()]) -> #fun_var{}. 2991 2992mk_fun_var(Fun, Types) -> 2993 Deps = [t_var_name(Var) || Var <- t_collect_vars(t_product(Types))], 2994 #fun_var{'fun' = Fun, deps = ordsets:from_list(Deps)}. 2995 2996-endif. 2997 2998-spec get_deps(constr()) -> deps(). 2999 3000get_deps(#constraint{deps = D}) -> D; 3001get_deps(#constraint_list{deps = D}) -> D; 3002get_deps(#constraint_ref{deps = D}) -> D. 3003 3004-spec find_constraint_deps([fvar_or_type()]) -> deps(). 3005 3006find_constraint_deps(List) -> 3007 ordsets:from_list(find_constraint_deps(List, [])). 3008 3009find_constraint_deps([#fun_var{deps = Deps}|Tail], Acc) -> 3010 find_constraint_deps(Tail, [Deps|Acc]); 3011find_constraint_deps([Type|Tail], Acc) -> 3012 NewAcc = [[t_var_name(D) || D <- t_collect_vars(Type)]|Acc], 3013 find_constraint_deps(Tail, NewAcc); 3014find_constraint_deps([], Acc) -> 3015 lists:append(Acc). 3016 3017mk_constraint_1(Lhs, eq, Rhs, Deps) when Lhs < Rhs -> 3018 #constraint{lhs = Lhs, op = eq, rhs = Rhs, deps = Deps}; 3019mk_constraint_1(Lhs, eq, Rhs, Deps) -> 3020 #constraint{lhs = Rhs, op = eq, rhs = Lhs, deps = Deps}; 3021mk_constraint_1(Lhs, Op, Rhs, Deps) -> 3022 #constraint{lhs = Lhs, op = Op, rhs = Rhs, deps = Deps}. 3023 3024mk_constraints([Lhs|LhsTail], Op, [Rhs|RhsTail]) -> 3025 [mk_constraint(Lhs, Op, Rhs) | 3026 mk_constraints(LhsTail, Op, RhsTail)]; 3027mk_constraints([], _Op, []) -> 3028 []. 3029 3030mk_constraint_ref(Id, Deps) -> 3031 %% See also solve_ref_or_list(), #constraint_ref{}. 3032 Ds = ordsets:del_element(t_var_name(Id), Deps), 3033 #constraint_ref{id = Id, deps = Ds}. 3034 3035mk_constraint_list(Type, List) -> 3036 List1 = ordsets:from_list(lift_lists(Type, List)), 3037 case Type of 3038 conj -> 3039 List2 = ordsets:filter(fun(X) -> get_deps(X) =/= [] end, List1), 3040 mk_constraint_list_cont(Type, List2); 3041 disj -> 3042 case lists:any(fun(X) -> get_deps(X) =:= [] end, List1) of 3043 true -> mk_constraint_list_cont(Type, [mk_constraint_any(eq)]); 3044 false -> mk_constraint_list_cont(Type, List1) 3045 end 3046 end. 3047 3048mk_constraint_list_cont(Type, List) -> 3049 Deps = calculate_deps(List), 3050 case Deps =:= [] of 3051 true -> #constraint_list{type = conj, 3052 list = [mk_constraint_any(eq)], 3053 deps = []}; 3054 false -> #constraint_list{type = Type, list = List, deps = Deps} 3055 end. 3056 3057lift_lists(Type, List) -> 3058 lift_lists(Type, List, []). 3059 3060lift_lists(Type, [#constraint_list{type = Type, list = List}|Tail], Acc) -> 3061 lift_lists(Type, Tail, List++Acc); 3062lift_lists(Type, [C|Tail], Acc) -> 3063 lift_lists(Type, Tail, [C|Acc]); 3064lift_lists(_Type, [], Acc) -> 3065 Acc. 3066 3067update_constraint_list(CL, List) -> 3068 CL#constraint_list{list = List}. 3069 3070%% We expand guard constraints into dijunctive normal form to gain 3071%% precision in simple guards. However, because of the exponential 3072%% growth of this expansion in the presens of disjunctions we can even 3073%% get into trouble while expanding. 3074%% 3075%% To limit this we only expand when the number of disjunctions are 3076%% below a certain limit. This limit is currently set based on the 3077%% behaviour of boolean 'or'. 3078%% 3079%% V1 = V2 or V3 3080%% 3081%% Gives us in simplified form the constraints 3082%% 3083%% <Some cs> * ((V1 = true) + (V2 = true) + (V1 = false)) 3084%% 3085%% and thus a three-parted disjunction. If want to allow for two 3086%% levels of disjunction we need to have 3^2 = 9 disjunctions. If we 3087%% want three levels we need 3^3 = 27 disjunctions. More than that 3088%% seems unnecessary and tends to blow up. 3089%% 3090%% Note that by not expanding we lose some precision, but we get a 3091%% safe over approximation. 3092 3093-define(DISJ_NORM_FORM_LIMIT, 28). 3094 3095mk_disj_norm_form(#constraint_list{} = CL) -> 3096 try 3097 List1 = expand_to_conjunctions(CL), 3098 mk_disj_constraint_list(List1) 3099 catch 3100 throw:too_many_disj -> CL 3101 end. 3102 3103expand_to_conjunctions(#constraint_list{type = conj, list = List}) -> 3104 List1 = [C || C <- List, is_simple_constraint(C)], 3105 List2 = [expand_to_conjunctions(C) || #constraint_list{} = C <- List], 3106 case List2 =:= [] of 3107 true -> [mk_conj_constraint_list(List1)]; 3108 false -> 3109 case List2 of 3110 [JustOneList] -> 3111 [mk_conj_constraint_list([L|List1]) || L <- JustOneList]; 3112 _ -> 3113 combine_conj_lists(List2, List1) 3114 end 3115 end; 3116expand_to_conjunctions(#constraint_list{type = disj, list = List}) -> 3117 if length(List) > ?DISJ_NORM_FORM_LIMIT -> throw(too_many_disj); 3118 true -> ok 3119 end, 3120 List1 = [C || C <- List, is_simple_constraint(C)], 3121 %% Just an assert. 3122 [] = [C || #constraint{} = C <- List1], 3123 Expanded = lists:append([expand_to_conjunctions(C) 3124 || #constraint_list{} = C <- List]), 3125 ReturnList = Expanded ++ List1, 3126 if length(ReturnList) > ?DISJ_NORM_FORM_LIMIT -> throw(too_many_disj); 3127 true -> ReturnList 3128 end. 3129 3130is_simple_constraint(#constraint{}) -> true; 3131is_simple_constraint(#constraint_ref{}) -> true; 3132is_simple_constraint(#constraint_list{}) -> false. 3133 3134combine_conj_lists([List1, List2|Left], Prefix) -> 3135 NewList = [mk_conj_constraint_list([L1, L2]) || L1 <- List1, L2 <- List2], 3136 if length(NewList) > ?DISJ_NORM_FORM_LIMIT -> throw(too_many_disj); 3137 true -> ok 3138 end, 3139 combine_conj_lists([NewList|Left], Prefix); 3140combine_conj_lists([List], Prefix) -> 3141 [mk_conj_constraint_list([mk_conj_constraint_list(Prefix), L]) || L <- List]. 3142 3143calculate_deps(List) -> 3144 calculate_deps(List, []). 3145 3146calculate_deps([H|Tail], Acc) -> 3147 Deps = get_deps(H), 3148 calculate_deps(Tail, [Deps|Acc]); 3149calculate_deps([], []) -> []; 3150calculate_deps([], [L]) -> L; 3151calculate_deps([], Acc) -> 3152 lists:umerge(Acc). 3153 3154mk_conj_constraint_list(List) -> 3155 mk_constraint_list(conj, List). 3156 3157mk_disj_constraint_list([NotReallyAList]) -> 3158 NotReallyAList; 3159mk_disj_constraint_list(List) -> 3160 %% Make sure each element in the list is either a conjunction or a 3161 %% ref. Wrap single constraints into conjunctions. 3162 List1 = [wrap_simple_constr(C) || C <- List], 3163 mk_constraint_list(disj, List1). 3164 3165wrap_simple_constr(#constraint{} = C) -> mk_conj_constraint_list([C]); 3166wrap_simple_constr(#constraint_list{} = C) -> C; 3167wrap_simple_constr(#constraint_ref{} = C) -> C. 3168 3169enumerate_constraints(State) -> 3170 Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State))) 3171 || Id <- state__scc(State)], 3172 {_, _, NewState} = enumerate_constraints(Cs, 0, [], State), 3173 NewState. 3174 3175enumerate_constraints([#constraint_ref{id = Id} = C|Tail], N, Acc, State) -> 3176 Cs = state__get_cs(Id, State), 3177 {[NewCs], NewN, NewState1} = enumerate_constraints([Cs], N, [], State), 3178 NewState2 = state__store_constrs(Id, NewCs, NewState1), 3179 enumerate_constraints(Tail, NewN+1, [C|Acc], NewState2); 3180enumerate_constraints([#constraint_list{type = conj, list = List} = C|Tail], 3181 N, Acc, State) -> 3182 %% Separate the flat constraints from the deep ones to make a 3183 %% separate fixpoint iteration over the flat ones for speed. 3184 {Flat, Deep} = lists:partition(fun(#constraint{}) -> true; 3185 (#constraint_list{}) -> false; 3186 (#constraint_ref{}) -> false 3187 end, List), 3188 {NewFlat, N1, State1} = enumerate_constraints(Flat, N, [], State), 3189 {NewDeep, N2, State2} = enumerate_constraints(Deep, N1, [], State1), 3190 {NewList, N3} = 3191 if 3192 NewFlat =:= [] -> {NewDeep, N2}; 3193 NewDeep =:= [] -> {NewFlat, N2}; 3194 true -> 3195 TmpCList = mk_conj_constraint_list(NewFlat), 3196 {[TmpCList#constraint_list{id = {list, N2}}| NewDeep], 3197 N2 + 1} 3198 end, 3199 NewAcc = [C#constraint_list{list = NewList, id = {list, N3}}|Acc], 3200 enumerate_constraints(Tail, N3+1, NewAcc, State2); 3201enumerate_constraints([#constraint_list{list = List, type = disj} = C|Tail], 3202 N, Acc, State) -> 3203 {NewList, NewN, NewState} = enumerate_constraints(List, N, [], State), 3204 NewAcc = [C#constraint_list{list = NewList, id = {list, NewN}}|Acc], 3205 enumerate_constraints(Tail, NewN+1, NewAcc, NewState); 3206enumerate_constraints([#constraint{} = C|Tail], N, Acc, State) -> 3207 enumerate_constraints(Tail, N, [C|Acc], State); 3208enumerate_constraints([], N, Acc, State) -> 3209 {lists:reverse(Acc), N, State}. 3210 3211%% Put the fun ref constraints last in any conjunction since we need 3212%% to separate the environment from the interior of the function. 3213order_fun_constraints(State) -> 3214 Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State))) 3215 || Id <- state__scc(State)], 3216 order_fun_constraints(Cs, State). 3217 3218order_fun_constraints([#constraint_ref{id = Id}|Tail], State) -> 3219 Cs = state__get_cs(Id, State), 3220 {[Cs1], State1} = order_fun_constraints([Cs], [], [], State), 3221 NewCs = Cs1#constraint_list{deps = Cs#constraint_list.deps}, 3222 NewState = state__store_constrs(Id, NewCs, State1), 3223 order_fun_constraints(Tail, NewState); 3224order_fun_constraints([], State) -> 3225 State. 3226 3227order_fun_constraints([#constraint_ref{} = C|Tail], Funs, Acc, State) -> 3228 order_fun_constraints(Tail, [C|Funs], Acc, State); 3229order_fun_constraints([#constraint_list{list = List, 3230 type = Type, 3231 masks = OldMasks} = C|Tail], 3232 Funs, Acc, State) -> 3233 case OldMasks of 3234 undefined -> 3235 {NewList, NewState} = 3236 case Type of 3237 conj -> order_fun_constraints(List, [], [], State); 3238 disj -> 3239 FoldFun = fun(X, AccState) -> 3240 {[NewX], NewAccState} = 3241 order_fun_constraints([X], [], [], AccState), 3242 {NewX, NewAccState} 3243 end, 3244 lists:mapfoldl(FoldFun, State, List) 3245 end, 3246 NewList2 = reset_deps(NewList, State), 3247 C1 = update_constraint_list(C, NewList2), 3248 Masks = calculate_masks(NewList, 1, []), 3249 NewAcc = [update_masks(C1, Masks)|Acc], 3250 order_fun_constraints(Tail, Funs, NewAcc, NewState); 3251 M when is_map(M) -> 3252 order_fun_constraints(Tail, Funs, [C|Acc], State) 3253 end; 3254order_fun_constraints([#constraint{} = C|Tail], Funs, Acc, State) -> 3255 order_fun_constraints(Tail, Funs, [C|Acc], State); 3256order_fun_constraints([], Funs, Acc, State) -> 3257 NewState = order_fun_constraints(Funs, State), 3258 {lists:reverse(Acc)++Funs, NewState}. 3259 3260update_masks(C, Masks) -> 3261 C#constraint_list{masks = Masks}. 3262 3263reset_deps(ConstrList, #state{solvers = Solvers}) -> 3264 case lists:member(v1, Solvers) of 3265 true -> 3266 ConstrList; 3267 false -> 3268 [reset_deps(Constr) || Constr <- ConstrList] 3269 end. 3270 3271reset_deps(#constraint{}=C) -> C#constraint{deps = []}; 3272reset_deps(#constraint_list{}=C) -> C#constraint_list{deps = []}; 3273reset_deps(#constraint_ref{}=C) -> C#constraint_ref{deps = []}. 3274 3275calculate_masks([C|Cs], I, L0) -> 3276 calculate_masks(Cs, I+1, [{V, I} || V <- get_deps(C)] ++ L0); 3277calculate_masks([], _I, L) -> 3278 M = family(L), 3279 maps:from_list(M). 3280 3281%% ============================================================================ 3282%% 3283%% Utilities. 3284%% 3285%% ============================================================================ 3286 3287bif_return(M, F, A, Xs) -> 3288 erl_bif_types:type(M, F, A, Xs). 3289 3290is_singleton_non_number_type(Type) -> 3291 case t_is_number(Type) of 3292 true -> false; 3293 false -> is_singleton_type(Type) 3294 end. 3295 3296is_singleton_type(Type) -> 3297 case t_is_atom(Type) of 3298 true -> 3299 case t_atom_vals(Type) of 3300 unknown -> false; 3301 [_] -> true; 3302 [_|_] -> false 3303 end; 3304 false -> 3305 case t_is_integer(Type) of 3306 true -> 3307 case t_number_vals(Type) of 3308 unknown -> false; 3309 [_] -> true; 3310 [_|_] -> false 3311 end; 3312 false -> 3313 t_is_nil(Type) 3314 end 3315 end. 3316 3317find_element(Args, Cs) -> 3318 [Pos, Tuple] = Args, 3319 case t_is_number(Pos) of 3320 true -> 3321 case erl_types:t_number_vals(Pos) of 3322 'unknown' -> 'unknown'; 3323 [I] -> 3324 case find_constraint(Tuple, Cs) of 3325 'unknown' -> 'unknown'; 3326 #constraint{lhs = ExTuple} -> 3327 case erl_types:t_is_tuple(ExTuple) of 3328 true -> 3329 Elems = erl_types:t_tuple_args(ExTuple), 3330 Elem = lists:nth(I, Elems), 3331 case erl_types:t_is_var(Elem) of 3332 true -> Elem; 3333 false -> 'unknown' 3334 end; 3335 false -> 'unknown' 3336 end 3337 end; 3338 _ -> 'unknown' 3339 end; 3340 false -> 'unknown' 3341 end. 3342 3343find_constraint(_Tuple, []) -> 3344 'unknown'; 3345find_constraint(Tuple, [#constraint{op = 'eq', rhs = Tuple} = C|_]) -> 3346 C; 3347find_constraint(Tuple, [#constraint_list{list = List}|Cs]) -> 3348 find_constraint(Tuple, List ++ Cs); 3349find_constraint(Tuple, [_|Cs]) -> 3350 find_constraint(Tuple, Cs). 3351 3352-spec fold_literal_maybe_match(cerl:cerl(), state()) -> cerl:cerl(). 3353 3354fold_literal_maybe_match(Tree0, State) -> 3355 Tree1 = cerl:fold_literal(Tree0), 3356 case state__is_in_match(State) of 3357 false -> Tree1; 3358 true -> dialyzer_utils:refold_pattern(Tree1) 3359 end. 3360 3361lookup_record(State, Tag, Arity) -> 3362 #state{module = M, mod_records = ModRecs, cserver = CServer} = State, 3363 {State1, Rec} = 3364 case lists:keyfind(M, 1, ModRecs) of 3365 {M, Rec0} -> 3366 {State, Rec0}; 3367 false -> 3368 Rec0 = dialyzer_codeserver:lookup_mod_records(M, CServer), 3369 NewModRecs = [{M, Rec0}|ModRecs], 3370 {State#state{mod_records = NewModRecs}, Rec0} 3371 end, 3372 case erl_types:lookup_record(Tag, Arity, Rec) of 3373 {ok, Fields} -> 3374 RecType = 3375 t_tuple([t_from_term(Tag)| 3376 [FieldType || {_FieldName, _Abstr, FieldType} <- Fields]]), 3377 {ok, RecType, State1}; 3378 error -> 3379 {error, State1} 3380 end. 3381 3382is_literal_record(Tree) -> 3383 Ann = cerl:get_ann(Tree), 3384 lists:member(record, Ann). 3385 3386family(L) -> 3387 dialyzer_utils:family(L). 3388 3389%% ============================================================================ 3390%% 3391%% Pretty printer and debug facilities. 3392%% 3393%% ============================================================================ 3394 3395-ifdef(DEBUG_CONSTRAINTS). 3396-ifndef(DEBUG). 3397-define(DEBUG, true). 3398-endif. 3399-endif. 3400 3401-ifdef(DEBUG). 3402format_type(#fun_var{deps = Deps, origin = Origin}) -> 3403 L = [format_type(t_var(X)) || X <- Deps], 3404 io_lib:format("Fun@L~p(~ts)", [Origin, join_chars(L, ",")]); 3405format_type(Type) -> 3406 case cerl:is_literal(Type) of 3407 true -> io_lib:format("~tw", [cerl:concrete(Type)]); 3408 false -> erl_types:t_to_string(Type) 3409 end. 3410 3411join_chars([], _Sep) -> 3412 []; 3413join_chars([H|T], Sep) -> 3414 [H|[[Sep,X] || X <- T]]. 3415 3416debug_lookup_name(Var) -> 3417 case maps:find(t_var_name(Var), get(dialyzer_typesig_map)) of 3418 error -> Var; 3419 {ok, Name} -> Name 3420 end. 3421-endif. 3422 3423-ifdef(DEBUG_NAME_MAP). 3424debug_make_name_map(Vars, Funs) -> 3425 Map = get(dialyzer_typesig_map), 3426 NewMap = 3427 if Map =:= undefined -> debug_make_name_map(Vars, Funs, maps:new()); 3428 true -> debug_make_name_map(Vars, Funs, Map) 3429 end, 3430 put(dialyzer_typesig_map, NewMap). 3431 3432debug_make_name_map([Var|VarLeft], [Fun|FunLeft], Map) -> 3433 Name = {cerl:fname_id(Var), cerl:fname_arity(Var)}, 3434 FunLabel = cerl_trees:get_label(Fun), 3435 debug_make_name_map(VarLeft, FunLeft, maps:put(FunLabel, Name, Map)); 3436debug_make_name_map([], [], Map) -> 3437 Map. 3438 3439-else. 3440debug_make_name_map(_Vars, _Funs) -> 3441 ok. 3442-endif. 3443 3444-ifdef(DEBUG_CONSTRAINTS). 3445pp_constrs_scc(SCC, State) -> 3446 [pp_constrs(Fun, state__get_cs(Fun, State), State) || Fun <- SCC]. 3447 3448pp_constrs(Fun, Cs, State) -> 3449 io:format("Constraints for fun: ~tw", [debug_lookup_name(Fun)]), 3450 MaxDepth = pp_constraints(Cs, State), 3451 io:format("Depth: ~w\n", [MaxDepth]). 3452 3453pp_constraints(Cs, State) -> 3454 Res = pp_constraints([Cs], 0, 0, State), 3455 io:nl(), 3456 Res. 3457 3458pp_constraints([List|Tail], Level, MaxDepth, State) when is_list(List) -> 3459 pp_constraints(List++Tail, Level, MaxDepth, State); 3460pp_constraints([#constraint_ref{id = Id}|Left], Level, MaxDepth, State) -> 3461 Cs = state__get_cs(Id, State), 3462 pp_indent(Level), 3463 io:format("%Ref ~w%", [t_var_name(Id)]), 3464 pp_constraints([Cs|Left], Level, MaxDepth, State); 3465pp_constraints([#constraint{}=C], Level, MaxDepth, _State) -> 3466 pp_op(C, Level), 3467 erlang:max(Level, MaxDepth); 3468pp_constraints([#constraint{}=C|Tail], Level, MaxDepth, State) -> 3469 pp_op(C, Level), 3470 pp_constraints(Tail, Level, MaxDepth, State); 3471pp_constraints([#constraint_list{type = Type, list = List, id = Id}|Tail], 3472 Level, MaxDepth, State) -> 3473 pp_indent(Level), 3474 case Type of 3475 conj -> io:format("Conj ~w (", [Id]); 3476 disj -> io:format("Disj ~w (", [Id]) 3477 end, 3478 NewMaxDepth = pp_constraints(List, Level+1, MaxDepth, State), 3479 io:format(")"), 3480 case Tail =:= [] of 3481 true -> NewMaxDepth + 1; 3482 false -> pp_constraints(Tail, Level, NewMaxDepth, State) 3483 end. 3484 3485pp_op(#constraint{lhs = Lhs, op = Op, rhs = Rhs}, Level) -> 3486 pp_indent(Level), 3487 io:format("~ts ~w ~ts", [format_type(Lhs), Op, format_type(Rhs)]). 3488 3489pp_indent(Level) -> 3490 io:format("\n~*s", [Level*2, ""]). 3491-else. 3492pp_constrs_scc(_SCC, _State) -> 3493 ok. 3494-endif. 3495 3496-ifdef(TO_DOT). 3497 3498constraints_to_dot_scc(SCC, State) -> 3499 %% TODO: handle Unicode names. 3500 io:format("SCC: ~tp\n", [SCC]), 3501 Name = lists:flatten([format_lookup_name(debug_lookup_name(Fun)) 3502 || Fun <- SCC]), 3503 Cs = [state__get_cs(Fun, State) || Fun <- SCC], 3504 constraints_to_dot(Cs, Name, State). 3505 3506format_lookup_name({FunName, Arity}) -> 3507 TupleS = io_lib:format("{~ts,~w}", [atom_to_list(FunName), Arity]), 3508 io_lib:format("~tw", [list_to_atom(lists:flatten(TupleS))]). 3509 3510constraints_to_dot(Cs0, Name, State) -> 3511 NofCs = length(Cs0), 3512 Cs = lists:zip(lists:seq(1, NofCs), Cs0), 3513 {Graph, Opts, _N} = constraints_to_nodes(Cs, NofCs + 1, 1, [], [], State), 3514 dialyzer_dot:translate_list(Graph, "/tmp/cs.dot", "foo", Opts), 3515 %% "-T ps" works for Latin-1. dialyzer_dot cannot handle UTF-8 either. 3516 Res = os:cmd("dot -o /tmp/"++ Name ++ ".ps -T ps /tmp/cs.dot"), 3517 io:format("Res: ~ts~n", [Res]), 3518 ok. 3519 3520constraints_to_nodes([{Name, #constraint_list{type = Type, list = List, id=Id}} 3521 |Left], N, Level, Graph, Opts, State) -> 3522 N1 = N + length(List), 3523 NewList = lists:zip(lists:seq(N, N1 - 1), List), 3524 Names = [SubName || {SubName, _C} <- NewList], 3525 Edges = [{Name, SubName} || SubName <- Names], 3526 ThisNode = [{Name, Opt} || Opt <- [{label, 3527 lists:flatten(io_lib:format("~w", [Id]))}, 3528 {shape, get_shape(Type)}, 3529 {level, Level}]], 3530 {NewGraph, NewOpts, N2} = constraints_to_nodes(NewList, N1, Level+1, 3531 [Edges|Graph], 3532 [ThisNode|Opts], State), 3533 constraints_to_nodes(Left, N2, Level, NewGraph, NewOpts, State); 3534constraints_to_nodes([{Name, #constraint{lhs = Lhs, op = Op, rhs = Rhs}}|Left], 3535 N, Level, Graph, Opts, State) -> 3536 Label = lists:flatten(io_lib:format("~ts ~w ~ts", 3537 [format_type(Lhs), Op, 3538 format_type(Rhs)])), 3539 ThisNode = [{Name, Opt} || Opt <- [{label, Label}, {level, Level}]], 3540 NewOpts = [ThisNode|Opts], 3541 constraints_to_nodes(Left, N, Level, Graph, NewOpts, State); 3542constraints_to_nodes([{Name, #constraint_ref{id = Id0}}|Left], 3543 N, Level, Graph, Opts, State) -> 3544 Id = debug_lookup_name(Id0), 3545 CList = state__get_cs(Id0, State), 3546 ThisNode = [{Name, Opt} || Opt <- [{label, 3547 lists:flatten(io_lib:format("~w", [Id]))}, 3548 {shape, ellipse}, 3549 {level, Level}]], 3550 NewList = [{N, CList}], 3551 {NewGraph, NewOpts, N1} = constraints_to_nodes(NewList, N + 1, Level + 1, 3552 [{Name, N}|Graph], 3553 [ThisNode|Opts], State), 3554 constraints_to_nodes(Left, N1, Level, NewGraph, NewOpts, State); 3555constraints_to_nodes([], N, _Level, Graph, Opts, _State) -> 3556 {lists:flatten(Graph), lists:flatten(Opts), N}. 3557 3558get_shape(conj) -> box; 3559get_shape(disj) -> diamond. 3560 3561-else. 3562constraints_to_dot_scc(_SCC, _State) -> 3563 ok. 3564-endif. 3565