Skip to content

Commit 90c8d24

Browse files
sipmasipma
committed
CHJ:POLY: fix warnings and reformat
1 parent aaf6605 commit 90c8d24

File tree

8 files changed

+242
-279
lines changed

8 files changed

+242
-279
lines changed

‎CodeHawk/CHJ/jchpoly/jCHAnalysis.ml‎

Lines changed: 38 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@
33
Author: Anca Browne
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
6-
6+
77
Copyright (c) 2005-2020 Kestrel Technology LLC
8-
Copyright (c) 2020-2023 Henny Sipma
8+
Copyright (c) 2020-2024 Henny B. Sipma
99
1010
Permission is hereby granted, free of charge, to any person obtaining a copy
1111
of this software and associated documentation files (the "Software"), to deal
1212
in the Software without restriction, including without limitation the rights
1313
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1414
copies of the Software, and to permit persons to whom the Software is
1515
furnished to do so, subject to the following conditions:
16-
16+
1717
The above copyright notice and this permission notice shall be included in all
1818
copies or substantial portions of the Software.
19-
19+
2020
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2121
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2222
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -26,52 +26,34 @@
2626
SOFTWARE.
2727
============================================================================= *)
2828

29-
open Big_int_Z
30-
3129
(* chlib *)
3230
open CHPretty
33-
open CHPrettyUtil
34-
open CHLanguage
35-
open CHAtlas
36-
open CHIntervalsDomainExtensiveArrays
37-
open CHIterator
38-
open CHStack
39-
open CHNumerical
40-
open CHUtils
41-
42-
(* chutil *)
43-
open CHXmlDocument
4431

4532
(* jchpre *)
46-
open JCHPreFileIO
47-
open JCHTaintOrigin
48-
49-
open JCHGlobals
50-
open JCHSystem
5133
open JCHPrintUtils
5234

5335

54-
let analysis_pass start bottom_up =
55-
if start then
56-
JCHFields.int_field_manager#start
57-
else
36+
let analysis_pass start bottom_up =
37+
if start then
38+
JCHFields.int_field_manager#start
39+
else
5840
begin
59-
JCHIntStubs.int_stub_manager#reset_calls ;
60-
JCHFields.int_field_manager#reset
61-
end ;
62-
JCHNumericAnalysis.make_numeric_analysis bottom_up
41+
JCHIntStubs.int_stub_manager#reset_calls;
42+
JCHFields.int_field_manager#reset
43+
end;
44+
JCHNumericAnalysis.make_numeric_analysis bottom_up
6345

6446
let numeric_analysis_1_2 () =
65-
pr__debug [NL; STR "Numeric analysis - First Pass"; NL; NL] ;
66-
analysis_pass true true ;
67-
JCHSystemUtils.add_timing "numeric analysis - first pass" ;
68-
pr__debug [NL; STR "Numeric analysis - Second Pass"; NL; NL] ;
69-
analysis_pass false false ;
70-
JCHSystemUtils.add_timing "numeric analysis - second pass"
47+
pr__debug [NL; STR "Numeric analysis - First Pass"; NL; NL];
48+
analysis_pass true true;
49+
JCHSystemUtils.add_timing "numeric analysis - first pass";
50+
pr__debug [NL; STR "Numeric analysis - Second Pass"; NL; NL];
51+
analysis_pass false false;
52+
JCHSystemUtils.add_timing "numeric analysis - second pass"
7153

72-
let numeric_analysis_1 () =
73-
analysis_pass true true ;
74-
JCHSystemUtils.add_timing "numeric analysis"
54+
let _numeric_analysis_1 () =
55+
analysis_pass true true;
56+
JCHSystemUtils.add_timing "numeric analysis"
7557

7658
let analyze_system
7759
~(analysis_level:int)
@@ -82,46 +64,46 @@ let analyze_system
8264
~(use_time_limits:bool)
8365
~(poly_analysis_time_limit:int)
8466
~(num_analysis_time_limit:int)
85-
~(use_overflow:bool) =
67+
~(use_overflow:bool) =
8668

87-
if not (Sys.file_exists "codehawk") then Unix.mkdir "codehawk" 0o750 ;
88-
if not (Sys.file_exists "codehawk/temp") then Unix.mkdir "codehawk/temp" 0o750 ;
89-
JCHBasicTypes.set_permissive true ;
90-
pr__debug [STR "Start the analysis."; NL] ;
69+
if not (Sys.file_exists "codehawk") then Unix.mkdir "codehawk" 0o750;
70+
if not (Sys.file_exists "codehawk/temp") then Unix.mkdir "codehawk/temp" 0o750;
71+
JCHBasicTypes.set_permissive true;
72+
pr__debug [STR "Start the analysis."; NL];
9173
JCHSystem.jsystem#set ((JCHIFSystem.chif_system)#get_system JCHIFSystem.base_system);
9274
pr__debug [STR "System was translated."; NL];
9375

