Skip to content

Commit 8376c96

Browse files
shannonzhufacebook-github-bot
authored andcommitted
Use full annotation store in resolution fixpoint
Summary: Store and fetch the full set of local annotations, as we used to. iirc, the resolution fixpoint is used so we can rebuild a resolution and have typing context at each step in the fixpoint / before and after each statement. Before this diff to make the temporary annotations change a little easier to tackle at once, this continued to only store non-temporary annotations. Temporary annotations *are* part of the type context though, so we should both store the full annotation store (both permanent and temporary local annotations) when we save a pre/post condition, as well as read in both when constructing a resolution from a saved pre/post condition set. Reviewed By: grievejia Differential Revision: D30413804 fbshipit-source-id: 59139cfc1fa855a70a6654da42d119666af9095d
1 parent d2082a9 commit 8376c96

File tree

7 files changed

+65
-47
lines changed

7 files changed

+65
-47
lines changed

source/analysis/localAnnotationMap.ml

Lines changed: 42 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -10,18 +10,33 @@ open Ast
1010
open Pyre
1111

1212
module Annotations = struct
13+
type annotation_store = {
14+
annotations: RefinementUnit.t Reference.Map.Tree.t;
15+
temporary_annotations: RefinementUnit.t Reference.Map.Tree.t;
16+
}
17+
[@@deriving eq]
18+
1319
type t = {
14-
precondition: RefinementUnit.t Reference.Map.Tree.t;
15-
postcondition: RefinementUnit.t Reference.Map.Tree.t;
20+
precondition: annotation_store;
21+
postcondition: annotation_store;
1622
}
1723
[@@deriving eq]
1824

19-
let pp_state formatter map =
20-
let pp_element ~key ~data =
21-
Format.fprintf formatter "\"%a\": \"%a\", " Reference.pp key RefinementUnit.pp data
25+
let pp_state formatter { annotations; temporary_annotations } =
26+
let pp_element ~temporary ~key ~data =
27+
let temporary_suffix = if temporary then "(temp)" else "" in
28+
Format.fprintf
29+
formatter
30+
"\"%a\": \"%a\"%s, "
31+
Reference.pp
32+
key
33+
RefinementUnit.pp
34+
data
35+
temporary_suffix
2236
in
2337
Format.fprintf formatter "{";
24-
Reference.Map.Tree.iteri map ~f:pp_element;
38+
Reference.Map.Tree.iteri annotations ~f:(pp_element ~temporary:false);
39+
Reference.Map.Tree.iteri temporary_annotations ~f:(pp_element ~temporary:true);
2540
Format.fprintf formatter "}"
2641

2742

@@ -58,32 +73,47 @@ let pp formatter statements =
5873
let show map = Format.asprintf "%a" pp map
5974

6075
let set
61-
?(precondition = Reference.Map.empty)
62-
?(postcondition = Reference.Map.empty)
76+
?(precondition =
77+
{ Resolution.annotations = Reference.Map.empty; temporary_annotations = Reference.Map.empty })
78+
?(postcondition =
79+
{ Resolution.annotations = Reference.Map.empty; temporary_annotations = Reference.Map.empty })
6380
~key
6481
local_annotations
6582
=
83+
let convert_to_tree { Resolution.annotations; temporary_annotations } =
84+
{
85+
Annotations.annotations = Reference.Map.to_tree annotations;
86+
temporary_annotations = Reference.Map.to_tree temporary_annotations;
87+
}
88+
in
6689
Hashtbl.set
6790
local_annotations
6891
~key
6992
~data:
7093
{
71-
Annotations.precondition = Reference.Map.to_tree precondition;
72-
postcondition = Reference.Map.to_tree postcondition;
94+
Annotations.precondition = convert_to_tree precondition;
95+
postcondition = convert_to_tree postcondition;
7396
}
7497

7598

7699
module ReadOnly = struct
77100
type t = Annotations.t Int.Map.Tree.t
78101

