@@ -820,3 +820,355 @@ let undo_compress (changes, _old) =
820
820
ty.desc < - desc; r := ! next
821
821
| _ -> () )
822
822
log
823
+
824
+
825
+ module Alloc_mode = struct
826
+ type nonrec const = Types .alloc_mode_const = Global | Local
827
+ type t = Types .alloc_mode =
828
+ | Amode of const
829
+ | Amodevar of alloc_mode_var
830
+
831
+ let global = Amode Global
832
+ let local = Amode Local
833
+ let of_const = function
834
+ | Global -> global
835
+ | Local -> local
836
+
837
+ let min_mode = global
838
+
839
+ let max_mode = local
840
+
841
+ let le_const a b =
842
+ match a, b with
843
+ | Global , _ | _ , Local -> true
844
+ | Local , Global -> false
845
+
846
+ let join_const a b =
847
+ match a, b with
848
+ | Local , _ | _ , Local -> Local
849
+ | Global , Global -> Global
850
+
851
+ let meet_const a b =
852
+ match a, b with
853
+ | Global , _ | _ , Global -> Global
854
+ | Local , Local -> Local
855
+
856
+ exception NotSubmode
857
+ (*
858
+ let pp_c ppf = function
859
+ | Global -> Printf.fprintf ppf "0"
860
+ | Local -> Printf.fprintf ppf "1"
861
+ let pp_v ppf v =
862
+ let i = v.mvid in
863
+ (if i < 26 then Printf.fprintf ppf "%c" (Char.chr (Char.code 'a' + i))
864
+ else Printf.fprintf ppf "v%d" i);
865
+ Printf.fprintf ppf "[%a%a]" pp_c v.lower pp_c v.upper
866
+ *)
867
+ let submode_cv m v =
868
+ (* Printf.printf " %a <= %a\n" pp_c m pp_v v; *)
869
+ if le_const m v.lower then ()
870
+ else if not (le_const m v.upper) then raise NotSubmode
871
+ else begin
872
+ let m = join_const v.lower m in
873
+ v.lower < - m;
874
+ if m = v.upper then v.vlower < - []
875
+ end
876
+
877
+ let rec submode_vc v m =
878
+ (* Printf.printf " %a <= %a\n" pp_v v pp_c m; *)
879
+ if le_const v.upper m then ()
880
+ else if not (le_const v.lower m) then raise NotSubmode
881
+ else begin
882
+ let m = meet_const v.upper m in
883
+ v.upper < - m;
884
+ v.vlower |> List. iter (fun a ->
885
+ (* a <= v <= m *)
886
+ submode_vc a m;
887
+ v.lower < - join_const v.lower a.lower;
888
+ );
889
+ if v.lower = m then v.vlower < - []
890
+ end
891
+
892
+ let submode_vv a b =
893
+ (* Printf.printf " %a <= %a\n" pp_v a pp_v b; *)
894
+ if le_const a.upper b.lower then ()
895
+ else if List. memq a b.vlower then ()
896
+ else begin
897
+ submode_vc a b.upper;
898
+ b.vlower < - a :: b.vlower;
899
+ submode_cv a.lower b;
900
+ end
901
+
902
+ let submode a b =
903
+ match
904
+ match a, b with
905
+ | Amode a , Amode b ->
906
+ if not (le_const a b) then raise NotSubmode
907
+ | Amodevar v , Amode c ->
908
+ (* Printf.printf "%a <= %a\n" pp_v v pp_c c; *)
909
+ submode_vc v c
910
+ | Amode c , Amodevar v ->
911
+ (* Printf.printf "%a <= %a\n" pp_c c pp_v v; *)
912
+ submode_cv c v
913
+ | Amodevar a , Amodevar b ->
914
+ (* Printf.printf "%a <= %a\n" pp_v a pp_v b; *)
915
+ submode_vv a b
916
+ with
917
+ | () -> Ok ()
918
+ | exception NotSubmode -> Error ()
919
+
920
+ let submode_exn t1 t2 =
921
+ match submode t1 t2 with
922
+ | Ok () -> ()
923
+ | Error () -> invalid_arg " submode_exn"
924
+
925
+ let equate a b =
926
+ match submode a b, submode b a with
927
+ | Ok () , Ok () -> Ok ()
928
+ | Error (), _ | _ , Error () -> Error ()
929
+
930
+ let next_id = ref (- 1 )
931
+ let fresh () =
932
+ incr next_id;
933
+ { upper = Local ; lower = Global ; vlower = [] ; mvid = ! next_id }
934
+
935
+ let rec all_equal v = function
936
+ | [] -> true
937
+ | v' :: rest ->
938
+ if v == v' then all_equal v rest
939
+ else false
940
+
941
+ let joinvars vars =
942
+ match vars with
943
+ | [] -> global
944
+ | v :: rest ->
945
+ let v =
946
+ if all_equal v rest then v
947
+ else begin
948
+ let v = fresh () in
949
+ List. iter (fun v' -> submode_vv v' v) vars;
950
+ v
951
+ end
952
+ in
953
+ Amodevar v
954
+
955
+ let join ms =
956
+ let rec aux vars = function
957
+ | [] -> joinvars vars
958
+ | Amode Global :: ms -> aux vars ms
959
+ | Amode Local :: _ -> local
960
+ | Amodevar v :: ms -> aux (v :: vars) ms
961
+ in aux [] ms
962
+
963
+ let constrain_upper = function
964
+ | Amode m -> m
965
+ | Amodevar v ->
966
+ submode_cv v.upper v;
967
+ v.upper
968
+
969
+ let compress_vlower v =
970
+ (* Ensure that each transitive lower bound of v
971
+ is a direct lower bound of v *)
972
+ let rec trans v' =
973
+ if le_const v'.upper v.lower then ()
974
+ else if List. memq v' v.vlower then ()
975
+ else begin
976
+ v.vlower < - v' :: v.vlower;
977
+ trans_low v'
978
+ end
979
+ and trans_low v' =
980
+ submode_cv v'.lower v;
981
+ List. iter trans v'.vlower
982
+ in
983
+ List. iter trans_low v.vlower
984
+
985
+ let constrain_lower = function
986
+ | Amode m -> m
987
+ | Amodevar v ->
988
+ compress_vlower v;
989
+ submode_vc v v.lower;
990
+ v.lower
991
+
992
+ let newvar () = Amodevar (fresh () )
993
+
994
+ let check_const = function
995
+ | Amode m -> Some m
996
+ | Amodevar v when v.lower = v.upper ->
997
+ Some v.lower
998
+ | Amodevar _ -> None
999
+
1000
+ let print_const ppf = function
1001
+ | Global -> Format. fprintf ppf " Global"
1002
+ | Local -> Format. fprintf ppf " Local"
1003
+
1004
+ let print_var_id ppf v =
1005
+ Format. fprintf ppf " ?%i" v.mvid
1006
+
1007
+ let print_var ppf v =
1008
+ compress_vlower v;
1009
+ if v.lower = v.upper then begin
1010
+ print_const ppf v.lower
1011
+ end else if v.vlower = [] then begin
1012
+ print_var_id ppf v
1013
+ end else begin
1014
+ Format. fprintf ppf " %a[> %a]"
1015
+ print_var_id v
1016
+ (Format. pp_print_list print_var_id) v.vlower
1017
+ end
1018
+
1019
+ let print ppf = function
1020
+ | Amode m -> print_const ppf m
1021
+ | Amodevar v -> print_var ppf v
1022
+
1023
+ end
1024
+
1025
+ module Value_mode = struct
1026
+
1027
+ type const =
1028
+ | Global
1029
+ | Regional
1030
+ | Local
1031
+
1032
+ let r_as_l : const -> Alloc_mode.const = function
1033
+ | Global -> Global
1034
+ | Regional -> Local
1035
+ | Local -> Local
1036
+ [@@ warning " -unused-value-declaration" ]
1037
+
1038
+ let r_as_g : const -> Alloc_mode.const = function
1039
+ | Global -> Global
1040
+ | Regional -> Global
1041
+ | Local -> Local
1042
+ [@@ warning " -unused-value-declaration" ]
1043
+
1044
+ let of_alloc_consts
1045
+ ~(r_as_l : Alloc_mode.const )
1046
+ ~(r_as_g : Alloc_mode.const ) =
1047
+ match r_as_l, r_as_g with
1048
+ | Global , Global -> Global
1049
+ | Global , Local -> assert false
1050
+ | Local , Global -> Regional
1051
+ | Local , Local -> Local
1052
+
1053
+ type t = Types .value_mode =
1054
+ { r_as_l : Alloc_mode .t ;
1055
+ (* [r_as_l] is the image of the mode under the [r_as_l] function *)
1056
+ r_as_g : Alloc_mode .t ;
1057
+ (* [r_as_g] is the image of the mode under the [r_as_g] function.
1058
+ Always less than [r_as_l]. *) }
1059
+
1060
+ let global =
1061
+ let r_as_l = Alloc_mode. global in
1062
+ let r_as_g = Alloc_mode. global in
1063
+ { r_as_l; r_as_g }
1064
+
1065
+ let regional =
1066
+ let r_as_l = Alloc_mode. local in
1067
+ let r_as_g = Alloc_mode. global in
1068
+ { r_as_l; r_as_g }
1069
+
1070
+ let local =
1071
+ let r_as_l = Alloc_mode. local in
1072
+ let r_as_g = Alloc_mode. local in
1073
+ { r_as_l; r_as_g }
1074
+
1075
+ let of_const = function
1076
+ | Global -> global
1077
+ | Regional -> regional
1078
+ | Local -> local
1079
+
1080
+ let max_mode =
1081
+ let r_as_l = Alloc_mode. max_mode in
1082
+ let r_as_g = Alloc_mode. max_mode in
1083
+ { r_as_l; r_as_g }
1084
+
1085
+ let min_mode =
1086
+ let r_as_l = Alloc_mode. min_mode in
1087
+ let r_as_g = Alloc_mode. min_mode in
1088
+ { r_as_l; r_as_g }
1089
+
1090
+ let of_alloc mode =
1091
+ let r_as_l = mode in
1092
+ let r_as_g = mode in
1093
+ { r_as_l; r_as_g }
1094
+
1095
+ let local_to_regional t = { t with r_as_g = Alloc_mode. global }
1096
+
1097
+ let regional_to_global t = { t with r_as_l = t.r_as_g }
1098
+
1099
+ let regional_to_local t = { t with r_as_g = t.r_as_l }
1100
+
1101
+ let global_to_regional t = { t with r_as_l = Alloc_mode. local }
1102
+
1103
+ let regional_to_global_alloc t = t.r_as_g
1104
+
1105
+ let regional_to_local_alloc t = t.r_as_l
1106
+
1107
+ type error = [`Regionality | `Locality ]
1108
+
1109
+ let submode t1 t2 =
1110
+ match Alloc_mode. submode t1.r_as_l t2.r_as_l with
1111
+ | Error () -> Error `Regionality
1112
+ | Ok () as ok -> begin
1113
+ match Alloc_mode. submode t1.r_as_g t2.r_as_g with
1114
+ | Ok () -> ok
1115
+ | Error () -> Error `Locality
1116
+ end
1117
+
1118
+ let submode_exn t1 t2 =
1119
+ match submode t1 t2 with
1120
+ | Ok () -> ()
1121
+ | Error _ -> invalid_arg " submode_exn"
1122
+
1123
+ let rec submode_meet t = function
1124
+ | [] -> Ok ()
1125
+ | t' :: rest ->
1126
+ match submode t t' with
1127
+ | Ok () -> submode_meet t rest
1128
+ | Error _ as err -> err
1129
+
1130
+ let join ts =
1131
+ let r_as_l = Alloc_mode. join (List. map (fun t -> t.r_as_l) ts) in
1132
+ let r_as_g = Alloc_mode. join (List. map (fun t -> t.r_as_g) ts) in
1133
+ { r_as_l; r_as_g }
1134
+
1135
+ let constrain_upper t =
1136
+ let r_as_l = Alloc_mode. constrain_upper t.r_as_l in
1137
+ let r_as_g = Alloc_mode. constrain_upper t.r_as_g in
1138
+ of_alloc_consts ~r_as_l ~r_as_g
1139
+
1140
+ let constrain_lower t =
1141
+ let r_as_l = Alloc_mode. constrain_lower t.r_as_l in
1142
+ let r_as_g = Alloc_mode. constrain_lower t.r_as_g in
1143
+ of_alloc_consts ~r_as_l ~r_as_g
1144
+
1145
+ let newvar () =
1146
+ let r_as_l = Alloc_mode. newvar () in
1147
+ let r_as_g = Alloc_mode. newvar () in
1148
+ Alloc_mode. submode_exn r_as_g r_as_l;
1149
+ { r_as_l; r_as_g }
1150
+
1151
+ let check_const t =
1152
+ match Alloc_mode. check_const t.r_as_l with
1153
+ | None -> None
1154
+ | Some r_as_l ->
1155
+ match Alloc_mode. check_const t.r_as_g with
1156
+ | None -> None
1157
+ | Some r_as_g ->
1158
+ Some (of_alloc_consts ~r_as_l ~r_as_g )
1159
+
1160
+ let print_const ppf = function
1161
+ | Global -> Format. fprintf ppf " Global"
1162
+ | Regional -> Format. fprintf ppf " Regional"
1163
+ | Local -> Format. fprintf ppf " Local"
1164
+
1165
+ let print ppf t =
1166
+ match check_const t with
1167
+ | Some const -> print_const ppf const
1168
+ | None ->
1169
+ Format. fprintf ppf
1170
+ " @[<2>r_as_l: %a@ r_as_g: %a@]"
1171
+ Alloc_mode. print t.r_as_l
1172
+ Alloc_mode. print t.r_as_g
1173
+
1174
+ end
0 commit comments