9476
JCHAnalysisUtils.numeric_params#set_analysis_level analysis_level;
95-
JCHAnalysisUtils.numeric_params#set_system_use_intervals use_intervals;
77+
JCHAnalysisUtils.numeric_params#set_system_use_intervals use_intervals;
9678
JCHAnalysisUtils.numeric_params#set_number_joins number_joins;
9779
JCHAnalysisUtils.numeric_params#set_max_poly_coefficient max_poly_coeff;
98-
JCHAnalysisUtils.numeric_params#set_max_number_constraints_allowed max_nb_constraints ;
80+
JCHAnalysisUtils.numeric_params#set_max_number_constraints_allowed max_nb_constraints;
9981
JCHAnalysisUtils.numeric_params#set_use_time_limits false;
100-
JCHAnalysisUtils.numeric_params#set_use_time_limits use_time_limits;
82+
JCHAnalysisUtils.numeric_params#set_use_time_limits use_time_limits;
10183
JCHAnalysisUtils.numeric_params#set_constraint_analysis_time_limit poly_analysis_time_limit;
10284
JCHAnalysisUtils.numeric_params#set_numeric_analysis_time_limit num_analysis_time_limit;
10385
JCHAnalysisUtils.numeric_params#set_use_overflow use_overflow;
10486

105-
numeric_analysis_1_2 () ;
106-
JCHNumericAnalysis.set_pos_fields () ; (* needed for cost analysis *)
87+
numeric_analysis_1_2 ();
88+
JCHNumericAnalysis.set_pos_fields (); (* needed for cost analysis *)
10789
pr__debug [STR "Polyhedra invariants were produced."; NL];
10890
pr__debug [STR "Loops were reported."; NL]
10991

11092
let analyze_taint () =
111-
pr__debug [STR "analyze_taint "; NL] ;
93+
pr__debug [STR "analyze_taint "; NL];
11294
JCHSystem.jsystem#set (JCHIFSystem.chif_system#get_system JCHIFSystem.base_system);
11395
JCHTaintOrigin.set_use_one_top_target false;
114-
JCHTGraphAnalysis.make_tgraphs true
96+
JCHTGraphAnalysis.make_tgraphs true
11597

11698