102+
let convert_to_map { Annotations.annotations; temporary_annotations } =
103+
{
104+
Resolution.annotations = Reference.Map.of_tree annotations;
105+
temporary_annotations = Reference.Map.of_tree temporary_annotations;
106+
}
107+
108+
79109
let get_precondition local_annotations key =
80110
Int.Map.Tree.find local_annotations key
81-
>>| fun { Annotations.precondition; _ } -> Reference.Map.of_tree precondition
111+
>>| fun { Annotations.precondition; _ } -> convert_to_map precondition
82112

83113

84114
let get_postcondition local_annotations key =
85115
Int.Map.Tree.find local_annotations key
86-
>>| fun { Annotations.postcondition; _ } -> Reference.Map.of_tree postcondition
116+
>>| fun { Annotations.postcondition; _ } -> convert_to_map postcondition
87117
end
88118

89119
let read_only local_annotations = Hashtbl.to_alist local_annotations |> Int.Map.Tree.of_alist_exn

source/analysis/localAnnotationMap.mli

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,6 @@
55
* LICENSE file in the root directory of this source tree.
66
*)
77

8-
open Ast
9-
108
type t
119

1210
val empty : unit -> t
@@ -18,18 +16,18 @@ val pp : Format.formatter -> t -> unit
1816
val show : t -> string
1917

2018
val set
21-
: ?precondition:RefinementUnit.t Reference.Map.t ->
22-
?postcondition:RefinementUnit.t Reference.Map.t ->
19+
: ?precondition:Resolution.annotation_store ->
20+
?postcondition:Resolution.annotation_store ->
2321
key:int ->
2422
t ->
2523
unit
2624

2725
module ReadOnly : sig
2826
type t
2927

30-
val get_precondition : t -> int -> RefinementUnit.t Reference.Map.t option
28+
val get_precondition : t -> int -> Resolution.annotation_store option
3129

32-
val get_postcondition : t -> int -> RefinementUnit.t Reference.Map.t option
30+
val get_postcondition : t -> int -> Resolution.annotation_store option
3331
end
3432

3533
val read_only : t -> ReadOnly.t

source/analysis/lookup.ml

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -265,30 +265,22 @@ let create_of_module type_environment qualifier =
265265
let pre_annotations, post_annotations =
266266
let key = [%hash: int * int] (node_id, statement_index) in
267267
( LocalAnnotationMap.ReadOnly.get_precondition annotation_lookup key
268-
|> Option.value ~default:Reference.Map.empty,
268+
|> Option.value ~default:Resolution.empty_annotation_store,
269269
LocalAnnotationMap.ReadOnly.get_postcondition annotation_lookup key
270-
|> Option.value ~default:Reference.Map.empty )
270+
|> Option.value ~default:Resolution.empty_annotation_store )
271271
in
272272
let pre_resolution =
273273
(* TODO(T65923817): Eliminate the need of creating a dummy context here *)
274274
TypeCheck.resolution
275275
global_resolution
276-
~annotation_store:
277-
{
278-
Resolution.annotations = pre_annotations;
279-
temporary_annotations = Reference.Map.empty;
280-
}
276+
~annotation_store:pre_annotations
281277
(module TypeCheck.DummyContext)
282278
in
283279
let post_resolution =
284280
(* TODO(T65923817): Eliminate the need of creating a dummy context here *)
285281
TypeCheck.resolution
286282
global_resolution
287-
~annotation_store:
288-
{
289-
Resolution.annotations = post_annotations;
290-
temporary_annotations = Reference.Map.empty;
291-
}
283+
~annotation_store:post_annotations
292284
(module TypeCheck.DummyContext)
293285
in
294286
Visit.visit

