Skip to content

Commit 6fdc646

Browse files
ZippeyKeys12ZippeyKeys12
committed
Generate wrappers for testing static functions
1 parent 2ebfed4 commit 6fdc646

27 files changed

+449
-184
lines changed

‎bin/common.ml‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -261,6 +261,27 @@ let handle_error_with_user_guidance ~(label : string) (e : exn) : unit =
261261
exit 1
262262

263263

264+
let static_funcs (cabs_tunit : CF.Cabs.translation_unit) : string list =
265+
let (CF.Cabs.TUnit decls) = cabs_tunit in
266+
List.filter_map
267+
(fun decl ->
268+
match decl with
269+
| CF.Cabs.EDecl_func
270+
(FunDef
271+
( _,
272+
_,
273+
{ storage_classes; _ },
274+
Declarator
275+
(_, DDecl_function (DDecl_identifier (_, Identifier (_, fsym)), _)),
276+
_ ))
277+
when List.exists
278+
(fun scs -> match scs with CF.Cabs.SC_static -> true | _ -> false)
279+
storage_classes ->
280+
Some fsym
281+
| _ -> None)
282+
decls
283+
284+
264285
open Cmdliner
265286

266287
let (dir_and_mk_if_not_exist :

‎bin/instrument.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ let generate_executable_specs
131131
~magic_comment_char_dollar (* Callbacks *)
132132
~save_cpp:(Some pp_file)
133133
~handle_error
134-
~f:(fun ~cabs_tunit:_ ~prog5 ~ail_prog ~statement_locs:_ ~paused:_ ->
134+
~f:(fun ~cabs_tunit ~prog5 ~ail_prog ~statement_locs:_ ~paused:_ ->
135135
if run && Option.is_none prog5.main then (
136136
print_endline "Tried running instrumented file (`--run`) without `main` function.";
137137
exit 1);
@@ -146,6 +146,7 @@ let generate_executable_specs
146146
filename
147147
pp_file
148148
out_file
149+
(Common.static_funcs cabs_tunit)
149150
ail_prog
150151
prog5
151152
with

‎bin/seqTest.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,7 @@ let run_seq_tests
8383
filename
8484
pp_file
8585
out_file
86+
(Common.static_funcs cabs_tunit)
8687
ail_prog
8788
prog5;
8889
let config : SeqTests.seq_config =

‎bin/test.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -142,6 +142,7 @@ let run_tests
142142
filename
143143
pp_file
144144
out_file
145+
(Common.static_funcs cabs_tunit)
145146
ail_prog
146147
prog5
147148
with

‎lib/bugExplanation/bugExplanation.mli‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,12 @@ val synthesize_replicators
55
: string ->
66
CF.GenTypes.genTypeCategory A.sigma ->
77
unit Mucore.file ->
8-
Fulminate.Extract.instrumentation list ->
8+
(bool * Fulminate.Extract.instrumentation) list ->
99
(A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list
1010

1111
val synthesize_shape_analyzers
1212
: string ->
1313
CF.GenTypes.genTypeCategory A.sigma ->
1414
unit Mucore.file ->
15-
Fulminate.Extract.instrumentation list ->
15+
(bool * Fulminate.Extract.instrumentation) list ->
1616
(A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list

‎lib/bugExplanation/replicators.ml‎

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -645,11 +645,18 @@ let compile_spec
645645
filename
646646
(sigma : CF.GenTypes.genTypeCategory A.sigma)
647647
(prog5 : unit Mucore.file)
648+
(is_static : bool)
648649
(sym : Sym.t)
649650
(at : 'a AT.t)
650651
: A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition
651652
=
652-
let fsym = pred_sym sym in
653+
let fsym =
654+
pred_sym
655+
(if is_static then
656+
Sym.fresh (Fulminate.Utils.static_prefix filename ^ "_" ^ Sym.pp_string sym)
657+
else
658+
sym)
659+
in
653660
let args =
654661
match List.assoc Sym.equal sym sigma.declarations with
655662
| _, _, Decl_function (_, _, args, _, _, _) ->
@@ -833,7 +840,7 @@ let synthesize
833840
filename
834841
(sigma : CF.GenTypes.genTypeCategory A.sigma)
835842
(prog5 : unit Mucore.file)
836-
(insts : Fulminate.Extract.instrumentation list)
843+
(insts : (bool * Fulminate.Extract.instrumentation) list)
837844
: (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list
838845
=
839846
(* Per type *)
@@ -848,6 +855,7 @@ let synthesize
848855
let module SctypesSet = Set.Make (Sctypes) in
849856
let arg_types =
850857
insts
858+
|> List.map snd
851859
|> List.filter (fun (inst : Fulminate.Extract.instrumentation) ->
852860
Option.is_some inst.internal)
853861
|> List.filter_map (fun (inst : Fulminate.Extract.instrumentation) ->
@@ -905,7 +913,10 @@ let synthesize
905913
(* Per specification *)
906914
let spec_replicators =
907915
insts
908-
|> List.filter_map (fun (inst : Fulminate.Extract.instrumentation) ->
909-
Option.map (fun lat -> compile_spec filename sigma prog5 inst.fn lat) inst.internal)
916+
|> List.filter_map
917+
(fun ((is_static, inst) : bool * Fulminate.Extract.instrumentation) ->
918+
Option.map
919+
(fun lat -> compile_spec filename sigma prog5 is_static inst.fn lat)
920+
inst.internal)
910921
in
911922
type_replicators @ pred_replicators @ spec_replicators

‎lib/bugExplanation/replicators.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ val synthesize
55
: string ->
66
CF.GenTypes.genTypeCategory A.sigma ->
77
unit Mucore.file ->
8-
Fulminate.Extract.instrumentation list ->
8+
(bool * Fulminate.Extract.instrumentation) list ->
99
(A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list

‎lib/bugExplanation/shapeAnalyzers.ml‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -355,11 +355,18 @@ let compile_spec
355355
filename
356356
(sigma : CF.GenTypes.genTypeCategory A.sigma)
357357
(prog5 : unit Mucore.file)
358+
(is_static : bool)
358359
(sym : Sym.t)
359360
(at : 'a AT.t)
360361
: A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition
361362
=
362-
let fsym = pred_sym sym in
363+
let fsym =
364+
pred_sym
365+
(if is_static then
366+
Sym.fresh (Fulminate.Utils.static_prefix filename ^ "_" ^ Sym.pp_string sym)
367+
else
368+
sym)
369+
in
363370
let args =
364371
match List.assoc Sym.equal sym sigma.declarations with
365372
| _, _, Decl_function (_, _, args, _, _, _) ->
@@ -427,7 +434,7 @@ let synthesize
427434
filename
428435
(sigma : CF.GenTypes.genTypeCategory A.sigma)
429436
(prog5 : unit Mucore.file)
430-
(insts : Fulminate.Extract.instrumentation list)
437+
(insts : (bool * Fulminate.Extract.instrumentation) list)
431438
: (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list
432439
=
433440
(* Per type *)
@@ -454,7 +461,10 @@ let synthesize
454461
(* Per specification *)
455462
let spec_analyzers =
456463
insts
457-
|> List.filter_map (fun (inst : Fulminate.Extract.instrumentation) ->
458-
Option.map (fun lat -> compile_spec filename sigma prog5 inst.fn lat) inst.internal)
464+
|> List.filter_map
465+
(fun ((is_static, inst) : bool * Fulminate.Extract.instrumentation) ->
466+
Option.map
467+
(fun lat -> compile_spec filename sigma prog5 is_static inst.fn lat)
468+
inst.internal)
459469
in
460470
type_analyzers @ pred_analyzers @ spec_analyzers

‎lib/bugExplanation/shapeAnalyzers.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ val synthesize
55
: string ->
66
CF.GenTypes.genTypeCategory A.sigma ->
77
unit Mucore.file ->
8-
Fulminate.Extract.instrumentation list ->
8+
(bool * Fulminate.Extract.instrumentation) list ->
99
(A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list

‎lib/fulminate/fulminate.ml‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,7 @@ let main
164164
filename
165165
in_filename (* WARNING: this file will be delted after this function *)
166166
out_filename
167+
(static_funcs : string list)
167168
((startup_sym_opt, (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma)) as
168169
ail_prog)
169170
prog5
@@ -193,6 +194,13 @@ let main
193194
let filtered_instrumentation, filtered_sigm =
194195
filter_selected_fns prog5 sigm full_instrumentation
195196
in
197+
let static_funcs =
198+
filtered_instrumentation
199+
|> List.filter (fun (inst : Extract.instrumentation) ->
200+
List.exists (String.equal (Sym.pp_string inst.fn)) static_funcs)
201+
|> List.map (fun (inst : Extract.instrumentation) -> inst.fn)
202+
|> Sym.Set.of_list
203+
in
196204
let filtered_ail_prog = (startup_sym_opt, filtered_sigm) in
197205
Records.populate_record_map filtered_instrumentation prog5;
198206
let executable_spec =
@@ -328,8 +336,10 @@ let main
328336
Source_injection.(
329337
output_injections
330338
oc
331-
{ filename = in_filename;
339+
{ orig_filename = filename;
340+
filename = in_filename;
332341
program = ail_prog;
342+
static_funcs;
333343
pre_post = pre_post_pairs;
334344
in_stmt = in_stmt_injs;
335345
returns = executable_spec.returns;

0 commit comments

Comments
 (0)