117-
let analyze_taint_origins taint_origin_ind local_vars_only =
118-
pr__debug [STR "analyze_taint "; NL] ;
99+
let analyze_taint_origins taint_origin_ind local_vars_only =
100+
pr__debug [STR "analyze_taint "; NL];
119101
JCHSystem.jsystem#set (JCHIFSystem.chif_system#get_system JCHIFSystem.base_system);
120102
JCHTaintOrigin.set_use_one_top_target true;
121-
JCHTGraphAnalysis.make_tgraphs false ;
122-
pr__debug [STR "Start making origin graphs "; NL] ;
103+
JCHTGraphAnalysis.make_tgraphs false;
104+
pr__debug [STR "Start making origin graphs "; NL];
123105
let res_table =
124106
JCHTOriginGraphs.get_taint_origin_graph local_vars_only taint_origin_ind in
125107
pr__debug [NL; STR "result: "; NL; res_table#toPretty; NL];
126-
JCHSystemUtils.add_timing "origin graphs" ;
108+
JCHSystemUtils.add_timing "origin graphs";
127109
JCHTNode.save_taint_trail res_table taint_origin_ind

‎CodeHawk/CHJ/jchpoly/jCHAnalysis.mli‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@
33
Author: Anca Browne
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
6-
6+
77
Copyright (c) 2005-2020 Kestrel Technology LLC
8-
Copyright (c) 2020-2023 Henny Sipma
8+
Copyright (c) 2020-2024 Henny B. Sipma
99
1010
Permission is hereby granted, free of charge, to any person obtaining a copy
1111
of this software and associated documentation files (the "Software"), to deal
1212
in the Software without restriction, including without limitation the rights
1313
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1414
copies of the Software, and to permit persons to whom the Software is
1515
furnished to do so, subject to the following conditions:
16-
16+
1717
The above copyright notice and this permission notice shall be included in all
1818
copies or substantial portions of the Software.
19-
19+
2020
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2121
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2222
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE

‎CodeHawk/CHJ/jchpoly/jCHAnalysisUtils.mli‎

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@
33
Author: Anca Browne
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
6-
6+
77
Copyright (c) 2005-2020 Kestrel Technology LLC
8-
Copyright (c) 2020-2023 Henny Sipma
8+
Copyright (c) 2020-2024 Henny B. Sipma
99
1010
Permission is hereby granted, free of charge, to any person obtaining a copy
1111
of this software and associated documentation files (the "Software"), to deal
1212
in the Software without restriction, including without limitation the rights
1313
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1414
copies of the Software, and to permit persons to whom the Software is
1515
furnished to do so, subject to the following conditions:
16-
16+
1717
The above copyright notice and this permission notice shall be included in all
1818
copies or substantial portions of the Software.
19-
19+
2020
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2121
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2222
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -38,8 +38,6 @@ open CHUtils
3838
(* jchlib *)
3939
open JCHBasicTypesAPI
4040

41-
(* jchpre *)
42-
open JCHPreAPI
4341

4442
val set_current_proc_name : symbol_t -> unit
4543
val get_current_proc_name : unit -> symbol_t
@@ -109,9 +107,9 @@ val has_untranslated_caller : symbol_t -> bool
109107
val get_slot_interval : logical_stack_slot_int -> interval_t
110108

111109
val is_numeric : JCHProcInfo.jproc_info_t -> variable_t -> bool
112-
val is_collection : JCHProcInfo.jproc_info_t -> variable_t -> bool
113-
val is_array : JCHProcInfo.jproc_info_t -> variable_t -> bool
114-
val is_collection_or_array : JCHProcInfo.jproc_info_t -> variable_t -> bool
110+
val is_collection : JCHProcInfo.jproc_info_t -> variable_t -> bool
111+
val is_array : JCHProcInfo.jproc_info_t -> variable_t -> bool
112+
val is_collection_or_array : JCHProcInfo.jproc_info_t -> variable_t -> bool
115113

116114
val float_to_interval : float -> numerical_t * numerical_t * interval_t
117115

@@ -121,10 +119,10 @@ val get_length_vars :
121119
-> variable_t list
122120
* variable_t list
123121
* variable_t CHUtils.VariableCollections.table_t
124-
122+
125123
val include_length_vars :
126124
JCHProcInfo.jproc_info_t -> variable_t list -> variable_t list
127-
125+
128126
val include_all_length_vars :
129127
JCHProcInfo.jproc_info_t
130128
-> variable_t list
@@ -133,4 +131,3 @@ val include_all_length_vars :
133131
-> variable_t list * variable_t list * int list
134132

135133
val integer_div : interval_t -> interval_t -> interval_t
136-

‎CodeHawk/CHJ/jchpoly/jCHCollectors.mli‎

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -3,19 +3,20 @@
33
Author: Anca Browne
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
6-
7-
Copyright (c) 2005-2020 Kestrel Technology LLC
6+
7+
Copyright (c) 2005-2020 Kestrel Technology LLC
8+
Copyright (c) 2020-2024 Henny B. Sipma
89
910
Permission is hereby granted, free of charge, to any person obtaining a copy
1011
of this software and associated documentation files (the "Software"), to deal
1112
in the Software without restriction, including without limitation the rights
1213
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1314
copies of the Software, and to permit persons to whom the Software is
1415
furnished to do so, subject to the following conditions:
15-
16+
1617
The above copyright notice and this permission notice shall be included in all
1718
copies or substantial portions of the Software.
18-
19+
1920
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2021
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2122
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -28,22 +29,19 @@
2829
(* chlib *)
2930
open CHLanguage
3031

31-
(* jchlib *)
32-
open JCHBasicTypesAPI
33-
34-
(* jchpre *)
35-
open JCHPreAPI
3632

3733
val collect_loop_vars : symbol_t -> code_int -> variable_t list
3834

3935
val collect_bound_vars : symbol_t -> code_int -> variable_t list
4036

41-
val collect_lin_eqs_info :
37+
val collect_lin_eqs_info :
4238
symbol_t
43-
-> JCHProcInfo.jproc_info_t
39+
-> JCHProcInfo.jproc_info_t
4440
-> CHUtils.VariableCollections.set_t CHUtils.IntCollections.table_t
4541
* CHUtils.IntCollections.set_t
46-
* variable_t CHUtils.VariableCollections.table_t CHUtils.VariableCollections.table_t
42+
* variable_t
43+
CHUtils.VariableCollections.table_t CHUtils.VariableCollections.table_t
4744

4845
val collect_state_pcs :
49-
JCHProcInfo.jproc_info_t -> CHUtils.IntCollections.set_t CHUtils.SymbolCollections.table_t
46+
JCHProcInfo.jproc_info_t
47+
-> CHUtils.IntCollections.set_t CHUtils.SymbolCollections.table_t

0 commit comments

Comments
 (0)