source/analysis/resolution.ml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,10 @@ let pp format { annotation_store = { annotations; temporary_annotations }; type_
6161

6262
let show resolution = Format.asprintf "%a" pp resolution
6363

64+
let empty_annotation_store =
65+
{ annotations = Reference.Map.empty; temporary_annotations = Reference.Map.empty }
66+
67+
6468
let is_global { global_resolution; _ } ~reference =
6569
Reference.delocalize reference |> GlobalResolution.global global_resolution |> Option.is_some
6670

source/analysis/resolution.mli

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ val create
3030
unit ->
3131
t
3232

33+
val empty_annotation_store : annotation_store
34+
3335
val resolve_expression : t -> Expression.t -> t * Type.t
3436

3537
val resolve_expression_to_type : t -> Expression.t -> Type.t

source/analysis/typeCheck.ml

Lines changed: 7 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1874,8 +1874,7 @@ module State (Context : Context) = struct
18741874
let state =
18751875
let resolution_fixpoint = LocalAnnotationMap.empty () in
18761876
let error_map = LocalErrorMap.empty () in
1877-
(* TODO(T70545381): Use full annotation store in resolution fixpoint. *)
1878-
let postcondition = Resolution.annotations resolution in
1877+
let postcondition = Resolution.annotation_store resolution in
18791878
let key = [%hash: int * int] (Cfg.entry_index, 0) in
18801879
LocalAnnotationMap.set resolution_fixpoint ~key ~postcondition;
18811880
LocalErrorMap.set error_map ~key ~errors;
@@ -5915,9 +5914,8 @@ module State (Context : Context) = struct
59155914
match post_resolution with
59165915
| None -> ()
59175916
| Some post_resolution ->
5918-
(* TODO(T70545381): Use full annotation store in resolution fixpoint. *)
5919-
let precondition = Resolution.annotations resolution in
5920-
let postcondition = Resolution.annotations post_resolution in
5917+
let precondition = Resolution.annotation_store resolution in
5918+
let postcondition = Resolution.annotation_store post_resolution in
59215919
LocalAnnotationMap.set state.resolution_fixpoint ~key ~precondition ~postcondition
59225920
in
59235921
{ state with resolution = post_resolution }
@@ -5952,8 +5950,7 @@ end
59525950

59535951
let resolution
59545952
global_resolution
5955-
?(annotation_store =
5956-
{ Resolution.annotations = Reference.Map.empty; temporary_annotations = Reference.Map.empty })
5953+
?(annotation_store = Resolution.empty_annotation_store)
59575954
(module Context : Context)
59585955
=
59595956
let module State = State (Context) in
@@ -5973,15 +5970,14 @@ let resolution
59735970

59745971

59755972
let resolution_with_key ~global_resolution ~local_annotations ~parent ~key context =
5976-
let annotations =
5973+
let annotation_store =
59775974
Option.value_map
59785975
local_annotations
59795976
~f:(fun map ->
59805977
LocalAnnotationMap.ReadOnly.get_precondition map key
5981-
|> Option.value ~default:Reference.Map.empty)
5982-
~default:Reference.Map.empty
5978+
|> Option.value ~default:Resolution.empty_annotation_store)
5979+
~default:Resolution.empty_annotation_store
59835980
in
5984-
let annotation_store = { Resolution.annotations; temporary_annotations = Reference.Map.empty } in
59855981
resolution global_resolution ~annotation_store context |> Resolution.with_parent ~parent
59865982

59875983

source/interprocedural/test/dependencyGraphTest.ml

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -354,12 +354,8 @@ let test_type_collection context =
354354
let test_expect (node_id, statement_index, test_expression, expected_type) =
355355
let key = [%hash: int * int] (node_id, statement_index) in
356356
let annotation_store =
357-
{
358-
Resolution.annotations =
359-
(LocalAnnotationMap.ReadOnly.get_precondition lookup key
360-
|> fun value -> Option.value_exn value);
361-
temporary_annotations = Reference.Map.empty;
362-
}
357+
LocalAnnotationMap.ReadOnly.get_precondition lookup key
358+
|> fun value -> Option.value_exn value
363359
in
364360
let global_resolution = TypeEnvironment.ReadOnly.global_resolution environment in
365361
let resolution =

0 commit comments

Comments
 (0)