-
Notifications
You must be signed in to change notification settings - Fork 44
/
Copy pathnodes.lkt
25189 lines (22701 loc) · 906 KB
/
nodes.lkt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import parser
import tokens
dynvar env: LexicalEnv
|" Origin for this property's request. See :ref:`The origin parameter` for more
|" details
dynvar origin: AdaNode
dynvar no_visibility: Bool
dynvar include_ud_indexing: Bool
dynvar dottable_type: AdaNode
dynvar imprecise_fallback: Bool
dynvar entry_point: AdaNode
|" Kind for the result of a cross reference operation.
|"
|" - ``no_ref`` is for no reference, it is the null value for this enum.
|" - ``precise`` is when the reference result is precise.
|" - ``imprecise`` is when there was an error computing the precise result,
|" and a result was gotten in an imprecise fashion.
|" - ``error`` is for unrecoverable errors (either there is no imprecise path
|" for the request you made, or the imprecise path errored out too).
@with_default(no_ref)
enum RefResultKind {
case no_ref, precise, imprecise, error
}
|" Kind of CallExpr type.
|"
|" - ``call`` is when the CallExpr is a procedure or function call.
|" - ``array_slice``, ``array_index`` is when the CallExpr is in fact an
|" array slice or an array subcomponent access expression, respectively.
|" - ``type_conversion`` is when the CallExpr is a type conversion.
|" - ``family_index`` is for entry calls using a family index.
enum CallExprKind {
case call, array_slice, array_index, type_conversion, family_index
}
|" Root node class for the Ada syntax tree.
@abstract
@generic_list_type("AdaList")
class AdaNode implements Node[AdaNode] {
@external()
fun can_reach(from_node: AdaNode): Bool
|" Return the scope of definition of this basic declaration.
@exported
fun declarative_scope(): DeclarativePart =
node.parents().find((p) => p is DeclarativePart).as[DeclarativePart]
|" Return the kind of the compilation unit owning this node.
fun owning_unit_kind(): AnalysisUnitKind =
node.unit.root.as![CompilationUnit].unit_kind()
|" Static method helper. Fetch the unit designated by unit_name. Return
|" the compilation unit node.
|"
|" This is designed in a way that will emit a
|" ``unit_requested(not_found_is_error=True, ...)`` event when not
|" finding the unit is supposed to be an error within Ada semantics.
fun withed_unit_helper(unit_name: Name): CompilationUnit = {
# Try to fetch the spec and the body for ``unit_name``, but do not emit
# a unit_requested event yet.
val unit_name_array = unit_name.as_symbol_array();
val spec =
node.designated_compilation_unit(
unit_name_array,
kind=AnalysisUnitKind.unit_specification,
not_found_is_error=false
);
val body =
if spec.is_null
then
node.designated_compilation_unit(
unit_name_array,
kind=AnalysisUnitKind.unit_body,
not_found_is_error=false
)
else null[CompilationUnit];
# Emit an event if one missing unit is actually required by Ada's
# semantics: either when we have a package body but got no spec, or
# when we have no body and no spec.
val _ =
if
(body.do((v1) => v1.decl() is PackageBody) and spec.is_null)
or (spec.is_null and body.is_null)
then
node.designated_compilation_unit(
unit_name_array,
kind=AnalysisUnitKind.unit_specification,
not_found_is_error=true
)
else null[CompilationUnit];
# Return the requested unit (the spec takes precedence)
spec or? body
}
fun is_contract_aspect(name: Symbol): Bool =
name in s"Pre"
| s"Pre'Class"
| s"Post"
| s"Post'Class"
| s"Refined_Post"
| s"Precondition"
| s"Postcondition"
| s"Precondition'Class"
| s"Postcondition'Class"
| s"Invariant"
| s"Invariant'Class"
| s"Type_Invariant"
| s"Type_Invariant'Class"
| s"Predicate"
| s"Static_Predicate"
| s"Dynamic_Predicate"
| s"Default_Initial_Condition"
| s"Initial_Condition"
| s"Contract_Cases"
| s"Test_Case"
| s"Global"
| s"Refined_Global"
| s"Refined_State"
| s"Stable_Properties"
| s"Depends"
| s"Refined_Depends"
| s"Predicate_Failure"
| s"SPARK_Mode"
|" Return True if the given ``name`` is that of an Ada aspect in which
|" references can designate entities declared *after* the entity on which
|" this aspect is defined.
fun aspect_has_forward_visibility(name: Symbol): Bool =
node.is_contract_aspect(name)
or name in s"Iterator_Element" | s"Default_Iterator"
fun in_aspect_with_forward_visibility(): Bool =
not node.parents().find(
(p) =>
p.as[AspectAssoc].do(
(a) =>
node.aspect_has_forward_visibility(
a.id.as_bare_entity.name_symbol()
)
)
or? p.as[Pragma].do(
(p) =>
node.aspect_has_forward_visibility(
p.id.as_bare_entity.name_symbol()
)
)
)
.is_null
|" Return whether self is contained by an aspect whose name is ``name``.
fun in_aspect(name: Symbol): Bool =
node.parents().any(
(p) => p.as[AspectAssoc].do((a) => a.id.name_is(name))
)
fun empty_env(): LexicalEnv =
node.parents().find((p) => p is CompilationUnit)
.as[CompilationUnit]
.get_empty_env()
|" Return True iff this node is not null.
fun is_not_null(): Bool =
# TODO: Remove this once we have better logic predicates: it is
# currently not possible to pass an arbitrary DSL expression to a
# predicate, so we must have a property for every expression that we
# might want to pass to a predicate.
not self.is_null
|" Static method. Evaluate the bounds of ``dr``.
fun eval_discrete_range(dr: DiscreteRange): EvalDiscreteRange =
if dr == null[DiscreteRange]
then
raise[EvalDiscreteRange] PreconditionFailure(
"Attempting to evaluate a null discrete range"
)
else
EvalDiscreteRange(
low_bound=dr.low_bound.do(
(lb) => lb.eval_as_int(),
default_val=0b
),
high_bound=dr.high_bound.eval_as_int()
)
|" Static method. Return the array of symbols joined by separator ``sep``.
fun sym_join(syms: Array[Symbol], sep: String): String =
sep.join(syms.map((s) => s.image()))
|" Return the compilation unit containing this node.
|"
|" .. note:: This returns the :typeref:`CompilationUnit` node, which is
|" different from the ``AnalysisUnit``. In particular, an analysis unit
|" can contain multiple compilation units.
@exported
fun enclosing_compilation_unit(): CompilationUnit =
node.parents().find((n) => n is CompilationUnit).as![CompilationUnit]
|" Static property. Will return True if current_env is a children of
|" parent.
fun is_children_env(parent: LexicalEnv, current_env: LexicalEnv): Bool =
if parent == null[LexicalEnv] then false
elif current_env == parent then true
elif current_env.is_null then false
else node.is_children_env(parent, current_env.env_parent)
|" Return self with an empty metadata field.
fun without_md(): Entity[AdaNode] =
Entity[AdaNode](
node=self.node,
info=EntityInfo(
md=null[Metadata],
rebindings=self.info.rebindings,
from_rebound=self.info.from_rebound
)
)
|" Assuming this node comes from an instantiated generic declaration,
|" return its non-instantiated counterpart lying in the generic
|" declaration.
@exported
fun get_uninstantiated_node(): Entity[AdaNode] = node.as_bare_entity
|" Return possible completions at this point in the file.
@exported
fun complete(): Iterator[CompletionItem] = {
bind origin = node.origin_node();
self.complete_items().filter(
# This property filters out `SyntheticSubpDecl` and
# `SyntheticObjectDecl` items because they are of no use for
# completion. This is not entirely true for `SyntheticObjectDecl`
# since they can be useful in type predicate aspects (yet not
# implemented since no likely helpful). Additional filtering can be
# done in `complete_items`.
(n) => not n.decl is SyntheticSubpDecl | SyntheticObjectDecl
)
.to_iterator()
}
|" Specialization of ``complete_item_weight``.
|"
|" Set the weight according to the type of the ``item``'s return value in
|" comparison to the type of the declaration designated by ``name``.
@with_dynvars(origin)
fun complete_item_weight_matching_type(
item: Entity[BasicDecl],
name: Entity[Name]
): Int = {
val te_not_null = not item.type_expression().is_null;
val td = item.type_expression()?.designated_type_decl();
# Promote declarations that returns a value
item.expr_type().do(
(_) =>
# Return value type of item matches name's type
if (
name.referenced_decl()?.type_expression()
?.designated_type_decl()
.matching_assign_type(td)
and te_not_null
)
then 100
# Re-try with best-effort resolution (for incomplete code)
elif {
bind imprecise_fallback = true;
name.referenced_decl()?.type_expression()
?.designated_type_decl()
.matching_assign_type(td)
and te_not_null
} then 70
# Types don't match but item returns a value
else 50,
default_val=0
)
}
|" Return the list of keywords that are valid at this point in the file.
|"
|" .. note::
|" This is work in progress. It will return all keywords for now,
|" without looking at the context.
@exported
fun valid_keywords(): Array[Symbol] =
[
s"abort",
s"abs",
s"abstract",
s"accept",
s"access",
s"aliased",
s"all",
s"and",
s"array",
s"at",
s"begin",
s"body",
s"case",
s"constant",
s"declare",
s"delay",
s"delta",
s"digits",
s"do",
s"else",
s"elsif",
s"end",
s"entry",
s"exception",
s"exit",
s"for",
s"function",
s"generic",
s"goto",
s"if",
s"in",
s"interface",
s"is",
s"limited",
s"loop",
s"mod",
s"new",
s"not",
s"null",
s"others",
s"out",
s"of",
s"or",
s"overriding",
s"package",
s"pragma",
s"private",
s"procedure",
s"protected",
s"raise",
s"range",
s"record",
s"rem",
s"renames",
s"requeue",
s"return",
s"reverse",
s"select",
s"separate",
s"some",
s"subtype",
s"synchronized",
s"tagged",
s"task",
s"terminate",
s"then",
s"type",
s"until",
s"use",
s"when",
s"while",
s"with",
s"xor"
]
|" Assuming that self is the error location of a semantic diagnostic and
|" that ``ctx`` is one of its logic contexts indicating which subprogram
|" was tried, return a node that indicates with more precision which part
|" of the subprogram caused a mismatch. For example, if self corresponds
|" to the second actual in the ``CallExpr``, this returns the second
|" parameter of the candidate subprogram.
@ignored
fun call_context(ctx: LogicContext): AdaNode = {
val bd = ctx.decl_node.as[BasicDecl];
bd?.subp_spec_or_null().do(
(spec) =>
ctx.ref_node.as[Name]?.parent_callexpr().do(
(ce) =>
if node == ce.node then spec.returns().node
else
node.match_formals(
spec.abstract_formal_params(),
ce.params(),
bd.info.md.dottable_subp
)
.find((pm) => pm.actual.assoc.expr().node == node)
.do(
(pm) => pm.formal.formal_decl().type_expression().node,
default_val=bd.defining_name().node
),
default_val=bd.defining_name().node
),
default_val=ctx.decl_node.node
)
}
|" Return the potentially empty list of generic package/subprogram
|" instantiations that led to the creation of this entity. Outer-most
|" instantiations appear last.
@exported
fun generic_instantiations(): Array[Entity[GenericInstantiation]] =
node.generic_instantiations_internal(self.info.rebindings)
fun generic_instantiations_internal(
r: EnvRebindings
): Array[Entity[GenericInstantiation]] =
if r == null[EnvRebindings]
then null[Array[Entity[GenericInstantiation]]]
else {
val head = (
r.new_env.env_node.as![GenericInstantiation].as_bare_entity
);
val tail = node.generic_instantiations_internal(r.get_parent);
[head] & tail
}
|" If the rebindings in ``base`` end with ``suffix``, ``base`` is
|" returned without it. Otherwise ``base`` is returned as-is.
fun remove_rebindings(
base: EnvRebindings,
suffix: EnvRebindings
): EnvRebindings =
if base.is_null or suffix.is_null then base
elif base.old_env == suffix.old_env and base.new_env == suffix.new_env
then node.remove_rebindings(base.get_parent, suffix.get_parent)
else base
|" Append a new entry ``old_env -> new_env`` to ``base``. This also takes
|" care of collapsing a subset of the rebindings if ``new_env`` is
|" actually inside an envinonment which is rebound by an existing entry.
|" In other words, this collapses generic formal package instantiations
|" done in a generic context where the actual package is known.
|" For example in the following snippet:
|"
|" .. code:: ada
|"
|" generic
|" package Interface_G is
|" end Interface_G;
|"
|" generic
|" with package I is new Interface_G (<>);
|" package Pkg_G is
|" end Pkg_G;
|"
|" package My_Interface is new Interface_G;
|" package My_Pkg is new Pkg_G (My_Interface);
|"
|" Navigating inside ``My_Pkg`` leads us in ``Pkg_G`` with rebindings
|" ``[My_Pkg]``. From here, navigating inside the instantiation of the
|" formal package ``I`` would lead us in ``Interface_G`` with rebindings
|" ``[My_Pkg, I]``. However, ``add_rebinding`` sees that ``I`` is
|" rebound by the instantiation of ``My_Pkg`` and therefore collapses
|" the two rebindings from ``[My_Pkg, I]`` to ``[My_Interface]``.
fun add_rebinding(
base: EnvRebindings,
old_env: LexicalEnv,
new_env: LexicalEnv
): EnvRebindings = {
val parent_env = new_env.env_node.node_env;
if (
base.is_null or not parent_env.env_node is GenericDecl
or not node.is_rebound(base, parent_env)
)
then base.append_rebinding(old_env, new_env)
elif base.old_env == parent_env
then
base.new_env.get_first(
new_env
.env_node
.as[GenericPackageInstantiation]
.name
.name_symbol(),
lookup=LookupKind.minimal
)
.as[GenericPackageInstantiation]
.do(
(gpi) => {
val gen_env =
gpi.nonbound_generic_decl_from_self()
.node
.children_env;
val info =
EntityInfo(
md=null[Metadata],
rebindings=node.add_rebinding(
base.get_parent,
gen_env,
gpi.instantiation_env
),
from_rebound=false
);
# Collapsing may make some entries irrelevant, so shed
# rebindings at this point to remove those.
gen_env.shed_rebindings(info).rebindings
},
default_val=base.append_rebinding(old_env, new_env)
)
else node.add_rebinding(base.get_parent, old_env, new_env)
}
|" Return whether ``old_env`` is rebound somewhere inside the given
|" rebindings.
fun is_rebound(base: EnvRebindings, old_env: LexicalEnv): Bool =
not base.is_null
and (
base.old_env == old_env
or node.is_rebound(base.get_parent, old_env)
)
|" Append rebindings from ``to_insert`` to ``base``, stopping as soon as
|" an entry from ``to_insert`` is already rebound in ``base``, such that
|" for example ``insert_rebindings([A, C], [B, C, D]) = [A, C, D]``.
fun insert_rebindings(
base: EnvRebindings,
to_insert: EnvRebindings
): EnvRebindings =
if to_insert.is_null then base
elif base.is_null then to_insert
elif node.is_rebound(base, to_insert.old_env) then base
else
node.add_rebinding(
node.insert_rebindings(base, to_insert.get_parent),
to_insert.old_env,
to_insert.new_env
)
|" Return whether ``parent`` is a parent of ``base``. This considers
|" the chain as a whole, i.e. ``has_parent_rebindings([A, B, C], [A, B])``
|" returns True, but both ``has_parent_rebindings([A, B, C], [B, C])`` as
|" well as ``has_parent_rebindings([A, C], [A, B])`` return False.
fun has_parent_rebindings(
base: EnvRebindings,
parent: EnvRebindings
): Bool =
base == parent or parent.is_null
or (
not base.is_null
and node.has_parent_rebindings(base.get_parent, parent)
)
# We mark this property as memoizable because for the moment, we only ever
# get the first result of logic resolution, so we only ever want the result
# of the first evaluation of this property. When we change that, we'll
# probably change the solving API anyway.
@call_memoizable
fun logic_val(
from_node: Entity[AdaNode],
lvar: LogicVar
): LogicValResult = {
val success = from_node.resolve_names_from_closest_entry_point();
LogicValResult(
success=success,
value=if success then lvar.get_value() else null[Entity[AdaNode]]
)
}
fun semantic_parent_helper(env: LexicalEnv): Entity[AdaNode] =
env.do(
(env) =>
env.env_node.as_entity
or? self.semantic_parent_helper(env.env_parent)
)
|" Return the semantic parent for this node, if applicable, null
|" otherwise.
|"
|" .. note:: A node lying outside of a library item's declaration or
|" subunit's body does not have a parent environment, meaning that
|" this property will return null.
@exported
fun semantic_parent(): Entity[AdaNode] =
self.semantic_parent_helper(self.node_env)
|" Recursively call ``semantic_parent`` to get all the semantic parents
|" of this node.
fun semantic_parents(): Array[Entity[AdaNode]] =
self.semantic_parent().do((sp) => [sp] & sp.semantic_parents())
|" Return the parent basic decl for this node, if applicable, null
|" otherwise.
|"
|" .. note:: If the parent BasicDecl of the given node is a generic
|" declaration, this call will return the instantiation from which
|" the node was retrieved instead, if any. This also applies to bodies
|" of generic declarations.
|"
|" .. note:: When called on a subunit's body, this property will return
|" its corresponding body stub.
|"
|" .. note:: When called on a node lying outside of a library item's
|" declaration or subunit's body this property will return null.
@exported
fun parent_basic_decl(): Entity[BasicDecl] =
# On synthetic types that are rooted in their parents, we want to
# call parent_basic_decl on the parent type, to avoid getting the
# type itself as a parent_basic_decl (since some types introduce a
# scope).
if
self is ClasswideTypeDecl
| DiscreteBaseSubtypeDecl
| SynthAnonymousTypeDecl
| SyntheticSubpDecl
then
self.parents(with_self=false).find(
(p) => p is BasicDecl
).parent_basic_decl()
else {
val gen_decl = self.as[GenericDecl];
val gen_body =
self.as[Body]?.decl_part().do(
(dp) => dp.as[GenericDecl] or? dp.parent.as[GenericDecl]
);
(gen_decl or? gen_body).do((gd) => gd.decl().get_instantiation())
or? self.semantic_parent().do(
(sp) =>
if sp is GenericSubpInternal | GenericPackageInternal
then sp.parent_basic_decl()
else sp.as[BasicDecl] or? sp.parent_basic_decl()
)
}
|" Helper for the properties ``has_spark_mode_on`` and
|" ``is_subject_to_proof``.
|"
|" This property will determine if the decl or body has SPARK mode on,
|" with some special paths for bodies.
|"
|" It will also, for bodies only, determine whether there are
|" ``Skip_Proof`` or ``Skip_Flow_And_Proof`` annotations, if the parameter
|" ``include_skip_proof_annotations`` is True.
fun is_spark_impl(include_skip_proof_annotations: Bool): Bool = {
val spark_mode = self.spark_mode_aspect();
# For bodies, and if `include_skip_proof_annotations` is True,
# check `Skip_Proof`/`Skip_Flow_And_Proof`.
if (
include_skip_proof_annotations
and not self.as[Body].do(
(b) => b,
default_val=self.semantic_parents().find((n) => n is Body)
.as[Body]
)
.do(
(b) =>
b.gnatprove_annotations().find(
(a) =>
a.as[Name].name_symbol() in s"Skip_Proof"
| s"Skip_Flow_And_Proof"
)
)
.is_null
)
then false
elif not spark_mode.exists then false
else
spark_mode.value.do(
(mode) => mode.as[Name].name_is(s"On"),
# `SPARK_Mode` without value is `On` by default
default_val=true
)
}
|" Returns whether this subprogram has explicitly been set as having
|" ``Spark_Mode`` to ``On``, directly or indirectly.
|"
|" Doesn't include subprograms that can be inferred by GNATprove as being
|" SPARK.
@exported
fun has_spark_mode_on(): Bool = self.is_spark_impl(false)
|" Returns whether this subprogram body is subject to proof in the context
|" of the SPARK/GNATprove tools.
@exported
fun is_subject_to_proof(): Bool = self.is_spark_impl(true)
# TODO (S917-027): re-enable this protection or remove it once we
# moved forward on memoization soundness issues in Langkit.
# This comment was associated with the following previous libadalang DSL::
# call_non_memoizable_because=(
# None and
# 'Getting an analysis unit cannot appear in a memoized context'
# )
|" Return the analysis unit for the given ``kind`` corresponding to this
|" Name. Return null if ``load_if_needed`` is false and the unit is not
|" loaded yet.
|"
|" For nested library units, this will trigger the processing of parent
|" library units, so for example, if you ``get_unit('A.B.C')``, this will
|" load units ``A.B.C``, ``A.B`` and ``A``, except if ``process_parents``
|" is False.
|"
|" ``not_found_is_error`` will condition the parameter of the same name in
|" the ``Unit_Requested`` callback. The client of ``get_unit`` is supposed
|" to pass ``True`` if the unit not being found is an error in the Ada
|" sense.
@external()
fun get_unit(
name: Array[Symbol],
kind: AnalysisUnitKind,
load_if_needed: Bool,
not_found_is_error: Bool,
process_parents: Bool = true
): AnalysisUnit
|" Fetch the compilation unit designated by the given name defined in an
|" analysis unit of the given kind.
fun designated_compilation_unit(
name: Array[Symbol],
kind: AnalysisUnitKind,
load_if_needed: Bool = true,
not_found_is_error: Bool = true,
process_parents: Bool = true
): CompilationUnit = {
val designated_analysis_unit =
node.get_unit(
name,
kind,
load_if_needed,
not_found_is_error,
process_parents
);
node.compilation_unit_with_name(designated_analysis_unit, name)
}
|" Helper for ``designated_compilation_unit``. From a given analysis unit,
|" that might contain several compilation units, and a name, return the
|" corresponding compilation unit.
fun compilation_unit_with_name(
unit: AnalysisUnit,
name: Array[Symbol]
): CompilationUnit =
unit?.root.do(
(v1) =>
match v1 {
# If the root of the analysis unit is a single compilation
# unit, it is necessarily the one we look for.
case single: CompilationUnit => single
# If the root of the analysis unit comprises multiple
# compilation units, look for the one with a matching fully
# qualified name.
case multi: ASTList[CompilationUnit] =>
multi.find(
(c) => c.syntactic_fully_qualified_name() == name
)
# If the root is a PragmaNodeList (`pragma No_Body` case),
# there is no compilation unit for `name`.
case _: ASTList[Pragma] => null[CompilationUnit]
case _ =>
raise[CompilationUnit] PropertyError(
"Unexpected analysis unit root"
)
}
)
|" If the corresponding analysis unit is loaded, return the root decl
|" node for the given analysis unit ``kind`` and corresponding to the
|" name ``name``. If it's not loaded, return none.
fun get_unit_root_decl(
name: Array[Symbol],
kind: AnalysisUnitKind,
load_if_needed: Bool = true,
not_found_is_error: Bool = true,
process_parents: Bool = true
): BasicDecl = {
val cu =
node.designated_compilation_unit(
name,
kind,
load_if_needed,
not_found_is_error,
process_parents
);
cu?.decl()
}
|" Filters out among the list of given units those that cannot refer to
|" the unit in which this node lies. If transitive is True, the whole
|" transitive closure of imports will be used to find a reference to the
|" unit of this node.
@exported
@external()
fun filter_is_imported_by(
units: Array[AnalysisUnit],
transitive: Bool
): Array[AnalysisUnit]
|" Return the environment to bind initially during the construction of the
|" xref equation for this node. Note that this only makes sense if this
|" node is an xref entry point.
fun xref_initial_env(): LexicalEnv = self.children_env
|" This property can be used when an xref_equation needs to bind one of
|" self's logic vars (given in ``dest``) to one of ``outer_node``'s logic
|" vars given in ``node_var``, when ``outer_node`` is a node that is not a
|" children of self. Indeed, due to the stop_resolution mechanism, binding
|" to such a variable directly may not have the expected effect: if there
|" is a "stop_resolution" boundary between the current node and the outer
|" node, then the outer node's variable already has a value when we
|" construct the current node's equation, hence using it in an equation
|" will reset its content instead of binding to its value. This property
|" basically checks whether this is the case or not in order to create an
|" equation that either assigns ``dest`` to the known value or that binds
|" it to the given variable.
@with_dynvars(entry_point)
fun bind_to_non_local(
dest: LogicVar,
outer_node: AdaNode,
node_var: LogicVar
): Equation =
if outer_node.parents().contains(entry_point) then dest <-> node_var
else dest <- node_var.get_value()
|" Wrapper for xref_equation, meant to be used inside of xref_equation
|" when you want to get the sub equation of a sub expression. It is
|" used to change the behavior when xref_equation is called from
|" another xref_equation call, or from the top level, so that we can do
|" resolution in several steps.
@with_dynvars(env, origin, entry_point)
fun sub_equation(): Equation =
if self.xref_stop_resolution() then self.stop_resolution_equation()
else self.xref_equation()
|" Internal helper for resolve_names. Resolve names for this node up to
|" xref_entry_point and xref_stop_resolution boundaries.
@external(uses_entity_info=true, uses_envs=true)
@call_memoizable
@with_dynvars(env, origin, entry_point)
fun resolve_own_names(generate_diagnostics: Bool): Bool
|" Internal helper for resolve_names, implementing the recursive logic
|" needed to resolve names across xref_stop_resolution boundaries.
@with_dynvars(env, origin)
fun resolve_children_names(generate_diagnostics: Bool): Bool =
node.children.all(
(c) =>
c.do(
# Only resolve nodes that have xref_stop_resolution set, and do
# not recursively explore nodes that are xref entry points.
(c) =>
if c.xref_entry_point() then true
else
(
if c.as_entity.xref_stop_resolution()
then {
bind entry_point = c;
bind env = self.xref_initial_env();
c.as_entity.resolve_own_names(generate_diagnostics)
}
else true
)
and c.as_entity.resolve_children_names(
generate_diagnostics
),
default_val=true
)
)
|" Resolves names for this node up to xref_entry_point boundaries.
@with_dynvars(env, origin)
fun resolve_names_internal(generate_diagnostics: Bool): Bool = {
bind entry_point = node;
self.resolve_own_names(generate_diagnostics)
and self.resolve_children_names(generate_diagnostics)
}
|" Resolves names in this node with an additional constraint given by
|" ``additional_equation``, up to xref_entry_point boundaries.
@with_dynvars(env, origin)
fun resolve_names_internal_with_eq(additional_equation: Equation): Bool = {
val eq =
{
bind entry_point = node;
self.xref_equation()
}
%and additional_equation;
eq.solve() and self.resolve_children_names(false)
}
|" This will resolve names for this node. If the operation is successful,
|" then type_var and ref_var will be bound on appropriate subnodes of the
|" statement.
@exported
@memoized
@call_memoizable
fun resolve_names(): Bool = {
bind env = self.xref_initial_env();
bind origin = node.origin_node();
self.resolve_names_internal(false)
}
|" Resolve names from the closest entry point up to this node. Note that
|" unlike ``resolve_names``, this will *not* trigger resolution of every
|" node with stop_resolution that lie in the sub-tree formed by the
|" closest entry point. It will only resolve those that are in the path to
|" resolving self. Consider for example the following entry point:
|"
|" .. code::
|"
|" R := (A, B);
|"
|" Since aggregate association nodes have ``stop_resolution`` set to True,
|" calling ``resolve_names_from_closest_entry_point`` on ``B`` will
|" resolve nodes ``R`` and ``B`` but not ``A``, because ``A`` does not lie
|" on the path to ``B``.
|"
|" This can be useful for resolving aggregates of variant records, because
|" resolution of a component association can safely call the resolution
|" of a discriminant association without triggering an infinite recursion,
|" as both are on different "paths".
fun resolve_names_from_closest_entry_point(): Bool =
# This is the closest entry point: resolve its names and stop the
# recursion.
if self.xref_entry_point()
then {
bind env = self.xref_initial_env();
bind origin = node.origin_node();
bind entry_point = node;
self.resolve_own_names(false)
}
# Otherwise, recurse on the parent
else
self.parent?.resolve_names_from_closest_entry_point().do(
(_) => {
bind env = self.xref_initial_env();
bind origin = node.origin_node();
# Resolution succeeded for the parent and this is a
# stop resolution, so resolve own names as well.
if self.xref_stop_resolution()
then {
bind entry_point = node;
self.resolve_own_names(false)
}
# Resolution succeeded and there is nothing to do
# on that particular node: return successfully.
else true
}
)
|" Return all the diagnostics produced by ``resolve_own_names`` on this
|" node. If it was never called on this node, or if it was called without
|" diagnostic generation enabled, return an empty array.
@external(uses_entity_info=true, uses_envs=true)
@call_memoizable
fun own_nameres_diagnostics(): Array[SolverDiagnostic]
|" Accumulates all the diagnostics emitted on the children of this node,
|" up to ``xref_entry_point`` boundaries. This considers all children
|" nodes and not only those for which ``xref_stop_resolution`` is True,
|" so as to handle calls to ``resolve_names_internal`` that are done
|" during the construction of xref equations.
@with_dynvars(env, origin)
fun children_nameres_diagnostics(): Array[SolverDiagnostic] =
self.children.mapcat(
(c) =>
c.do(
(c) =>
if c.is_null or c.xref_entry_point()
then null[Array[SolverDiagnostic]]
else
c.own_nameres_diagnostics()
& c.children_nameres_diagnostics()
)
)
|" If name resolution on this xref entry point fails, this returns all the
|" diagnostics that were produced while resolving it.
@exported
fun nameres_diagnostics(): Array[SolverDiagnostic] = {
bind env = self.xref_initial_env();
bind origin = node.origin_node();
val _ = self.resolve_names_internal(true);
self.own_nameres_diagnostics() & self.children_nameres_diagnostics()
}
|" Used as a predicate during name resolution to emit a diagnostic
|" when an entity is not found.
@predicate_error("no such entity")
fun missing_entity_error(): Bool = not node.is_null