Source file value_requests.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
(** Server requests about the values inferred by the Eva analysis. *)
open Server
open Data
open Cil_types
module Kmap = Kernel_function.Hashtbl
module Smap = Cil_datatype.Stmt.Hashtbl
module CSet = Callstack.Set
module CSmap = Callstack.Hashtbl
module Md = Markdown
module Jdecl = Kernel_ast.Decl
module Jstmt = Kernel_ast.Stmt
module Jmarker = Kernel_ast.Marker
let package =
let title = "Values inferred by the Eva analysis" in
Package.package ~plugin:"eva" ~name:"values" ~title ()
type evaluation_point =
| Initial
| Pre of kernel_function
| Stmt of kernel_function * stmt
let post kf =
if Analysis.use_spec_instead_of_definition kf
then raise Not_found
else
try Stmt (kf, Kernel_function.find_return kf)
with Kernel_function.No_Statement -> raise Not_found
let request_at = function
| Initial -> Results.at_start
| Stmt (_, stmt) -> Results.before stmt
| Pre kf -> Results.at_start_of kf
let property_evaluation_point = function
| Property.IPCodeAnnot { ica_kf = kf; ica_stmt = stmt }
| IPPropertyInstance { ii_kf = kf; ii_stmt = stmt } -> Stmt (kf, stmt)
| IPPredicate {ip_kf; ip_kind = PKEnsures (_, Normal)} -> post ip_kf
| IPPredicate { ip_kf = kf;
ip_kind = PKRequires _ | PKAssumes _ | PKTerminates }
| IPAssigns {ias_kf = kf} | IPFrom {if_kf = kf} ->
Pre kf
| IPPredicate _ | IPComplete _ | IPDisjoint _ | IPDecrease _
| IPAxiomatic _ | IPModule _ | IPLemma _
| IPTypeInvariant _ | IPGlobalInvariant _
| IPOther _ | IPAllocation _ | IPReachable _ | IPExtended _ | IPBehavior _ ->
raise Not_found
let marker_evaluation_point = function
| Printer_tag.PGlobal _ -> Initial
| PStmt (kf, stmt) | PStmtStart (kf, stmt) -> Stmt (kf, stmt)
| PVDecl (kf, kinstr, v) when not (v.vformal || v.vglob) ->
begin
match kf, kinstr with
| Some kf, Kstmt ({skind = Instr (Local_init _)} as s) -> Stmt (kf, s)
| _ -> raise Not_found
end
| PLval (kf, ki, _) | PExp (kf, ki, _) | PVDecl (kf, ki, _) ->
begin
match kf, ki with
| Some kf, Kstmt stmt -> Stmt (kf, stmt)
| Some kf, Kglobal -> Pre kf
| None, Kglobal -> Initial
| None, Kstmt _ -> assert false
end
| PTermLval (_, _, prop, _) | PIP prop -> property_evaluation_point prop
| PType _ -> raise Not_found
let term_lval_to_lval kf tlval =
try
let result = Option.bind Eva_utils.find_return_var kf in
Logic_to_c.term_lval_to_lval ?result tlval
with Logic_to_c.No_conversion -> raise Not_found
let tag_varinfo_as_lval_at eval_point =
let kf, kinstr =
match eval_point with
| Initial -> None, Kglobal
| Pre kf -> Some kf, Kglobal
| Stmt (kf, stmt) -> Some kf, Kstmt stmt
in
fun vi ->
let marker = Printer_tag.PLval (kf, kinstr, Cil.var vi) in
Server.Kernel_ast.Marker.index marker
let with_updated_varinfo_printer eval_point f =
let tag_vi = tag_varinfo_as_lval_at eval_point in
let module Printer_class(X: Printer.PrinterClass) = struct
class printer () = object
inherit X.printer () as super
method! varinfo fmt vi =
Format.fprintf fmt "@{<%s>%a@}" (tag_vi vi) super#varinfo vi;
end
end in
let printer = Printer.current_printer () in
let finally () = Printer.set_printer printer in
Printer.update_printer (module Printer_class: Printer.PrinterExtension);
Fun.protect ~finally f
let print_value fmt loc =
let is_scalar = Ast_types.is_scalar in
let evaluation_point = marker_evaluation_point loc in
let request = request_at evaluation_point in
let eval =
match loc with
| Printer_tag.PLval (_, _, lval) when is_scalar (Cil.typeOfLval lval) ->
Results.eval_lval lval
| Printer_tag.PExp (_, _, expr) when is_scalar (Cil.typeOf expr) ->
Results.eval_exp expr
| PVDecl (_, _, vi) when is_scalar vi.vtype ->
Results.eval_var vi
| PTermLval (kf, _, _ip, tlval) ->
let lval = term_lval_to_lval kf tlval in
if is_scalar (Cil.typeOfLval lval)
then Results.eval_lval lval
else raise Not_found
| _ -> raise Not_found
in
let pretty = Cvalue.V_Or_Uninitialized.pretty in
let eval_cvalue at = Results.(eval at |> as_cvalue_or_uninitialized) in
let before = eval_cvalue request in
let print =
match evaluation_point with
| Initial | Pre _ -> fun () -> pretty fmt before
| Stmt (_, stmt) ->
let after = eval_cvalue (Results.after stmt) in
if Cvalue.V_Or_Uninitialized.equal before after
then fun () -> pretty fmt before
else fun () ->
Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
in
with_updated_varinfo_printer evaluation_point print
let () =
Server.Kernel_ast.Information.register
~id:"eva.value"
~label:"Value"
~title:"Possible values inferred by Eva"
~enable:Analysis.is_computed
print_value
type term = Pexpr of exp | Plval of lval | Ppred of predicate
type probe = term * evaluation_point
type truth = Abstract_interp.truth
type evaluation = {
value: Jtext.t;
alarms: ( truth * string ) list ;
pointed_vars: (string * Printer_tag.localizable) list;
}
type 'v next =
| After of 'v
| Cond of 'v * 'v
| Nothing
type evaluations = {
here: evaluation;
next: evaluation next;
}
let next_steps = function
| Initial | Pre _ -> `None
| Stmt (_, stmt) ->
match stmt.skind with
| If (cond, _, _, _) -> `Condition (stmt, cond)
| Instr (Set _ | Call _ | Local_init _) -> `Effect stmt
| Instr _ when Annotations.has_code_annot stmt -> `Effect stmt
| Instr (Asm _ | Code_annot _ | Skip _)
| Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| TryCatch _ | TryFinally _ | TryExcept _
| Return _ | Break _ | Continue _ | Goto _ | Throw _ -> `None
let probe_stmt stmt =
match stmt.skind with
| Instr (Set (lv, _, _))
| Instr (Call (Some lv, _, _, _)) -> Plval lv
| Instr (Local_init (v, _, _)) -> Plval (Var v, NoOffset)
| Return (Some e, _) | If (e, _, _, _) | Switch (e, _, _, _) -> Pexpr e
| _ -> raise Not_found
let probe_code_annot = function
| AAssert (_, p) | AInvariant (_, true, p) -> Ppred p.tp_statement
| _ -> raise Not_found
let probe_property = function
| Property.IPCodeAnnot ica -> probe_code_annot ica.ica_ca.annot_content
| IPPropertyInstance { ii_pred = Some pred }
| IPPredicate {ip_pred = pred} ->
Ppred (Logic_const.pred_of_id_pred pred)
| _ -> raise Not_found
let probe_marker = function
| Printer_tag.PLval (_, _, lval)
when Ast_types.is_fun (Cil.typeOfLval lval) -> raise Not_found
| PVDecl (_, _, vi) when Ast_types.is_fun vi.vtype -> raise Not_found
| PLval (_, _, l) -> Plval l
| PExp (_, _, e) -> Pexpr e
| PStmt (_, s) | PStmtStart (_, s) -> probe_stmt s
| PVDecl (_, _, v) -> Plval (Var v, NoOffset)
| PTermLval (kf, _, _, tlval) ->
Plval (term_lval_to_lval kf tlval)
| PIP property -> probe_property property
| _ -> raise Not_found
let probe marker =
try Some (probe_marker marker, marker_evaluation_point marker)
with Not_found -> None
module Jtruth : Data.S with type t = truth = struct
type t = truth
let jtype = Package.(Junion [ Jtag "True" ; Jtag "False" ; Jtag "Unknown" ])
let to_json = function
| Abstract_interp.Unknown -> `String "Unknown"
| True -> `String "True"
| False -> `String "False"
let of_json = function
| `String "True" -> Abstract_interp.True
| `String "False" -> Abstract_interp.False
| _ -> Abstract_interp.Unknown
end
type offsetmap =
| Offsetmap of Cvalue.V_Offsetmap.t
| Bottom | Empty | Top | InvalidLoc
let pp_offsetmap typ fmt = function
| Bottom -> Format.fprintf fmt "<BOTTOM>"
| Empty -> Format.fprintf fmt "<EMPTY>"
| Top -> Format.fprintf fmt "<NO INFORMATION>"
| InvalidLoc -> Format.fprintf fmt "<INVALID LOCATION>"
| Offsetmap offsm ->
Cvalue.V_Offsetmap.pretty_generic ~typ () fmt offsm ;
Eval_op.pretty_stitched_offsetmap fmt typ offsm
let vi state =
let b = Base.of_varinfo vi in
try
match Cvalue.Model.find_base b state with
| `Bottom -> Bottom
| `Value m -> Offsetmap m
| `Top -> Top
with Not_found -> InvalidLoc
let reduce_loc_and_eval state loc =
if Cvalue.Model.is_top state then Top
else if not (Cvalue.Model.is_reachable state) then Bottom
else if Z_or_top.is_zero loc.Locations.size then Empty
else
let loc' = Locations.(valid_part Read loc) in
if Locations.is_bottom loc' then InvalidLoc
else
try
let size = Z_or_top.project loc'.Locations.size in
match Cvalue.Model.copy_offsetmap loc'.Locations.addr size state with
| `Bottom -> InvalidLoc
| `Value offsm -> Offsetmap offsm
with Abstract_interp.Error_Top -> Top
let find_offsetmap cvalue_state precise_loc =
let f loc acc =
match acc, reduce_loc_and_eval cvalue_state loc with
| Offsetmap o1, Offsetmap o2 -> Offsetmap (Cvalue.V_Offsetmap.join o1 o2)
| Bottom, v | v, Bottom -> v
| Empty, v | v, Empty -> v
| Top, Top -> Top
| InvalidLoc, InvalidLoc -> InvalidLoc
| InvalidLoc, (Offsetmap _ as res) -> res
| Offsetmap _, InvalidLoc -> acc
| Top, r | r, Top -> r
in
Precise_locs.fold f precise_loc Bottom
let get_bases cvalue =
try Base.SetLattice.project (Cvalue.V.get_bases cvalue)
with Abstract_interp.Error_Top -> Base.Hptset.empty
let get_pointed_bases = function
| Offsetmap offsm ->
let get_bases v = Cvalue.V_Or_Uninitialized.get_v v |> get_bases in
let f v acc = get_bases v |> Base.Hptset.union acc in
Cvalue.V_Offsetmap.fold_on_values f offsm Base.Hptset.empty
| Bottom | Empty | Top | InvalidLoc -> Base.Hptset.empty
let filter_variables bases =
let add_var base acc =
try Base.to_varinfo base :: acc
with Base.Not_a_C_variable -> acc
in
let vars = List.rev (Base.Hptset.fold add_var bases []) in
List.filter (fun vi -> not (Ast_types.is_fun vi.vtype)) vars
module type EvaProxy = sig
val evaluate : probe -> Callstack.t option -> evaluations
end
module Proxy(A : Engine_sig.S_with_results) : EvaProxy = struct
open Eval
type dstate = A.Dom.state or_top_bottom
let get_precise_loc =
let default = fun _ -> Precise_locs.loc_top in
Option.value ~default (A.Loc.get Main_locations.PLoc.key)
let get_cvalue =
let default = fun _ -> Cvalue.V.top in
Option.value ~default (A.Val.get Main_values.CVal.key)
let domain_state callstack = function
| Initial -> A.get_state Initial
| Pre kf -> A.get_state ?callstack (Start kf)
| Stmt (_, stmt) -> A.get_state ?callstack (Before stmt)
type result =
| Value of A.Val.t Eval.flagged_value
| Offsetmap of offsetmap
| Status of truth
let pp_result typ fmt = function
| Value v ->
(Eval.pretty_value_with_flags (A.Val.pretty_typ (Some typ))) fmt v
| Offsetmap offsm -> pp_offsetmap typ fmt offsm
| Status truth -> Alarmset.Status.pretty fmt truth
let get_pointed_bases = function
| Value v -> get_bases Bottom.(map get_cvalue v.v |> value ~bottom:Cvalue.V.bottom)
| Offsetmap offsm -> get_pointed_bases offsm
| Status _ -> Base.Hptset.empty
let get_pointed_markers eval_point result =
let bases = get_pointed_bases result in
let vars = filter_variables bases in
let kf, kinstr =
match eval_point with
| Initial -> None, Kglobal
| Pre kf -> Some kf, Kglobal
| Stmt (kf, stmt) -> Some kf, Kstmt stmt
in
let to_marker vi =
let text = Pretty_utils.to_string Printer.pp_varinfo vi in
let marker = Printer_tag.PLval (kf, kinstr, Cil.var vi) in
text, marker
in
List.map to_marker vars
let make_value typ eval_point (result, alarms) =
let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty in
let f alarm status acc = (status, descr alarm) :: acc in
let alarms = Alarmset.fold f [] alarms |> List.rev in
let pretty_eval = Bottom.pretty (pp_result typ) in
let result_to_json () = Data.jpretty pretty_eval result in
let value = with_updated_varinfo_printer eval_point result_to_json in
let pointed_markers = get_pointed_markers eval_point in
let pointed_vars = Bottom.(map pointed_markers result |> value ~bottom:[]) in
{ value; alarms; pointed_vars }
let lval_to_offsetmap (lval : Eva_ast.lval) state =
let cvalue_state = A.Dom.get_cvalue_or_top state in
match lval.node with
| Var vi, NoOffset ->
let r = extract_single_var vi cvalue_state in
`Value r, Alarmset.none
| _ ->
A.eval_lval_to_loc state lval >>=: fun loc ->
let precise_loc = get_precise_loc loc in
find_offsetmap cvalue_state precise_loc
let eval_lval (lval : Eva_ast.lval) state =
match Ast_types.unroll_node lval.typ with
| TInt _ | TEnum _ | TPtr _ | TFloat _ ->
A.copy_lvalue state lval >>=: fun value -> Value value
| _ ->
lval_to_offsetmap lval state >>=: fun offsm -> Offsetmap offsm
let eval_expr expr state =
A.eval_expr state expr >>=: fun value ->
Value { v = `Value value; initialized = true; escaping = false }
let eval_pred eval_point predicate state =
let result =
match eval_point with
| Initial | Pre _ -> None
| Stmt (kf, _) -> Eva_utils.find_return_var kf
in
let env =
Abstract_domain.{ states = (function _ -> A.Dom.top) ; result }
in
let truth = A.Dom.evaluate_predicate env state predicate in
`Value (Status truth), Alarmset.none
let do_next eval state eval_point callstack =
match next_steps eval_point with
| `Condition (stmt, cond) ->
let cond' = Eva_ast.translate_exp cond in
let kf = Kernel_function.find_englobing_kf stmt in
let dummy_callstack = Callstack.init ~thread:0 ~entry_point:kf in
let pos = Position.local stmt dummy_callstack in
let then_state = (A.assume_cond ~pos state cond' true :> dstate) in
let else_state = (A.assume_cond ~pos state cond' false :> dstate) in
Cond (eval then_state, eval else_state)
| `Effect stmt ->
let after_state = A.get_state ?callstack (After stmt) in
After (eval after_state)
| `None -> Nothing
let eval_steps typ eval eval_point callstack =
let default str =
let value = Data.jtext str in
{ value; alarms = []; pointed_vars = []; }
in
let eval = function
| `Bottom -> default "Unreachable"
| `Top -> default "No information"
| `Value state -> make_value typ eval_point (eval state)
in
let before = domain_state callstack eval_point in
let here = eval before in
let next =
match before with
| `Value state -> do_next eval state eval_point callstack
| _ -> Nothing
in
{ here; next; }
let evaluate (term, eval_point) callstack =
match term with
| Plval lval ->
let lval' = Eva_ast.translate_lval lval in
eval_steps lval'.typ (eval_lval lval') eval_point callstack
| Pexpr expr ->
let expr' = Eva_ast.translate_exp expr in
eval_steps expr'.typ (eval_expr expr') eval_point callstack
| Ppred pred ->
eval_steps Cil_const.intType (eval_pred eval_point pred) eval_point callstack
end
let proxy =
let make (a : (module Engine_sig.S_with_results)) =
(module Proxy (val a) : EvaProxy)
in
let current = ref (make @@ Engine.current ()) in
let hook a = current := make a in
Engine.register_hook hook ;
fun () -> !current
let is_reachable = function
| Stmt (_, stmt) -> Results.is_reachable stmt
| Pre kf -> Results.is_called kf
| Initial -> Results.is_reachable_kinstr Kglobal
let () =
let getProbeInfo = Request.signature ~input:(module Jmarker) () in
let set_evaluable = Request.result getProbeInfo
~name:"evaluable" ~descr:(Md.plain "Can the probe be evaluated?")
(module Jbool)
and set_code = Request.result_opt getProbeInfo
~name:"code" ~descr:(Md.plain "Probe source code")
(module Jstring)
and set_stmt = Request.result_opt getProbeInfo
~name:"stmt" ~descr:(Md.plain "Probe statement")
(module Jstmt)
and set_effects = Request.result getProbeInfo
~name:"effects" ~descr:(Md.plain "Effectfull statement")
~default:false (module Jbool)
and set_condition = Request.result getProbeInfo
~name:"condition" ~descr:(Md.plain "Conditional statement")
~default:false (module Jbool)
in
let set_probe rq pp p eval_point =
let computed = Analysis.is_computed () in
let reachable = is_reachable eval_point in
set_evaluable rq (computed && reachable);
set_code rq (Some (Pretty_utils.to_string pp p));
begin
match eval_point with
| Initial | Pre _ -> ()
| Stmt (_kf, stmt) -> set_stmt rq (Some stmt)
end ;
match next_steps eval_point with
| `None -> ()
| `Condition _ -> set_condition rq true
| `Effect _ -> set_effects rq true
in
Request.register_sig ~package getProbeInfo
~kind:`GET ~name:"getProbeInfo"
~descr:(Md.plain "Probe information")
begin fun rq marker ->
match probe marker with
| None -> set_evaluable rq false
| Some (term, eval_point) ->
match term with
| Plval l -> set_probe rq Printer.pp_lval l eval_point
| Pexpr e -> set_probe rq Printer.pp_exp e eval_point
| Ppred p -> set_probe rq Printer.pp_predicate p eval_point
end
module JEvaluation = struct
open Server.Data
type record
let record: record Record.signature = Record.signature ()
let value = Record.field record ~name:"value"
~descr:(Markdown.plain "Textual representation of the value")
(module Data.Jtext)
let alarms = Record.field record ~name:"alarms"
~descr:(Markdown.plain "Alarms raised by the evaluation")
(module Jlist (Jpair (Jtruth) (Jstring)))
let pointed_vars = Record.field record ~name:"pointedVars"
~descr:(Markdown.plain "List of variables pointed by the value")
(module Jlist (Jpair (Jstring) (Jmarker)))
let data = Record.publish record ~package ~name:"evaluation"
~descr:(Markdown.plain "Evaluation of an expression or lvalue")
module R: Record.S with type r = record = (val data)
type t = evaluation
let jtype = R.jtype
let to_json t =
R.default |>
R.set value t.value |>
R.set alarms t.alarms |>
R.set pointed_vars t.pointed_vars |>
R.to_json
end
let () =
let getValues = Request.signature () in
let get_tgt = Request.param getValues ~name:"target"
~descr:(Md.plain "Works with all markers containing an expression")
(module Jmarker)
and get_cs = Request.param_opt getValues ~name:"callstack"
~descr:(Md.plain "Callstack to collect (defaults to none)")
(module Callstack_requests.JCallstack)
and set_before = Request.result_opt getValues ~name:"vBefore"
~descr:(Md.plain "Domain values before execution")
(module JEvaluation)
and set_after = Request.result_opt getValues ~name:"vAfter"
~descr:(Md.plain "Domain values after execution")
(module JEvaluation)
and set_then = Request.result_opt getValues ~name:"vThen"
~descr:(Md.plain "Domain values for true condition")
(module JEvaluation)
and set_else = Request.result_opt getValues ~name:"vElse"
~descr:(Md.plain "Domain values for false condition")
(module JEvaluation)
in
Request.register_sig ~package getValues
~kind:`GET ~name:"getValues"
~descr:(Md.plain "Abstract values for the given marker")
~signals:Update.signals
begin fun rq () ->
let module A : EvaProxy = (val proxy ()) in
let marker = get_tgt rq and callstack = get_cs rq in
match probe marker with
| None -> ()
| Some probe ->
let domain = A.evaluate probe callstack in
set_before rq (Some domain.here);
match domain.next with
| After value -> set_after rq (Some value)
| Cond (v_then, v_else) ->
set_then rq (Some v_then);
set_else rq (Some v_else)
| Nothing -> ()
end