Skip to content

Commit cc690ac

Browse files
sipmasipma
committed
CHC: fix warnings, add documentation, reformat
1 parent ec73b67 commit cc690ac

30 files changed

+1083
-1086
lines changed

‎CodeHawk/CHC/cchanalyze/cCHAnalyze.ml‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,9 @@ open CHValueSetsDomainNoArrays
4444
(* chutil *)
4545
open CHAnalysisSetup
4646
open CHLogger
47-
open CHTiming
4847
open CHTimingLog
4948

5049
(* cchlib *)
51-
open CCHSettings
5250
open CCHUtilities
5351

5452
(* cchpre *)

‎CodeHawk/CHC/cchanalyze/cCHCommon.mli‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,23 @@
11
(* =============================================================================
2-
CodeHawk C Analyzer
2+
CodeHawk C Analyzer
33
Author: Henny Sipma
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
6-
6+
77
Copyright (c) 2005-2019 Kestrel Technology LLC
8+
Copyright (c) 2020-2024 Henny B. Sipma
9+
Copyright (c) 2024 Aarno Labs LLC
810
911
Permission is hereby granted, free of charge, to any person obtaining a copy
1012
of this software and associated documentation files (the "Software"), to deal
1113
in the Software without restriction, including without limitation the rights
1214
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1315
copies of the Software, and to permit persons to whom the Software is
1416
furnished to do so, subject to the following conditions:
15-
17+
1618
The above copyright notice and this permission notice shall be included in all
1719
copies or substantial portions of the Software.
18-
20+
1921
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2022
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2123
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE

‎CodeHawk/CHC/cchanalyze/cCHPOCheckAllocationBase.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ object (self)
206206
begin
207207
match memref#get_base with
208208
| CStackAddress svar ->
209-
let (vinfo,offset) = poq#env#get_local_variable svar in
209+
let (vinfo, _offset) = poq#env#get_local_variable svar in
210210
let deps = DLocal [inv#index] in
211211
let msg = "address of stack variable: " ^ vinfo.vname in
212212
Some (deps, msg)
@@ -227,7 +227,7 @@ object (self)
227227
begin
228228
match memref#get_base with
229229
| CGlobalAddress gvar ->
230-
let (vinfo,offset) = poq#env#get_global_variable gvar in
230+
let (vinfo, _offset) = poq#env#get_global_variable gvar in
231231
let deps = DLocal [inv#index] in
232232
let msg = "address of global variable: " ^ vinfo.vname in
233233
Some (deps, msg)
@@ -341,14 +341,14 @@ object (self)
341341

342342
(* ----------------------- violation -------------------------------------- *)
343343

344-
method private xpr_implies_violation (invindex: int) (x:xpr_t) =
344+
method private xpr_implies_violation (_invindex: int) (x:xpr_t) =
345345
let _ = poq#set_diagnostic_arg 1 ("UB: " ^ (x2s x)) in
346346
None
347347

348348
method private base_offset_implies_open_ended_violation
349349
(invindex: int) (v: variable_t) =
350350
match self#var_implies_safe invindex v with
351-
| Some (deps, msg) ->
351+
| Some (_deps, msg) ->
352352
let deps = DLocal [invindex] in
353353
let msg = "possibly some offset from valid base address: " ^ msg in
354354
Some (deps, msg)

‎CodeHawk/CHC/cchanalyze/cCHPOCheckBuffer.ml‎

Lines changed: 46 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,23 @@
11
(* =============================================================================
2-
CodeHawk C Analyzer
2+
CodeHawk C Analyzer
33
Author: Henny Sipma
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
6-
6+
77
Copyright (c) 2005-2019 Kestrel Technology LLC
8+
Copyright (c) 2020-2024 Henny B. Sipma
9+
Copyright (c) 2024 Aarno Labs LLC
810
911
Permission is hereby granted, free of charge, to any person obtaining a copy
1012
of this software and associated documentation files (the "Software"), to deal
1113
in the Software without restriction, including without limitation the rights
1214
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1315
copies of the Software, and to permit persons to whom the Software is
1416
furnished to do so, subject to the following conditions:
15-
17+
1618
The above copyright notice and this permission notice shall be included in all
1719
copies or substantial portions of the Software.
18-
20+
1921
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2022
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2123
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -25,9 +27,6 @@
2527
SOFTWARE.
2628
============================================================================= *)
2729

28-
(* chlib *)
29-
open CHNumerical
30-
3130
(* chutil *)
3231
open CHPrettyUtil
3332

@@ -39,7 +38,6 @@ open Xsimplify
3938

4039
(* cchlib *)
4140
open CCHBasicTypes
42-
open CCHTypesToPretty
4341

4442
(* cchpre *)
4543
open CCHPreTypes
@@ -50,78 +48,89 @@ open CCHAnalysisTypes
5048
let x2p = xpr_formatter#pr_expr
5149
let p2s = pretty_to_string
5250
let x2s x = p2s (x2p x)
53-
let e2s e = p2s (exp_to_pretty e)
5451

5552

5653
class buffer_checker_t
5754
(poq:po_query_int)
58-
(e1:exp)
59-
(e2:exp)
55+
(_e1:exp)
56+
(_e2:exp)
6057
(invs1:invariant_int list)
6158
(invs2:invariant_int list) =
6259
object (self)
6360
(* ----------------------------- safe ------------------------------------- *)
6461

65-
method private xpr_implies_safe inv1index inv2index x1 x2 =
62+
method private xpr_implies_safe
63+
(inv1index: int) (_inv2index: int) (x1: xpr_t) (x2: xpr_t) =
6664
match poq#xpr_buffer_offset_size 1 inv1index x1 with
6765
| Some (gname, xsize, xoffset, deps) ->
68-
let xconstraint = XOp (XGe, [ XOp (XMinus, [ xsize ; xoffset ]) ; x2 ]) in
66+
let xconstraint = XOp (XGe, [XOp (XMinus, [xsize; xoffset]); x2]) in
6967
let sconstraint = simplify_xpr xconstraint in
7068
if is_true sconstraint then
71-
let msg = "buffer: " ^ gname ^ " has size: " ^ (x2s xsize) ^ " and offset: "
72-
^ (x2s xoffset) ^ ", which satisfies safety constraint: "
73-
^ (x2s xconstraint) in
69+
let msg =
70+
Printf.sprintf
71+
("buffer: %s has size: %s and offset: %s, which satisfies safety "
72+
^^ " constraint: %s")
73+
gname
74+
(x2s xsize)
75+
(x2s xoffset)
76+
(x2s xconstraint) in
7477
Some (deps,msg)
7578
else
7679
begin
77-
poq#set_diagnostic ("remaining constraint: " ^ (x2s sconstraint)) ;
80+
poq#set_diagnostic ("remaining constraint: " ^ (x2s sconstraint));
7881
None
7982
end
8083
| _ -> None
81-
82-
method private inv_implies_safe inv1 inv2 =
83-
match (inv1#expr,inv2#upper_bound_xpr) with
84+
85+
method private inv_implies_safe (inv1: invariant_int) (inv2: invariant_int) =
86+
match (inv1#expr, inv2#upper_bound_xpr) with
8487
| (Some x1, Some x2) -> self#xpr_implies_safe inv1#index inv2#index x1 x2
8588
| _ -> None
86-
89+
8790
method check_safe =
8891
match (invs1,invs2) with
89-
| ([],_) | (_,[]) -> false
92+
| ([], _) | (_, []) -> false
9093
| _ ->
9194
List.fold_left (fun acc1 inv1 ->
9295
acc1 ||
9396
List.fold_left (fun acc2 inv2 ->
9497
acc2 ||
9598
match self#inv_implies_safe inv1 inv2 with
96-
| Some (deps,msg) ->
99+
| Some (deps, msg) ->
97100
begin
98-
poq#record_safe_result deps msg ;
101+
poq#record_safe_result deps msg;
99102
true
100103
end
101104
| _ -> false) acc1 invs2) false invs1
102-
105+
103106
(* ----------------------- violation -------------------------------------- *)
104107

105-
method private xpr_implies_violation inv1index inv2index x1 x2 =
108+
method private xpr_implies_violation
109+
(inv1index: int) (_inv2index: int) (x1: xpr_t) (x2: xpr_t) =
106110
match poq#xpr_buffer_offset_size 1 inv1index x1 with
107111
| Some (gname, xsize, xoffset, deps) ->
108-
let vconstraint = XOp (XLt, [ XOp (XMinus, [ xsize ; xoffset ]) ; x2 ]) in
109-
let safeconstraint = XOp (XGe, [ XOp (XMinus, [ xsize ; xoffset ]) ; x2 ]) in
112+
let vconstraint = XOp (XLt, [XOp (XMinus, [xsize; xoffset]); x2]) in
113+
let safeconstraint = XOp (XGe, [XOp (XMinus, [xsize; xoffset]); x2]) in
110114
let sconstraint = simplify_xpr vconstraint in
111115
if is_true sconstraint then
112-
let msg = "buffer: " ^ gname ^ " has size: " ^ (x2s xsize) ^ " and offset: "
113-
^ (x2s xoffset) ^ ", which violates safety constraint: "
114-
^ (x2s safeconstraint) in
115-
Some (deps,msg)
116+
let msg =
117+
Printf.sprintf
118+
("buffer: %s has size: %s and offset: %s, which violates safety "
119+
^^ "constraint: %s")
120+
gname
121+
(x2s xsize)
122+
(x2s xoffset)
123+
(x2s safeconstraint) in
124+
Some (deps, msg)
116125
else
117126
None
118127
| _ -> None
119128

120-
method private inv_implies_violation inv1 inv2 =
129+
method private inv_implies_violation (inv1: invariant_int) (inv2: invariant_int) =
121130
match (inv1#expr,inv2#upper_bound_xpr) with
122131
| (Some x1, Some x2) -> self#xpr_implies_violation inv1#index inv2#index x1 x2
123132
| _ -> None
124-
133+
125134
method check_violation =
126135
match (invs1,invs2) with
127136
| ([],_) | (_,[]) -> false
@@ -133,17 +142,17 @@ object (self)
133142
match self#inv_implies_violation inv1 inv2 with
134143
| Some (deps,msg) ->
135144
begin
136-
poq#record_violation_result deps msg ;
145+
poq#record_violation_result deps msg;
137146
true
138147
end
139148
| _ -> false) acc1 invs2) false invs1
140-
149+
141150
(* ----------------------- delegation ------------------------------------- *)
142151
method check_delegation = false
143152
end
144153

145154

146-
let check_buffer (poq:po_query_int) (e1:exp) (e2:exp) =
155+
let check_buffer (poq: po_query_int) (e1: exp) (e2: exp) =
147156
let invs1 = poq#get_invariants 1 in
148157
let invs2 = poq#get_invariants 2 in
149158
let _ = poq#set_diagnostic_invariants 1 in

‎CodeHawk/CHC/cchanalyze/cCHPOCheckCast.ml‎

Lines changed: 16 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,23 @@
11
(* =============================================================================
2-
CodeHawk C Analyzer
2+
CodeHawk C Analyzer
33
Author: Henny Sipma
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
6-
6+
77
Copyright (c) 2005-2019 Kestrel Technology LLC
8+
Copyright (c) 2020-2024 Henny B. Sipma
9+
Copyright (c) 2024 Aarno Labs LLC
810
911
Permission is hereby granted, free of charge, to any person obtaining a copy
1012
of this software and associated documentation files (the "Software"), to deal
1113
in the Software without restriction, including without limitation the rights
1214
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1315
copies of the Software, and to permit persons to whom the Software is
1416
furnished to do so, subject to the following conditions:
15-
17+
1618
The above copyright notice and this permission notice shall be included in all
1719
copies or substantial portions of the Software.
18-
20+
1921
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
2022
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
2123
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
@@ -25,48 +27,24 @@
2527
SOFTWARE.
2628
============================================================================= *)
2729

28-
(* chlib *)
29-
open CHNumerical
30-
open CHPretty
31-
32-
(* chutil *)
33-
open CHLogger
34-
open CHPrettyUtil
35-
36-
(* xprlib *)
37-
open Xprt
38-
open XprToPretty
39-
open Xsimplify
40-
30+
4131
(* cchlib *)
4232
open CCHBasicTypes
43-
open CCHFunctionSummary
44-
open CCHLibTypes
45-
open CCHTypesUtil
46-
open CCHTypesToPretty
4733

4834
(* cchpre *)
49-
open CCHCheckImplication
50-
open CCHCheckValid
51-
open CCHPOPredicate
5235
open CCHPreTypes
53-
open CCHProofObligation
54-
36+
5537
(* cchanalyze *)
5638
open CCHAnalysisTypes
5739

58-
let x2p = xpr_formatter#pr_expr
59-
let p2s = pretty_to_string
60-
let x2s x = p2s (x2p x)
61-
let e2s e = p2s (exp_to_pretty e)
62-
40+
6341
class cast_checker_t
64-
(poq:po_query_int)
65-
(tfrom:typ)
66-
(tto:typ)
67-
(e:exp)
68-
(invs:invariant_int list) =
69-
object (self)
42+
(_poq: po_query_int)
43+
(_tfrom: typ)
44+
(_tto: typ)
45+
(_e: exp)
46+
(_invs: invariant_int list) =
47+
object
7048
(* ----------------------------- safe ------------------------------------- *)
7149
method check_safe = false
7250
(* ----------------------- violation -------------------------------------- *)
@@ -76,7 +54,7 @@ object (self)
7654
end
7755

7856

79-
let check_cast (poq:po_query_int) (tfrom:typ) (tto:typ) (e:exp) =
57+
let check_cast (poq: po_query_int) (tfrom: typ) (tto: typ) (e: exp) =
8058
let invs = poq#get_invariants 3 in
8159
let _ = poq#set_diagnostic_invariants 3 in
8260
let checker = new cast_checker_t poq tfrom tto e invs in

0 commit comments

Comments
 (0)