Source file aorai_visitors.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
open Automaton_ast
open Extlib
open Logic_const
open Cil_types
open Cil
let dkey = Aorai_option.register_category "action"
module Aux_funcs =
struct
type kind =
| Not_aux_func
| Aux of kernel_function
| Pre of kernel_function
| Post of kernel_function
module Table = Cil_datatype.Varinfo.Hashtbl
let table = Table.create 17
let add vi kind =
Table.add table vi kind
let add_aux kf vi =
add vi (Aux kf)
let kind vi =
try Table.find table vi with Not_found -> Not_aux_func
let iter f =
Table.iter f table
end
let mk_auto_fct_block kf_aux kf status auto_state res =
let loc = Kernel_function.get_location kf in
Aorai_utils.auto_func_block kf_aux loc kf status auto_state res
let mk_pre_fct_block kf_pre kf =
mk_auto_fct_block
kf_pre
kf
Automaton_ast.Call
(Data_for_aorai.get_kf_init_state kf)
None
let mk_post_fct_block kf_post kf res =
mk_auto_fct_block
kf_post
kf
Automaton_ast.Return
(Data_for_aorai.get_kf_return_state kf)
res
class change_formals old_kf new_kf =
let old_formals = Kernel_function.get_formals old_kf in
let new_formals = Kernel_function.get_formals new_kf in
let formals = List.combine old_formals new_formals in
object
inherit Visitor.frama_c_inplace
method! vlogic_var_use lv =
match lv.lv_origin with
| None -> SkipChildren
| Some vi ->
try
let vi'= List.assq vi formals in
ChangeTo (Cil.cvar_to_lvar vi')
with Not_found -> SkipChildren
method! vvrbl vi =
try
let vi' = List.assq vi formals in
ChangeTo vi'
with Not_found -> SkipChildren
end
class change_result new_kf =
let v = List.hd (Kernel_function.get_formals new_kf) in
object
inherit Visitor.frama_c_inplace
method! vterm_lhost lh =
match lh with
TResult _ -> ChangeTo (TVar (Cil.cvar_to_lvar v))
| _ -> DoChildren
end
(**
This visitor adds an auxiliary function for each C function which takes
care of setting the automaton in a correct state before calling the
original one, and replaces each occurrence of the original function by
the auxiliary one. It also takes care of changing the automaton at function's
return.
*)
class visit_adding_code_for_synchronisation =
object (self)
inherit Visitor.frama_c_inplace
val aux_post_table = Kernel_function.Hashtbl.create 17
method do_fundec fundec loc =
let kf = Option.get self#current_kf in
let vi = Kernel_function.get_vi kf in
let vi_pre = Cil_const.copy_with_new_vid vi in
vi_pre.vname <- Data_for_aorai.get_fresh (vi_pre.vname ^ "_pre_func");
vi_pre.vdefined <- true;
vi_pre.vghost <- true;
Aux_funcs.(add vi_pre (Pre kf));
let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
vi_pre.vattr <- [];
let arg =
if Cil.isVoidType rettype
then []
else ["res",rettype,[]]
in
let vi_post =
Cil.makeGlobalVar ~ghost:true
(Data_for_aorai.get_fresh (vi.vname ^ "_post_func"))
(TFun(voidType,Some arg,false,[]))
in
Kernel_function.Hashtbl.add aux_post_table kf vi_post;
Aux_funcs.(add vi_post (Post kf));
let fun_dec_pre = Cil.emptyFunctionFromVI vi_pre in
let fun_dec_post = Cil.emptyFunctionFromVI vi_post in
Cil.setFunctionTypeMakeFormals
fun_dec_pre (TFun(Cil.voidType, args, varargs,[]));
Cil.setFunctionTypeMakeFormals
fun_dec_post (TFun(voidType,Some arg,false,[]));
Globals.Functions.replace_by_definition
(Cil.empty_funspec()) fun_dec_pre loc;
Globals.Functions.replace_by_definition
(Cil.empty_funspec()) fun_dec_post loc;
let kf_pre = Globals.Functions.get vi_pre in
let kf_post = Globals.Functions.get vi_post in
let aux_func_pre, pre_block,pre_locals = mk_pre_fct_block kf_pre kf in
let aux_func_post, post_block,post_locals =
mk_post_fct_block
kf_post kf (Extlib.opt_of_list fun_dec_post.sformals)
in
let vis = new change_formals kf kf_pre in
fun_dec_pre.slocals <- pre_locals;
fun_dec_pre.sbody <- Visitor.visitFramacBlock vis pre_block;
fun_dec_pre.svar.vdefined <- true;
fun_dec_post.slocals <- post_locals;
fun_dec_post.sbody <- post_block;
fun_dec_post.svar.vdefined <- true;
let aux_funcs =
Cil_datatype.Varinfo.Set.union aux_func_pre aux_func_post
in
let globs =
Cil_datatype.Varinfo.Set.fold
(fun x acc ->
GFunDecl(Cil.empty_funspec(),x,loc) :: acc) aux_funcs
[ GFun(fun_dec_pre,loc); GFun(fun_dec_post,loc)]
in
Cil_datatype.Varinfo.Set.iter (Aux_funcs.add_aux kf) aux_funcs;
fundec.sbody.bstmts <-
Cil.mkStmtOneInstr ~ghost:true
(Call(None,Cil.evar ~loc vi_pre,
List.map (fun x -> Cil.evar ~loc x)
(Kernel_function.get_formals kf),
loc))
:: fundec.sbody.bstmts;
let keepSwitch = Kernel.KeepSwitch.get() in
Cfg.prepareCFG ~keepSwitch fun_dec_pre;
Cfg.cfgFun fun_dec_pre;
Cfg.prepareCFG ~keepSwitch fun_dec_post;
Cfg.cfgFun fun_dec_post;
globs
method! vglob_aux g =
match g with
| GFun (fundec,loc) ->
let kf = Globals.Functions.get fundec.svar in
if Data_for_aorai.isObservableFunction kf then
let globs = self#do_fundec fundec loc in
ChangeDoChildrenPost([g], fun x -> globs @ x)
else
DoChildren
| _ -> DoChildren
method! vstmt_aux stmt =
match stmt.skind with
| Return (res,loc) ->
let kf = Option.get self#current_kf in
if Data_for_aorai.isObservableFunction kf then begin
let args = match res with
| None -> []
| Some exp -> [Cil.copy_exp exp]
in
let aux_vi =
try Kernel_function.Hashtbl.find aux_post_table kf
with Not_found ->
Aorai_option.fatal
"Function %a has no associated post_func"
Kernel_function.pretty kf
in
let call =
mkStmtOneInstr
~ghost:true (Call (None,Cil.evar ~loc aux_vi,args,loc))
in
let new_return = mkStmt ~valid_sid:true stmt.skind in
let new_stmts = [call; new_return] in
stmt.skind<-Block(Cil.mkBlock(new_stmts))
end;
SkipChildren
| _ -> DoChildren
end
let post_treatment_loops = Hashtbl.create 97
let update_loop_assigns kf stmt state vi code_annot =
let loc = Cil_datatype.Stmt.loc stmt in
let assigns = Aorai_utils.aorai_assigns state loc in
let assigns =
Logic_utils.concat_assigns
(Writes
[Logic_const.new_identified_term (Logic_const.tvar ~loc vi), From []])
assigns
in
let new_assigns =
match code_annot.annot_content with
| AAssigns (bhvs,old_assigns) ->
Logic_const.new_code_annotation
(AAssigns (bhvs, Logic_utils.concat_assigns old_assigns assigns))
| _ -> Aorai_option.fatal "Expecting an assigns clause here"
in
Annotations.add_code_annot
~keep_empty:false Aorai_option.emitter ~kf stmt new_assigns
let get_action_post_cond kf ?init_trans return_states =
let to_consider pre_state int_states =
match init_trans with
| None -> true
| Some init_trans ->
try
let possible_states =
Data_for_aorai.Aorai_state.Map.find pre_state init_trans
in
not (Data_for_aorai.Aorai_state.Set.is_empty
(Data_for_aorai.Aorai_state.Set.inter
int_states possible_states))
with Not_found -> false
in
let treat_one_path pre_state post_state (int_states,_,bindings) acc =
if to_consider pre_state int_states then begin
let start = Logic_const.pre_label in
let post_conds =
Aorai_utils.action_to_pred ~start ~pre_state ~post_state bindings
in
Aorai_option.debug ~dkey
"Getting action post-conditions for %a, from state %s to state %s@\n%a"
Kernel_function.pretty kf
pre_state.Automaton_ast.name post_state.Automaton_ast.name
(Pretty_utils.pp_list ~sep:"@\n" Printer.pp_predicate)
post_conds;
post_conds @ acc
end
else acc
in
let treat_one_pre_state pre_state map acc =
Data_for_aorai.Aorai_state.Map.fold (treat_one_path pre_state) map acc
in
let post_cond =
Data_for_aorai.Aorai_state.Map.fold treat_one_pre_state return_states []
in
List.map
(fun post_cond -> (Normal, Logic_const.new_predicate post_cond))
post_cond
let make_zero_one_choice reachable_states =
let treat_one_state state _ acc =
(Logic_const.por
(Aorai_utils.is_state_pred state,
Aorai_utils.is_out_of_state_pred state)) :: acc
in
Data_for_aorai.Aorai_state.Map.fold treat_one_state reachable_states []
let needs_zero_one_choice states =
let needs_choice =
try
ignore
(Data_for_aorai.Aorai_state.Map.fold
(fun _ _ flag -> if flag then raise Exit else true)
states false);
false
with Exit -> true
in
if needs_choice then
List.map
Logic_const.new_predicate
(make_zero_one_choice states)
else []
let pred_reachable reachable_states =
let treat_one_state (nb, reachable, unreachable) state =
if Data_for_aorai.Aorai_state.Map.mem state reachable_states then
(nb+1,
Logic_const.por (reachable, Aorai_utils.is_state_pred state),
unreachable)
else
(nb, reachable,
Logic_const.pand (unreachable, Aorai_utils.is_out_of_state_pred state))
in
let (states,_) = Data_for_aorai.getGraph () in
let (nb, reachable, unreachable) =
List.fold_left treat_one_state (0,pfalse,ptrue) states
in
(nb > 1, reachable, unreachable)
let possible_start kf (start,int) =
let auto = Data_for_aorai.getGraph () in
let trans = Path_analysis.get_edges start int auto in
let treat_one_trans cond tr =
Logic_const.por
(cond, Aorai_utils.crosscond_to_pred tr.cross kf Automaton_ast.Call)
in
let cond =
if Data_for_aorai.isObservableFunction kf then
List.fold_left treat_one_trans Logic_const.pfalse trans
else Logic_const.ptrue
in
Logic_const.pand (Aorai_utils.is_state_pred start, cond)
let neg_trans kf trans =
let auto = Data_for_aorai.getGraph () in
let rec aux l acc =
match l with
| [] -> acc
| (start,stop) :: l ->
let same_start, rest =
List.fold_left
(fun (same_start, rest) (start', stop' as elt) ->
if Data_for_aorai.Aorai_state.equal start start' then
stop' :: same_start, rest
else
same_start, elt :: rest)
([stop],[]) l
in
let cond =
if Data_for_aorai.isObservableFunction kf then begin
let cond =
List.fold_left
(fun cond stop ->
let trans = Path_analysis.get_edges start stop auto in
List.fold_left
(fun cond tr ->
Logic_simplification.tand
cond (Logic_simplification.tnot tr.cross))
cond trans)
TTrue same_start
in
let cond = fst (Logic_simplification.simplifyCond cond) in
Aorai_utils.crosscond_to_pred cond kf Automaton_ast.Call
end else Logic_const.pfalse
in
let cond =
Logic_const.por (Aorai_utils.is_out_of_state_pred start, cond)
in
aux rest (Logic_const.pand (acc,cond))
in
aux trans Logic_const.ptrue
let get_unchanged_aux_var loc current_state =
let partition_action state (_,_,map) (actions,possible_states) =
let possible_states =
Data_for_aorai.Aorai_state.Set.add state possible_states
in
let treat_one_action t _ acc =
let states =
try Cil_datatype.Term.Map.find t acc
with Not_found -> Data_for_aorai.Aorai_state.Set.empty
in
Cil_datatype.Term.Map.add t
(Data_for_aorai.Aorai_state.Set.add state states) acc
in
let actions =
Cil_datatype.Term.Map.fold treat_one_action map actions
in (actions,possible_states)
in
let treat_one_action pre_hyp possible_states t action_states acc =
if not (Data_for_aorai.Aorai_state.Set.is_empty
(Data_for_aorai.Aorai_state.Set.diff
possible_states action_states))
then begin
let post_hyp =
Data_for_aorai.Aorai_state.Set.fold
(fun st acc ->
Logic_const.pand ~loc (acc,Aorai_utils.is_out_of_state_pred st))
action_states Logic_const.ptrue
in
let pred =
Logic_const.new_predicate
(Logic_const.pimplies ~loc
(pre_hyp,
Logic_const.pimplies ~loc
(post_hyp,
Logic_const.prel ~loc (Req,t,Logic_const.told ~loc t))))
in
(Normal,pred) :: acc
end else acc
in
let treat_one_pre_state start map acc =
let pre_hyp = Logic_const.pold ~loc (Aorai_utils.is_state_pred start) in
let actions_map, possible_states =
Data_for_aorai.Aorai_state.Map.fold
partition_action map
(Cil_datatype.Term.Map.empty, Data_for_aorai.Aorai_state.Set.empty)
in
Cil_datatype.Term.Map.fold
(treat_one_action pre_hyp possible_states) actions_map acc
in
Data_for_aorai.Aorai_state.Map.fold treat_one_pre_state current_state []
(**
This visitor adds a specification to each function and to each loop,
according to specifications stored into Data_for_aorai.
*)
class visit_adding_pre_post_from_buch treatloops =
let predicate_to_invariant kf stmt pred =
let pred = Logic_const.toplevel_predicate pred in
Annotations.add_code_annot
Aorai_option.emitter
~kf
stmt
(Logic_const.new_code_annotation (AInvariant([],true,pred)));
in
let all_possible_states state =
let treat_one_state _ = Data_for_aorai.merge_end_state in
Data_for_aorai.Aorai_state.Map.fold
treat_one_state state Data_for_aorai.Aorai_state.Map.empty
in
let condition_to_invariant kf possible_states stmt =
let has_multiple_choice =
try
ignore
(Data_for_aorai.Aorai_state.Map.fold
(fun _ _ b -> if b then raise Exit else true)
possible_states false);
false
with Exit ->
true
in
let treat_one_state s =
if Data_for_aorai.Aorai_state.Map.mem s possible_states then begin
if has_multiple_choice then begin
let pred =
Logic_const.por
(Aorai_utils.is_state_pred s, Aorai_utils.is_out_of_state_pred s)
in
predicate_to_invariant kf stmt pred
end else begin
predicate_to_invariant kf stmt (Aorai_utils.is_state_pred s)
end
end else begin
let pred = Aorai_utils.is_out_of_state_pred s in
predicate_to_invariant kf stmt pred
end
in
let (states,_) = Data_for_aorai.getGraph () in
List.iter treat_one_state states;
if has_multiple_choice then begin
let add_possible_state state _ acc =
if Data_for_aorai.is_reject_state state then acc
else
Logic_const.por (acc,Aorai_utils.is_state_pred state)
in
let pred =
Data_for_aorai.Aorai_state.Map.fold
add_possible_state possible_states Logic_const.pfalse
in
predicate_to_invariant kf stmt pred
end
in
let impossible_states_preds_inv start possible_states my_state =
let treat_one_start_state state start_state end_states acc =
if Data_for_aorai.Aorai_state.Map.mem state end_states then
Logic_const.pand
(acc,
Logic_const.pat(Aorai_utils.is_out_of_state_pred start_state, start))
else acc
in
let treat_one_state state _ acc =
let out_states =
Data_for_aorai.Aorai_state.Map.fold
(treat_one_start_state state) my_state Logic_const.ptrue
in
if Data_for_aorai.Aorai_state.Map.cardinal my_state = 1 &&
not (Logic_utils.is_trivially_true out_states)
then acc
else
Logic_const.pimplies
(out_states, Aorai_utils.is_out_of_state_pred state)
::acc
in
Data_for_aorai.Aorai_state.Map.fold treat_one_state possible_states []
in
let partition_pre_state map =
let (states,_) = Data_for_aorai.getGraph () in
let is_equiv st1 st2 =
let check_one _ o1 o2 =
match o1, o2 with
| None, None | Some _, Some _ -> Some ()
| None, Some _ | Some _, None -> raise Not_found
in
try
ignore (Data_for_aorai.Aorai_state.Map.merge check_one st1 st2); true
with Not_found -> false
in
let find_equivs (start,state, end_states) equivs =
let rec aux = function
| [] -> [[start,state],end_states]
| (equiv_class,end_states2 as infos) :: l ->
if is_equiv end_states end_states2 then
((start, state) :: equiv_class, end_states2) :: l
else infos :: aux l
in aux equivs
in
let filter equivs state =
let check_one_state start end_states equivs =
let end_states =
Data_for_aorai.Aorai_state.Map.filter
(fun _ (int_states,_,_) ->
Data_for_aorai.Aorai_state.Set.mem state int_states)
end_states
in
if Data_for_aorai.Aorai_state.Map.is_empty end_states then equivs
else find_equivs (start, state, end_states) equivs
in
Data_for_aorai.Aorai_state.Map.fold check_one_state map equivs
in
let res = List.fold_left filter [] states in
List.map fst res
in
let update_assigns loc kf ki spec =
let update_assigns bhv =
let assigns =
Aorai_utils.aorai_assigns (Data_for_aorai.get_kf_return_state kf) loc
in
match ki with
| Kstmt stmt ->
if bhv.b_assigns <> WritesAny then begin
let bhv_aorai = Cil.mk_behavior ~name:bhv.b_name ~assigns () in
let spec = Cil.empty_funspec () in
spec.spec_behavior <- [ bhv_aorai ];
let ca = Logic_const.new_code_annotation (AStmtSpec ([],spec)) in
Annotations.add_code_annot Aorai_option.emitter ~kf stmt ca
end
| Kglobal ->
Annotations.add_assigns
~keep_empty:true
Aorai_option.emitter
kf
~behavior:bhv.b_name
assigns;
in
List.iter update_assigns spec.spec_behavior
in
let mk_auto_fct_spec kf status auto_state =
let loc = Kernel_function.get_location kf in
Aorai_utils.auto_func_behaviors loc kf status auto_state
in
let mk_pre_fct_spec kf =
mk_auto_fct_spec kf Automaton_ast.Call (Data_for_aorai.get_kf_init_state kf)
in
let mk_post_fct_spec kf =
mk_auto_fct_spec kf
Automaton_ast.Return (Data_for_aorai.get_kf_return_state kf)
in
let needs_post kf =
let loc = Kernel_function.get_location kf in
let return_state = Data_for_aorai.get_kf_return_state kf in
let possible_states =
Data_for_aorai.Aorai_state.Map.fold
(fun _ map acc ->
Data_for_aorai.Aorai_state.Map.fold
(fun st _ acc -> Data_for_aorai.Aorai_state.Set.add st acc)
map acc)
return_state Data_for_aorai.Aorai_state.Set.empty
in
let action_post = get_unchanged_aux_var loc return_state in
if
Data_for_aorai.Aorai_state.Set.exists
Data_for_aorai.is_reject_state possible_states
then
let cond =
Data_for_aorai.Aorai_state.Set.fold
(fun st acc ->
if Data_for_aorai.is_reject_state st then acc
else Logic_const.por (Aorai_utils.is_state_pred st,acc))
possible_states Logic_const.pfalse
in
(Normal,Logic_const.new_predicate cond) :: action_post
else action_post
in
let mk_post kf =
let return_state = Data_for_aorai.get_kf_return_state kf in
let equivs = partition_pre_state return_state in
let mk_post_cond ?init_trans has_other_bhvs reachable_states =
let (multi_choice, reachable, unreachable) =
pred_reachable reachable_states
in
let post_cond = Normal, Logic_const.new_predicate reachable in
let post_cond =
if Aorai_option.Deterministic.get () || has_other_bhvs then [post_cond]
else
[Normal, Logic_const.new_predicate unreachable; post_cond]
in
let post_cond =
if multi_choice && not (Aorai_option.Deterministic.get ()) then
begin
let preds = make_zero_one_choice reachable_states in
List.fold_left
(fun acc p ->
(Normal, Logic_const.new_predicate p) :: acc)
post_cond preds
end
else post_cond
in
let post_cond =
if Data_for_aorai.isObservableFunction kf then begin
let infos = Aorai_utils.get_preds_post_bc_wrt_params kf in
if Logic_utils.is_trivially_true infos then post_cond
else (Normal, Logic_const.new_predicate infos) :: post_cond
end else post_cond
in
post_cond @ get_action_post_cond kf ?init_trans return_state
in
let bhvs =
match equivs with
| [ e ] ->
let name = "Buchi_property_behavior" in
let s = fst (List.hd e) in
let reachable_states =
Data_for_aorai.Aorai_state.Map.find s return_state
in
let post_cond = mk_post_cond false reachable_states in
[Cil.mk_behavior ~name ~post_cond ()]
| _ ->
let _,bhvs =
List.fold_left
(fun (i,acc) equiv ->
let (case_start, case_int) = List.hd equiv in
let assumes_l =
List.map (possible_start kf) equiv
in
let name = "Buchi_behavior_in_" ^ (string_of_int i) in
let assumes =
[Logic_const.new_predicate (Logic_const.pors assumes_l)]
in
let reachable_states =
Data_for_aorai.Aorai_state.Map.find case_start return_state
in
let reachable_states =
Data_for_aorai.Aorai_state.Map.filter
(fun _ (int,_,_) ->
Data_for_aorai.Aorai_state.Set.mem case_int int)
reachable_states
in
let init_trans =
List.fold_left
(fun acc (start, int) ->
let set =
try Data_for_aorai.Aorai_state.Map.find start acc
with Not_found -> Data_for_aorai.Aorai_state.Set.empty
in
Data_for_aorai.Aorai_state.Map.add
start
(Data_for_aorai.Aorai_state.Set.add int set)
acc)
Data_for_aorai.Aorai_state.Map.empty
equiv
in
let post_cond = mk_post_cond ~init_trans true reachable_states in
(i+1,
Cil.mk_behavior ~name ~assumes ~post_cond () :: acc))
(0,[])
equivs
in
if Aorai_option.Deterministic.get () then bhvs
else begin
let aux (i,bhvs) state =
let name = "Buchi_behavior_out_" ^ (string_of_int i) in
let select_equivalence_class equiv =
let (start, int) = List.hd equiv in
try
let map =
Data_for_aorai.Aorai_state.Map.find start return_state
in
let (int_states, _,_) =
Data_for_aorai.Aorai_state.Map.find state map
in
Data_for_aorai.Aorai_state.Set.mem int int_states
with Not_found -> false
in
let my_trans =
List.fold_left
(fun acc equiv ->
if select_equivalence_class equiv then
acc @ equiv
else acc)
[] equivs
in
let assumes = neg_trans kf my_trans in
if Logic_utils.is_trivially_false assumes then (i+1,bhvs)
else
let p = Aorai_utils.is_out_of_state_pred state in
let post_cond = [Normal, Logic_const.new_predicate p] in
let bhv =
if Logic_utils.is_trivially_true assumes then
Cil.mk_behavior ~name ~post_cond ()
else begin
let assumes = [Logic_const.new_predicate assumes] in
Cil.mk_behavior ~name ~assumes ~post_cond ()
end
in
(i+1,bhv :: bhvs)
in
let (states,_) = Data_for_aorai.getGraph () in
List.rev (snd (List.fold_left aux (0,bhvs) states))
end
in
let bhvs =
if Aorai_option.ConsiderAcceptance.get () &&
Datatype.String.equal
(Kernel_function.get_name kf) (Kernel.MainFunction.get())
then
Aorai_utils.mk_acceptance_bhv () :: bhvs
else bhvs
in
if Aorai_option.AddingOperationNameAndStatusInSpecification.get()
then begin
let called_post =
Logic_const.new_predicate
(Logic_const.prel
(Req ,
Logic_const.tvar
(Data_for_aorai.get_logic_var Data_for_aorai.curOpStatus),
Logic_const.term
(TConst
(Logic_utils.constant_to_lconstant
(Data_for_aorai.op_status_to_cenum Automaton_ast.Return)))
(Ctype Cil.intType)))
in
let called_post_2 =
Logic_const.new_predicate
(Logic_const.prel
(Req,
Logic_const.tvar
(Data_for_aorai.get_logic_var Data_for_aorai.curOp),
Logic_const.term
(TConst
(Logic_utils.constant_to_lconstant
(Data_for_aorai.func_to_cenum
(Kernel_function.get_name kf))))
(Ctype Cil.intType)))
in
let name = "Buchi_property_behavior_function_states" in
let post_cond = [Normal, called_post; Normal, called_post_2] in
Cil.mk_behavior ~name ~post_cond () :: bhvs
end else bhvs
in
object(self)
inherit Visitor.frama_c_inplace
val has_call = Stack.create ()
method private enter_block () = Stack.push (ref false) has_call
method private call () = Stack.iter (fun x -> x := true) has_call
method private leave_block () = !(Stack.pop has_call)
method! vfunc f =
let my_kf = Option.get self#current_kf in
let vi = Kernel_function.get_vi my_kf in
Populate_spec.populate_funspec my_kf [`Assigns];
let spec = Annotations.funspec my_kf in
let loc = Kernel_function.get_location my_kf in
(match Aux_funcs.kind vi with
| Aux_funcs.Pre _ | Post _ | Aux _ -> ()
| Not_aux_func ->
let bhvs = mk_post my_kf in
let my_state = Data_for_aorai.get_kf_init_state my_kf in
let requires = needs_zero_one_choice my_state in
let requires =
if Data_for_aorai.isObservableFunction my_kf then
Aorai_utils.auto_func_preconditions
loc my_kf Automaton_ast.Call my_state
@ requires
else requires
in
let post_cond = needs_post my_kf in
match Cil.find_default_behavior spec with
| Some b ->
let behavior = b.b_name in
Annotations.add_requires
Aorai_option.emitter my_kf ~behavior requires;
Annotations.add_ensures
Aorai_option.emitter my_kf ~behavior post_cond;
Annotations.add_behaviors Aorai_option.emitter my_kf bhvs
| None ->
let bhv = Cil.mk_behavior ~requires ~post_cond () in
Annotations.add_behaviors Aorai_option.emitter my_kf (bhv :: bhvs));
let after f = update_assigns f.svar.vdecl my_kf Kglobal spec; f in
ChangeDoChildrenPost(f,after)
method! vglob_aux g =
match g with
| GFun _ ->
let my_kf = Option.get self#current_kf in
let vi = Kernel_function.get_vi my_kf in
(match Aux_funcs.kind vi with
| Aux_funcs.Pre kf ->
let bhvs = mk_pre_fct_spec kf in
let vis = new change_formals kf my_kf in
let bhvs =
Visitor.visitFramacBehaviors vis bhvs
in
Annotations.add_behaviors Aorai_option.emitter my_kf bhvs;
SkipChildren
| Post kf ->
let (rt, _, _, _) =
Cil.splitFunctionTypeVI (Kernel_function.get_vi kf)
in
let bhvs = mk_post_fct_spec kf in
let bhvs =
if Cil.isVoidType rt then bhvs
else (Visitor.visitFramacBehaviors
(new change_result my_kf)
bhvs;)
in
Annotations.add_behaviors Aorai_option.emitter my_kf bhvs;
SkipChildren
| Aux _ | Not_aux_func ->
DoChildren )
| _ -> DoChildren;
method! vstmt_aux stmt =
let kf = Option.get self#current_kf in
let treat_loop body_ref stmt =
let init_state = Data_for_aorai.get_loop_init_state stmt in
let inv_state = Data_for_aorai.get_loop_invariant_state stmt in
let possible_states =
Data_for_aorai.merge_end_state
(all_possible_states init_state) (all_possible_states inv_state)
in
let loop_assigns =
Annotations.code_annot ~filter:Logic_utils.is_assigns stmt
in
let vi_init =
Data_for_aorai.get_varinfo
(Data_for_aorai.loopInit ^ "_" ^ string_of_int stmt.sid)
in
let loc = Cil_datatype.Stmt.loc stmt in
let stmt_varset =
Cil.mkStmtOneInstr ~ghost:true ~valid_sid:true
(Set((Var vi_init,NoOffset), Cil.zero ~loc, loc))
in
begin
try
let rec skipEmpty = function
[] -> []
| {skind=Instr (Skip _);labels=[]} :: rest -> skipEmpty rest
| x -> x
in
match skipEmpty !body_ref.bstmts with
| {skind=If(_,tb,fb,_)} as head:: _ ->
begin
match skipEmpty tb.bstmts, skipEmpty fb.bstmts with
| _, {skind=Break _}:: _
| _, {skind=Goto _} :: _
| {skind=Goto _} :: _, _
| {skind=Break _} :: _, _ ->
!body_ref.bstmts <-
head :: stmt_varset :: List.tl !body_ref.bstmts
| _ ->
raise Not_found
end
| _ -> raise Not_found
with Not_found ->
!body_ref.bstmts<-stmt_varset::!body_ref.bstmts
end;
let new_loop = mkStmt ~valid_sid:true stmt.skind in
let stmt_varset =
Cil.mkStmtOneInstr ~ghost:true ~valid_sid:true
(Set((Var(vi_init),NoOffset), Cil.one ~loc, loc))
in
let block = mkBlock [stmt_varset;new_loop] in
stmt.skind<-Block(block);
new_loop.labels <-
[ Label ("aorai_loop_" ^ string_of_int stmt.sid,
Cil_datatype.Stmt.loc stmt, false)];
let loop_entry_label = StmtLabel (ref new_loop) in
let mk_imply operator predicate =
pimplies
(prel(operator,
Aorai_utils.mk_term_from_vi vi_init,
Cil.lzero()),
predicate)
in
condition_to_invariant kf possible_states new_loop;
let init_preds =
impossible_states_preds_inv
Logic_const.pre_label possible_states init_state
in
let treat_init_pred pred =
let pred = mk_imply Rneq pred in
predicate_to_invariant kf new_loop pred
in
List.iter treat_init_pred init_preds;
let invariant_preds =
impossible_states_preds_inv loop_entry_label possible_states inv_state
in
let treat_inv_pred pred =
let pred = mk_imply Req pred in
predicate_to_invariant kf new_loop pred
in
List.iter treat_inv_pred invariant_preds;
let action_inv_preds =
Aorai_utils.all_actions_preds loop_entry_label inv_state
in
List.iter (predicate_to_invariant kf new_loop) action_inv_preds;
List.iter
(update_loop_assigns kf new_loop inv_state (Cil.cvar_to_lvar vi_init))
loop_assigns;
Hashtbl.add post_treatment_loops (ref stmt) (ref new_loop);
stmt
in
self#enter_block ();
let after s =
if self#leave_block () then
let annots = Annotations.code_annot stmt in
let _, specs = List.split (Logic_utils.extract_contract annots) in
List.iter
(update_assigns
(Cil_datatype.Stmt.loc stmt)
(Option.get self#current_kf)
(Kstmt stmt))
specs;
s
else
s
in
if treatloops then
match stmt.skind with
| Loop (_,block,_,_,_) ->
ChangeDoChildrenPost(stmt, after $ (treat_loop (ref block)))
| _ -> ChangeDoChildrenPost(stmt, after)
else
ChangeDoChildrenPost(stmt,after)
method! vinst = function
| Call _ | Local_init (_, ConsInit _, _) -> self#call (); DoChildren
| _ -> DoChildren
end
let add_pre_post_from_buch file treatloops =
let visitor = new visit_adding_pre_post_from_buch treatloops in
Cil.visitCilFile (visitor :> Cil.cilVisitor) file;
Hashtbl.iter
(fun old_stmt new_stmt ->
let new_s = !new_stmt in
let old_s = !old_stmt in
let kf = Kernel_function.find_englobing_kf old_s in
let annots =
Annotations.fold_code_annot
(fun e a acc ->
Annotations.remove_code_annot e ~kf old_s a;
if (Logic_utils.is_assigns a) then acc else (e, a) :: acc)
old_s
[];
in
List.iter (fun (e, a) -> Annotations.add_code_annot e ~kf new_s a) annots)
post_treatment_loops
let add_sync_with_buch file =
let visitor = new visit_adding_code_for_synchronisation in
Cil.visitCilFile (visitor :> Cil.cilVisitor) file