1
(**************************************************************************)
3
(* This file is part of Frama-C. *)
5
(* Copyright (C) 2007-2008 *)
6
(* INRIA (Institut National de Recherche en Informatique et en *)
9
(* you can redistribute it and/or modify it under the terms of the GNU *)
10
(* Lesser General Public License as published by the Free Software *)
11
(* Foundation, version 2.1. *)
13
(* It is distributed in the hope that it will be useful, *)
14
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
15
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
16
(* GNU Lesser General Public License for more details. *)
18
(* See the GNU Lesser General Public License version 2.1 *)
19
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
20
(**************************************************************************)
22
(* $Id: interp.ml,v 1.188 2008/12/09 10:36:46 uid525 Exp $ *)
40
(* Utility functions *)
46
(*****************************************************************************)
47
(* Smart constructors. *)
48
(*****************************************************************************)
50
let mktype tnode = new ptype tnode
52
let mkexpr enode pos = new pexpr ~pos enode
54
let void_expr = mkexpr (JCPEconst JCCvoid) Loc.dummy_position
55
let null_expr = mkexpr (JCPEconst JCCnull) Loc.dummy_position
56
let true_expr = mkexpr (JCPEconst(JCCboolean true)) Loc.dummy_position
57
let zero_expr = mkexpr (JCPEconst(JCCinteger "0")) Loc.dummy_position
58
let one_expr = mkexpr (JCPEconst(JCCinteger "1")) Loc.dummy_position
60
let mktag tag_node pos = new ptag ~pos tag_node
62
let mkidentifier name pos = new identifier ~pos name
64
let rec mkconjunct elist pos =
68
| e::el -> mkexpr (JCPEbinary(e,`Bland,mkconjunct el pos)) pos
70
let mkdecl dnode pos = new decl ~pos dnode
73
(*****************************************************************************)
74
(* Locate Jessie expressions on source program. *)
75
(*****************************************************************************)
77
let reg_pos ?id ?kind ?name pos = Output.reg_pos "C" ?id ?kind ?name pos
79
(* [locate] should be called on every Jessie expression which we would like to
80
* locate in the original source program.
82
let locate ?alarm ?pos e =
83
(* Recursively label conjuncts so that splitting conjuncts in Why still
84
* allows to locate the resulting VC.
86
let rec dopos ~toplevel e =
87
(* Generate (and store) a label associated to this source location *)
88
let pos = match pos with
91
if is_unknown_location e#pos then pos else e#pos
93
let lab = match alarm with
96
| Some Alarms.Division_alarm ->
97
reg_pos ~kind:Output.DivByZero pos
98
| Some Alarms.Memory_alarm ->
99
reg_pos ~kind:Output.PointerDeref pos
100
| Some Alarms.Shift_alarm ->
101
reg_pos ~kind:Output.ArithOverflow pos
102
| Some Alarms.Pointer_compare_alarm
103
| Some Alarms.Using_nan_or_infinite_alarm
104
| Some Alarms.Result_is_nan_or_infinite_alarm ->
106
| Some Alarms.Separation_alarm -> reg_pos pos
107
| Some Alarms.Other_alarm -> reg_pos pos
109
let e = match e#node with
110
| JCPEbinary(e1,`Bland,e2) ->
111
begin match e1#node,e2#node with
112
| JCPElabel _,JCPElabel _ -> e (* already labelled *)
113
| JCPElabel _,_ -> (* [e1] already labelled *)
114
let e2 = dopos ~toplevel:false e2 in
115
mkexpr (JCPEbinary(e1,`Bland,e2)) pos
116
| _,JCPElabel _ -> (* [e2] already labelled *)
117
let e1 = dopos ~toplevel:false e1 in
118
mkexpr (JCPEbinary(e1,`Bland,e2)) pos
119
| _,_ -> (* none already labelled *)
120
let e1 = dopos ~toplevel:false e1 in
121
let e2 = dopos ~toplevel:false e2 in
122
mkexpr (JCPEbinary(e1,`Bland,e2)) pos
126
(* Do not generate a label for every intermediate conjunct *)
128
| JCPEbinary(_e1,`Bland,_e2) when not toplevel -> e
130
(* Label the expression accordingly *)
131
mkexpr (JCPElabel(lab,e)) pos
133
dopos ~toplevel:true e
136
(*****************************************************************************)
137
(* Cil to Jessie translation of operators *)
138
(*****************************************************************************)
155
| Shiftlt -> `Bshift_left
156
| Shiftrt -> assert false (* Should be decided at point used *)
169
let relation = function
178
(*****************************************************************************)
179
(* Cil to Jessie translation of types *)
180
(*****************************************************************************)
182
let type_of_padding = mktype (JCPTidentifier name_of_padding_type)
184
let type_conversion_table = Hashtbl.create 0
186
let type_conversion ty1 ty2 =
187
let ty1 = typeRemoveAttributes ["const";"volatile"] (unrollType ty1) in
188
let ty2 = typeRemoveAttributes ["const";"volatile"] (unrollType ty2) in
189
let sig1 = typeSig ty1 and sig2 = typeSig ty2 in
191
let _,_,ty1_to_ty2,ty2_to_ty1 =
192
Hashtbl.find type_conversion_table (sig1,sig2)
194
ty1_to_ty2,ty2_to_ty1
197
let _,_,ty2_to_ty1,ty1_to_ty2 =
198
Hashtbl.find type_conversion_table (sig2,sig1)
200
ty1_to_ty2,ty2_to_ty1
202
let n1 = type_name ty1 and n2 = type_name ty2 in
203
let ty1_to_ty2 = unique_logic_name (n1 ^ "_to_" ^ n2) in
204
let ty2_to_ty1 = unique_logic_name (n2 ^ "_to_" ^ n1) in
206
type_conversion_table (sig1,sig2) (ty1,ty2,ty1_to_ty2,ty2_to_ty1);
207
ty1_to_ty2,ty2_to_ty1
209
type float_model = [ `Real | `Strict | `Full ]
211
let float_model : float_model ref = ref `Real
213
let ctype ?bitsize ty =
214
let tnode = match unrollType ty with
215
| TVoid _attr -> JCPTnative Tunit
218
if Cmdline.Jessie.IntModel.get_val () = Cmdline.Jessie.IMexact then
221
JCPTidentifier (name_of_integral_type ?bitsize ty)
223
| TFloat(fk,_attr) ->
225
match !float_model with
227
(* RealMode floats interpreted as reals *)
232
| FFloat -> JCPTnative Tfloat
233
| FDouble -> JCPTnative Tdouble
234
| FLongDouble -> failwith "Jessie does not handle long double yet"
237
| TPtr(_elemty,_attr) ->
238
if is_reference_type ty then
239
(* Do not use [_elemty] directly but rather [pointed_type ty] in order
240
* to get to the array element in references, i.e. pointers to arrays.
242
begin match unrollType (pointed_type ty) with
243
| TComp(compinfo,_attr) ->
244
let min_bound = Num.num_of_string "0" in
246
Num.num_of_string (Int64.to_string (reference_size ty - 1L))
248
JCPTpointer(compinfo.cname,[],Some min_bound,Some max_bound)
252
begin match unrollType (pointed_type ty) with
253
| TComp(compinfo,_attr) ->
254
JCPTpointer(compinfo.cname,[],None,None)
256
Format.eprintf "%a@." !Ast_printer.d_type ty;
260
| TArray _ -> assert false (* Removed by translation *)
264
(Cil.error "Function pointer type %a not allowed" !Ast_printer.d_type ty)
266
| TNamed _ -> assert false (* Removed by call to [unrollType] *)
268
| TComp(compinfo,_attr) -> JCPTidentifier compinfo.cname
270
| TEnum(enuminfo,_attr) -> JCPTidentifier enuminfo.ename
272
| TBuiltin_va_list _ ->
273
Errormsg.s (Cil.error "Type builtin_va_list not allowed")
278
| Ctype ty -> ctype ty
279
| Ltype (s,[]) -> mktype (JCPTidentifier s)
280
| Linteger -> mktype (JCPTnative Tinteger)
281
| Lreal -> mktype (JCPTnative Treal)
282
| Ltype(_,_) | Lvar _ | Larrow _ -> assert false (* TODO *)
285
(*****************************************************************************)
286
(* Cil to Jessie translation of constants *)
287
(*****************************************************************************)
289
let native_type_of_fkind x : Jc_env.native_type =
293
| FLongDouble -> failwith "Jessie does not handle long double yet"
295
let strip_float_suffix s =
296
let l = pred(String.length s) in
297
match String.get s l with
298
| 'f' | 'F' | 'l' | 'L' -> String.sub s 0 l
301
let rec const ~in_code pos = function
302
| CInt64(_i,_ik,Some s) -> JCPEconst(JCCinteger s)
303
(* Use the textual representation if available *)
305
| CInt64(i,_ik,None) -> JCPEconst(JCCinteger(Int64.to_string i))
307
| CStr _ | CWStr _ -> assert false (* Should have been rewritten *)
309
| CChr c -> JCPEconst(JCCinteger(string_of_int (Char.code c)))
311
| CReal(_f,fk,Some s) ->
312
(* Use the textual representation if available *)
313
let s = strip_float_suffix s in
314
begin match in_code,!float_model with
315
| false,_ | _,`Real -> JCPEconst(JCCreal s)
316
| true, (`Strict | `Full) ->
317
(* add a cast to float or double depending on the value of fk *)
318
JCPEcast(mkexpr (JCPEconst(JCCreal s)) pos, mktype (JCPTnative (native_type_of_fkind fk)))
320
| CReal(f,_fk,None) ->
321
(* otherwise use the float value *)
322
JCPEconst(JCCreal(string_of_float f))
325
let e = mkexpr (const_of_expr ~in_code pos item.eival) pos in
326
JCPEcast(e,ctype (TEnum(item.eihost,[])))
328
and const_of_expr ~in_code pos e =
329
match stripInfo e with Const c -> const ~in_code pos c | _ -> assert false
331
and boolean_const = function
332
| CInt64(i,_ik,_text) ->
333
if i = Int64.zero then JCCboolean false else JCCboolean true
335
| CStr _ | CWStr _ -> JCCboolean true
338
if Char.code c = 0 then JCCboolean false else JCCboolean true
340
| CReal(f,_fk,_text) ->
341
if f = 0.0 then JCCboolean false else JCCboolean true
343
| CEnum {eival = e} -> boolean_const_of_expr e
345
and boolean_const_of_expr e =
346
match stripInfo e with Const c -> boolean_const c | _ -> assert false
349
(*****************************************************************************)
350
(* Cil to Jessie translation of logic constructs *)
351
(*****************************************************************************)
354
| Label(lab,_,_) -> lab
355
| Case _ | Default _ -> assert false
357
let logic_label lab =
361
label_info_final_name = s;
366
| LogicLabel s -> label_name s
368
let labels = filter_out is_case_label !sref.labels in
369
assert (not (labels = []));
370
label_name (label (List.hd labels))
372
let logic_labels = List.map logic_label
374
let logic_labels_assoc =
375
List.map (fun (_,l) -> logic_label l)
377
let term_lhost pos = function
378
| TVar v -> mkexpr (JCPEvar v.lv_name) pos
379
| TResult -> mkexpr (JCPEvar "\\result") pos
380
| TMem _ -> assert false (* Should have been rewritten *)
382
let isLogicConstant t = match t.term_node with
386
let rec coerce_floats t =
387
match !float_model with
390
if isLogicFloatType t.term_type then
391
mkexpr (JCPEcast(term t, mktype (JCPTnative Treal))) t.term_loc
395
let enode = match t.term_node with
396
| TConst c -> const ~in_code:false t.term_loc c
398
| TDataCons({ctor_type = Ltype ("boolean",[])} as d,_args) ->
399
JCPEconst (JCCboolean (d.ctor_name = "\\true"))
401
| TDataCons _ | TUpdate _ ->
402
(* TODO, but only when we have real concrete
403
* types in the Frama-C annotation grammar
407
| TLval lv -> (term_lval t.term_loc lv)#node
409
| TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ ->
410
assert false (* Should be removed by constant folding *)
412
| TUnOp(op,t) -> JCPEunary(unop op,term t)
414
| TBinOp((Lt | Gt | Le | Ge as op),t1,t2)
415
when app_term_type isPointerType false t1.term_type ->
416
(* Pointer comparison is translated as subtraction *)
417
let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) t.term_loc in
418
JCPEbinary(sube,binop op,zero_expr)
420
(* | TBinOp((Eq | Ne as op),t1,t2) *)
421
(* when app_term_type isPointerType false t1.term_type *)
422
(* && (not (is_null_term t1 || is_null_term t2)) *)
423
(* && (not (is_base_addr t1 || is_base_addr t2)) -> *)
424
(* (\* Pointer (dis-)equality is translated as subtraction *\) *)
425
(* let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) t.term_loc in *)
426
(* JCPEbinary(sube,binop op,zero_expr) *)
428
| TBinOp(Shiftrt,t1,t2) ->
429
begin match possible_value_of_integral_term t2 with
430
| Some i when i >= 0L && i < 63L ->
431
(* Right shift by constant is division by constant *)
432
let pow = constant_term t2.term_loc (power_of_two i) in
433
JCPEbinary(term t1,`Bdiv,term pow)
435
let op = match t1.term_type with
437
if isSignedInteger ty1 then `Barith_shift_right
438
else `Blogical_shift_right
439
| Linteger -> `Barith_shift_right
442
JCPEbinary(term t1,op,term t2)
445
| TBinOp(Shiftlt as op,t1,t2) ->
446
begin match possible_value_of_integral_term t2 with
447
| Some i when i >= 0L && i < 63L ->
448
(* Left shift by constant is multiplication by constant *)
449
let pow = constant_term t2.term_loc (power_of_two i) in
450
JCPEbinary(term t1,`Bmul,term pow)
452
JCPEbinary(term t1,binop op,term t2)
455
| TBinOp((Lt | Gt | Le | Ge) as op,t1,t2) ->
456
JCPEbinary(term t1,binop op,term t2)
458
| TBinOp(op,t1,t2) ->
459
JCPEbinary(coerce_floats t1,binop op,coerce_floats t2)
462
when isIntegralType ty && isLogicArithmeticType t.term_type ->
463
if Cmdline.Jessie.IntModel.get_val () = Cmdline.Jessie.IMexact then
466
JCPEcast(term t,ctype ty)
469
when isFloatingType ty && isLogicArithmeticType t.term_type ->
470
JCPEcast(term t,ctype ty)
473
when isIntegralType ty && app_term_type isPointerType false t.term_type ->
474
(* && bits_sizeof ty = force_app_term_type bits_sizeof t.term_type -> *)
475
(* let _,ptr_to_int = force_app_term_type (type_conversion ty) t.term_type in *)
476
(* JCPEapp(ptr_to_int,[],[term t]) *)
478
(Cil.error "Casting from type %a to type %a not allowed"
479
!Ast_printer.d_logic_type t.term_type !Ast_printer.d_type ty)
481
| TCastE(ptrty,_t1) when isPointerType ptrty ->
482
let t = stripTermCasts t in
483
begin match t.term_node with
487
when is_integral_const c && value_of_integral_const c = Int64.zero ->
490
(* if isLogicIntegralType t.term_type then *)
492
(* mkexpr (JCPEaddress(Addr_absolute,term t)) t.term_loc *)
494
(* JCPEcast(addr,ctype ptrty) *)
495
(* else if force_app_term_type isIntegralType t.term_type *)
497
(* force_app_term_type bits_sizeof t.term_type *)
498
(* = bits_sizeof ptrty *)
500
(* let _,int_to_ptr = *)
501
(* force_app_term_type (type_conversion ptrty) t.term_type *)
503
(* JCPEapp(int_to_ptr,[],[term t]) *)
504
(* else if force_app_term_type isPointerType t.term_type then *)
505
(* let destty = pointed_type ptrty in *)
506
(* let srcty = force_app_term_type pointed_type t.term_type in *)
507
(* if Retype.subtype srcty destty then *)
509
(* else if Retype.TypeUnion.same_class destty srcty then *)
510
(* JCPEcast(term t,ctype ptrty) *)
513
(* JCPEcast(term t,ctype ptrty) *)
514
(* let _,ptr_to_ptr = *)
515
(* force_app_term_type (type_conversion ptrty) t.term_type *)
517
(* JCPEapp(ptr_to_ptr,[],[term t]) *)
519
(* Only hierarchical types are available in Jessie. It
520
* should have been encoded as the use of pointer types
524
(* match unrollType ty with *)
525
(* | TComp(compinfo,_) -> *)
526
(* JCPEcast(term t,compinfo.cname) *)
527
(* | _ -> assert false *)
529
(Cil.error "Casting from type %a to type %a not allowed in logic"
530
!Ast_printer.d_logic_type t.term_type !Ast_printer.d_type ptrty)
534
(* TODO: support other casts in Jessie as well, through low-level
538
(Cil.error "Casting from type %a to type %a not allowed"
539
!Ast_printer.d_logic_type t.term_type !Ast_printer.d_type ty)
541
| TAddrOf _tlv -> assert false (* Should have been rewritten *)
543
| TStartOf tlv -> (term_lval t.term_loc tlv)#node
545
| Tapp(linfo,labels,tlist) ->
546
let name = linfo.l_name in
547
JCPEapp(name,logic_labels_assoc labels,List.map coerce_floats tlist)
549
| Tif(t1,t2,t3) -> JCPEif(term t1,term t2,term t3)
551
| Told t -> JCPEold(term t)
553
| Tat(t,lab) -> JCPEat(term t,logic_label lab)
555
| Tbase_addr t -> JCPEbase_block(term t)
557
| Tblock_length _t -> assert false (* TODO: memory model for Jessie *)
559
| Tnull -> JCPEconst JCCnull
561
| TCoerce(_t,_typ) -> assert false (* TODO: see if useful *)
563
| TCoerceE(_t1,_t2) -> assert false (* TODO: see if useful *)
564
| Tlambda _ -> assert false (* TODO: does not exist in Jessie *)
566
| Ttypeof _ | Ttype _ -> assert false (* Should have been treated *)
567
| Ttsets _ -> assert false
569
mkexpr enode t.term_loc
572
let tag_node = match t.term_node with
573
| Ttypeof t -> JCPTtypeof (term t)
575
let id = mkidentifier (get_struct_name (pointed_type ty)) t.term_loc in
577
| _ -> assert false (* Not a tag *)
579
mktag tag_node t.term_loc
581
and term_lval pos lv =
583
| lhost, TNoOffset -> term_lhost pos lhost
585
| (TVar _ | TResult), _off ->
586
assert false (* Should have been rewritten *)
588
| TMem t, TField(fi,toff) ->
589
assert (toff = TNoOffset); (* Others should have been rewritten *)
591
if not fi.fcomp.cstruct then (* field of union *)
592
mkexpr (JCPEcast(e,ctype fi.ftype)) pos
594
let repfi = Retype.FieldUnion.repr fi in
596
if FieldinfoComparable.equal fi repfi then
600
mkexpr (JCPEcast(e,ctype (TPtr(TComp(repfi.fcomp,[]),[])))) pos
604
mkexpr (JCPEderef(e,fi.fname)) pos
606
| TMem t, TIndex(it,TField(fi,toff)) ->
607
assert (toff = TNoOffset); (* Others should have been rewritten *)
608
(* Normalization made it equivalent to simple add *)
609
let e = mkexpr (JCPEbinary(term t,`Badd,term it)) pos in
610
if not fi.fcomp.cstruct then (* field of union *)
611
mkexpr (JCPEcast(e,ctype fi.ftype)) pos
613
let repfi = Retype.FieldUnion.repr fi in
615
if FieldinfoComparable.equal fi repfi then
619
mkexpr (JCPEcast(e,ctype (TPtr(TComp(repfi.fcomp,[]),[])))) pos
623
mkexpr (JCPEderef(e,fi.fname)) pos
625
| TMem _e, TIndex _ ->
626
Format.eprintf "%a@." !Ast_printer.d_term_lval lv;
627
assert false (* Should have been rewritten *)
629
let tsets_lhost = function
630
| TSVar lv -> mkexpr (JCPEvar lv.lv_name) Loc.dummy_position
631
| TSResult -> mkexpr (JCPEvar "\\result") Loc.dummy_position
632
| TSMem _ as lhost ->
633
Format.eprintf "[Interp.tsets_lhost] unexpected %a@."
634
!Ast_printer.d_tsets_lhost lhost;
635
assert false (* Should have been rewritten *)
637
let rec tsets_elem ts =
638
let enode = match ts with
639
| TSLval lv -> (tsets_lval lv)#node
641
| TSStartOf lv -> (tsets_lval lv)#node
643
| TSAddrOf _ -> assert false (* Should have been rewritten *)
645
| TSConst c -> const ~in_code:false Loc.dummy_position c
647
| TSat(ts,lab) -> JCPEat(tsets_elem ts,logic_label lab)
649
| TSAdd_index(base,idx) ->
650
JCPEbinary(tsets_elem base,`Badd,term idx)
652
| TSAdd_range(base,low,high) ->
654
mkexpr (JCPErange(opt_map term low,opt_map term high)) Loc.dummy_position
656
JCPEbinary(tsets_elem base,`Badd,e)
659
when isIntegralType ty && isLogicArithmeticType (typeOfTsetsElem ts) ->
660
if Cmdline.Jessie.IntModel.get_val () = Cmdline.Jessie.IMexact then
663
JCPEcast(tsets_elem ts,ctype ty)
666
when isFloatingType ty && isLogicArithmeticType (typeOfTsetsElem ts) ->
667
JCPEcast(tsets_elem ts,ctype ty)
669
| TSCastE(ptrty,_ts1) when isPointerType ptrty ->
670
begin match stripTsetsCasts ts with
672
when is_integral_const c && value_of_integral_const c = Int64.zero ->
675
(* let ety = typeOfTsetsElem ts in *)
676
(* if isLogicIntegralType ety then *)
678
(* mkexpr (JCPEaddress(Addr_absolute,tsets_elem ts)) *)
679
(* Loc.dummy_position *)
681
(* JCPEcast(addr,ctype ptrty) *)
682
(* else if force_app_term_type isIntegralType ety then *)
684
(* force_app_term_type bits_sizeof ety *)
685
(* = bits_sizeof ptrty *)
687
(* let _,int_to_ptr = *)
688
(* force_app_term_type (type_conversion ptrty) ety *)
690
(* JCPEapp(int_to_ptr,[],[tsets_elem ts]) *)
691
(* else if force_app_term_type isPointerType ety then *)
692
(* let destty = pointed_type ptrty in *)
693
(* let srcty = force_app_term_type pointed_type ety in *)
694
(* if Retype.subtype srcty destty then *)
695
(* (tsets_elem ts)#node *)
696
(* else if Retype.TypeUnion.same_class destty srcty then *)
697
(* JCPEcast(tsets_elem ts,ctype ptrty) *)
699
(* let _,ptr_to_ptr = *)
700
(* force_app_term_type (type_conversion ptrty) ety *)
702
(* JCPEapp(ptr_to_ptr,[],[tsets_elem ts]) *)
704
(* Only hierarchical types are available in Jessie. It
705
* should have been encoded as the use of pointer types
708
(* match unrollType ty with *)
709
(* | TComp(compinfo,_) -> JCPEcast(tsets_elem ts,compinfo.cname) *)
710
(* | _ -> assert false *)
712
(Cil.error "Casting from type %a to type %a not allowed in logic"
713
!Ast_printer.d_logic_type (typeOfTsetsElem ts) !Ast_printer.d_type ptrty)
717
(* TODO: support other casts in Jessie as well, through low-level
721
(Cil.error "Casting from type %a to type %a not allowed"
722
!Ast_printer.d_logic_type (typeOfTsetsElem ts) !Ast_printer.d_type ty)
723
| TSapp _ -> assert false
725
mkexpr enode Loc.dummy_position
727
and tsets_lval = function
728
| lhost, TSNoOffset -> tsets_lhost lhost
730
| (TSVar _ | TSResult), _off ->
731
assert false (* Should have been rewritten *)
733
| TSMem ts, TSField(fi,tsoff) ->
734
assert (tsoff = TSNoOffset); (* Others should have been rewritten *)
735
let e = tsets_elem ts in
736
if not fi.fcomp.cstruct then (* field of union *)
737
mkexpr (JCPEcast(e,ctype fi.ftype)) Loc.dummy_position
739
let repfi = Retype.FieldUnion.repr fi in
741
if FieldinfoComparable.equal fi repfi then
745
mkexpr (JCPEcast(e,ctype (TPtr(TComp(repfi.fcomp,[]),[]))))
750
mkexpr (JCPEderef(e,fi.fname)) Loc.dummy_position
752
| TSMem ts, TSIndex(it,TSField(fi,tsoff)) ->
753
assert (tsoff = TSNoOffset); (* Others should have been rewritten *)
754
(* Normalization made it equivalent to simple add *)
756
mkexpr (JCPEbinary(tsets_elem ts,`Badd,term it)) Loc.dummy_position
758
if not fi.fcomp.cstruct then (* field of union *)
759
mkexpr (JCPEcast(e,ctype fi.ftype)) Loc.dummy_position
761
let repfi = Retype.FieldUnion.repr fi in
763
if FieldinfoComparable.equal fi repfi then
767
mkexpr (JCPEcast(e,ctype (TPtr(TComp(repfi.fcomp,[]),[]))))
772
mkexpr (JCPEderef(e,fi.fname)) Loc.dummy_position
774
| TSMem _ts, TSIndex _ -> assert false (* Should have been rewritten *)
776
| TSMem ts, TSRange(low,high,TSField(fi,tsoff)) ->
777
assert (tsoff = TSNoOffset); (* Others should have been rewritten *)
778
(* Normalization made it equivalent to simple add *)
779
let enode = JCPErange(opt_map term low,opt_map term high) in
780
let e = mkexpr enode Loc.dummy_position in
782
mkexpr (JCPEbinary(tsets_elem ts,`Badd,e)) Loc.dummy_position
784
if not fi.fcomp.cstruct then (* field of union *)
785
mkexpr (JCPEcast(e,ctype fi.ftype)) Loc.dummy_position
787
let repfi = Retype.FieldUnion.repr fi in
789
if FieldinfoComparable.equal fi repfi then
793
mkexpr (JCPEcast(e,ctype (TPtr(TComp(repfi.fcomp,[]),[]))))
798
mkexpr (JCPEderef(e,fi.fname)) Loc.dummy_position
800
| TSMem _ts, TSRange _ -> assert false (* Should have been rewritten *)
802
let rec tsets = function
803
| TSSingleton ts -> [tsets_elem ts]
805
| TSUnion locs -> List.flatten (List.map tsets locs)
806
| TSInter _locs -> assert false (* TODO *)
807
| TSComprehension(_t,_q,_p) -> assert false (* TODO *)
811
let enode = match p.content with
812
| Pfalse -> JCPEconst(JCCboolean false)
814
| Ptrue -> JCPEconst(JCCboolean true)
816
| Papp(pinfo,labels,tl) ->
817
JCPEapp(pinfo.l_name,logic_labels_assoc labels,List.map term tl)
819
| Prel((Rlt | Rgt | Rle | Rge as rel),t1,t2)
820
when app_term_type isPointerType false t1.term_type ->
821
(* Pointer comparison is translated as subtraction *)
822
let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) p.loc in
823
JCPEbinary(sube,relation rel,zero_expr)
825
(* | Prel((Req | Rneq as rel),t1,t2) *)
826
(* when app_term_type isPointerType false t1.term_type *)
827
(* && (not (is_null_term t1 || is_null_term t2)) *)
828
(* && (not (is_base_addr t1 || is_base_addr t2)) -> *)
829
(* (\* Pointer (dis-)equality is translated as subtraction *\) *)
830
(* let sube = mkexpr (JCPEbinary(term t1,`Bsub,term t2)) p.loc in *)
831
(* JCPEbinary(sube,relation rel,zero_expr) *)
833
| Prel(Req,t1,t2) when isTypeTagType t1.term_type ->
834
JCPEeqtype(tag t1,tag t2)
836
| Prel(Rneq,t1,t2) when isTypeTagType t1.term_type ->
837
let eq = mkexpr (JCPEeqtype(tag t1,tag t2)) p.loc in
841
JCPEbinary(coerce_floats t1,relation rel,coerce_floats t2)
844
JCPEbinary(pred p1,`Bland,pred p2)
847
JCPEbinary(pred p1,`Blor,pred p2)
850
let notp2 = { p2 with content = Pnot p2; } in
851
let p1notp2 = { p with content = Pand(p1,notp2); } in
852
let notp1 = { p1 with content = Pnot p1; } in
853
let p2notp1 = { p with content = Pand(p2,notp1); } in
854
JCPEbinary(pred p1notp2,`Blor,pred p2notp1)
857
JCPEbinary(pred p1,`Bimplies,pred p2)
860
JCPEbinary(pred p1,`Biff,pred p2)
862
| Pnot p -> JCPEunary(`Unot,pred p)
864
| Pif(t,p1,p2) -> JCPEif(term t,pred p1,pred p2)
866
| Plet(_v,_t,_p) -> assert false (* TODO *)
868
| Pforall([],p) -> (pred p)#node
871
JCPEquantifier(Forall,ltype v.lv_type,[v.lv_name],pred p)
873
| Pforall(v::q,subp) ->
874
let newp = { p with content = Pforall(q,subp) } in
875
JCPEquantifier(Forall,ltype v.lv_type,[v.lv_name],pred newp)
877
| Pexists([],p) -> (pred p)#node
880
JCPEquantifier(Exists,ltype v.lv_type,[v.lv_name],pred p)
882
| Pexists(v::q,subp) ->
883
let newp = { p with content = Pexists(q,subp) } in
884
JCPEquantifier(Exists,ltype v.lv_type,[v.lv_name],pred newp)
886
| Pold p -> JCPEold(pred p)
888
| Pat(p,lab) -> JCPEat(pred p,logic_label lab)
890
| Pvalid_index(t1,t2) ->
893
let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.loc in
894
let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.loc in
895
let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.loc in
896
let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e2)) p.loc in
897
(mkconjunct [emin; emax] p.loc)#node
899
| Pvalid(TSSingleton(TSAdd_index(t1,t2))) ->
900
let e1 = tsets_elem t1 in
902
let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.loc in
903
let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.loc in
904
let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.loc in
905
let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e2)) p.loc in
906
(mkconjunct [emin; emax] p.loc)#node
908
| Pvalid_range(t1,t2,t3) ->
912
let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.loc in
913
let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.loc in
914
let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.loc in
915
let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e3)) p.loc in
916
(mkconjunct [emin; emax] p.loc)#node
918
| Pvalid(TSSingleton(TSAdd_range(t1,t2,t3))) ->
919
let e1 = tsets_elem t1 in
920
begin match t2,t3 with
921
| None,None -> true_expr#node
924
let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.loc in
925
JCPEbinary(eoffmin,`Ble,e2)
928
let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.loc in
929
JCPEbinary(eoffmax,`Bge,e3)
933
let eoffmin = mkexpr (JCPEoffset(Offset_min,e1)) p.loc in
934
let emin = mkexpr (JCPEbinary(eoffmin,`Ble,e2)) p.loc in
935
let eoffmax = mkexpr (JCPEoffset(Offset_max,e1)) p.loc in
936
let emax = mkexpr (JCPEbinary(eoffmax,`Bge,e3)) p.loc in
937
(mkconjunct [emin; emax] p.loc)#node
942
List.flatten (List.map (fun e ->
943
let eoffmin = mkexpr (JCPEoffset(Offset_min,e)) p.loc in
944
let emin = mkexpr (JCPEbinary(eoffmin,`Ble,zero_expr)) p.loc in
945
let eoffmax = mkexpr (JCPEoffset(Offset_max,e)) p.loc in
946
let emax = mkexpr (JCPEbinary(eoffmax,`Bge,zero_expr)) p.loc in
950
(mkconjunct elist p.loc)#node
952
| Pfresh _t -> assert false (* TODO: add to memory model for Jessie *)
954
| Psubtype({term_node = Ttypeof t},{term_node = Ttype ty}) ->
955
JCPEinstanceof(term t,get_struct_name (pointed_type ty))
957
| Psubtype(_t1,_t2) -> assert false (* TODO *)
958
| Pseparated(_seps) -> assert false (* TODO *)
962
(* Keep names associated to predicate *)
965
(fun lab p -> mkexpr (JCPElabel(lab,p)) p#pos) p.name (pred p)
967
let pred_has_name p n =
968
List.exists (fun n2 -> n = n2) p.name
970
let remove_pred_name p n =
971
{ p with name = List.filter (fun n2 -> not (n = n2)) p.name }
973
let conjunct pos pl =
974
mkconjunct (List.map (pred $ Logic_const.pred_of_id_pred) pl) pos
977
| Location tset,_from -> tsets tset.its_content
978
| Nothing,_from -> []
980
(* Distinguish between:
981
* - no assign, which is the empty list in Cil and None in Jessie
982
* - assigns nothing, which is [Nothing] in Cil and the Some[] in Jessie
984
let assigns = function
991
not (Logic_const.tsets_is_result out.its_content)
992
| Nothing, _ -> false)
995
let assign_list = List.flatten (List.map zone assign_list) in
996
Some(Loc.dummy_position,assign_list)
1000
JCCrequires(locate (pred (Logic_const.pred_of_id_pred p)))
1002
let requires = List.map require funspec.spec_requires in
1008
Some(conjunct Loc.dummy_position b.b_assumes),
1009
None, (* requires *)
1010
assigns b.b_assigns,
1011
locate (conjunct Loc.dummy_position b.b_ensures))
1013
let behaviors = List.map behavior funspec.spec_behavior in
1015
if funspec.spec_complete_behaviors <> [] then
1016
Errormsg.warn "[Jessie plugin] complete behaviors specification ignored";
1017
if funspec.spec_disjoint_behaviors <> [] then
1018
Errormsg.warn "[Jessie plugin] disjoint behaviors specification ignored";
1019
if funspec.spec_variant <> None then
1020
Errormsg.warn "[Jessie plugin] variant for recursive function ignored";
1021
if funspec.spec_terminates <> None then
1022
Errormsg.warn "[Jessie plugin] termination condition ignored";
1024
(* TODO: translate function spec variant, terminates and complete/disjoint
1026
requires @ behaviors
1028
(* Depending on the argument status, an assertion with this status may
1029
not generate any PO but still be used as an hypothesis. *)
1030
let assertion = function
1031
| { status = Checked { valid = True } } -> Aassume
1034
let assert_ pos = function
1037
begin match annot.annot_content with
1038
| AAssert (behav,p,status) ->
1039
let asrt = assertion status in
1040
[mkexpr (JCPEassert (behav,asrt,locate ~pos (named_pred p))) pos]
1041
| AInvariant(behav,_,p) ->
1043
(behav,Aassert,locate ~pos (named_pred p))) pos]
1046
| AI(alarm,annot) ->
1047
begin match annot.annot_content with
1048
| AAssert (behav,p,status) ->
1050
if pred_has_name p name_of_hint_assertion then Ahint
1051
else assertion status
1053
let p = remove_pred_name p name_of_hint_assertion in
1055
if behav = [] then [ name_of_default_behavior ] else behav
1057
[mkexpr (JCPEassert (behav,asrt,locate ~alarm ~pos (named_pred p))) pos]
1058
| AInvariant(behav,_,p) ->
1060
if behav = [] then [ name_of_default_behavior ] else behav
1063
(behav,Aassert,locate ~alarm ~pos (named_pred p))) pos]
1067
let invariant annot =
1068
match annot.annot_content with
1069
| AInvariant(behav,_loopinv,p) -> behav, locate (pred p)
1073
match annot.annot_content with
1074
| AVariant(t,_) -> locate (term t)
1078
(*****************************************************************************)
1079
(* Cil to Jessie translation of coding constructs *)
1080
(*****************************************************************************)
1082
let set_curFundec, get_curFundec =
1083
let cf = ref None in
1084
((fun f -> cf := Some f),
1088
let res = emptyFunction "@empty@" in cf := Some res; res
1091
let rec expr pos e =
1092
(* Precise the location if possible *)
1093
let pos = match e with Info(_,einfo) -> einfo.exp_loc | _ -> pos in
1095
let expr = expr pos in
1096
let integral_expr = integral_expr pos in
1098
let enode = match stripInfo e with
1099
| Info _ -> assert false
1101
| Const c -> const ~in_code:true pos c
1103
| Lval lv -> (lval pos lv)#node
1105
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
1106
assert false (* Should be removed by constant folding *)
1108
| UnOp(_op,_e,ty) when isIntegralType ty ->
1109
(integral_expr e)#node
1113
locate (mkexpr (JCPEunary(unop op,expr e)) pos)
1117
| BinOp(_op,_e1,_e2,ty) when isIntegralType ty ->
1118
(integral_expr e)#node
1120
| BinOp(op,e1,e2,_ty) ->
1122
locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) pos)
1126
| CastE(ty,e') when isIntegralType ty && isArithmeticType (typeOf e') ->
1127
(integral_expr e)#node
1129
| CastE(ty,e) when isFloatingType ty && isArithmeticType (typeOf e) ->
1130
let e = locate (mkexpr (JCPEcast(expr e,ctype ty)) pos) in
1133
| CastE(ty,e') when isIntegralType ty && isPointerType (typeOf e') ->
1134
(* && bits_sizeof ty = bits_sizeof (typeOf e') -> *)
1135
(* let _,ptr_to_int = type_conversion ty (typeOf e') in *)
1136
(* JCPEapp(ptr_to_int,[],[expr e']) *)
1138
(Cil.error "Casting from type %a to type %a not allowed"
1139
!Ast_printer.d_type (typeOf e') !Ast_printer.d_type ty)
1141
| CastE(ptrty,_e1) when isPointerType ptrty ->
1142
begin match stripCastsAndInfo e with
1144
when is_integral_const c
1145
&& value_of_integral_const c = Int64.zero ->
1148
let ety = typeOf e in
1149
if isIntegralType ety(* && bits_sizeof ety = bits_sizeof ptrty *) then
1150
(* let _,int_to_ptr = type_conversion ptrty ety in *)
1151
(* JCPEapp(int_to_ptr,[],[integral_expr e]) *)
1153
(Cil.error "Casting from type %a to type %a not allowed"
1154
!Ast_printer.d_type (typeOf e) !Ast_printer.d_type ptrty)
1155
else if isPointerType ety then
1156
(* let destty = pointed_type ptrty in *)
1157
(* let srcty = pointed_type ety in *)
1158
(* if Retype.subtype srcty destty then *)
1160
(* else if Retype.TypeUnion.same_class destty srcty then *)
1161
(* let enode = JCPEcast(expr e,ctype ptrty) in *)
1162
(* let e = locate (mkexpr enode pos) in *)
1166
let enode = JCPEcast(expr e,ctype ptrty) in
1167
let e = locate (mkexpr enode pos) in
1169
(* let _,ptr_to_ptr = type_conversion ptrty ety in *)
1170
(* JCPEapp(ptr_to_ptr,[],[expr e]) *)
1172
(* Only hierarchical types are available in Jessie. It
1173
* should have been encoded as the use of pointer types
1174
* on structure type.
1176
(* match unrollType ty with *)
1177
(* | TComp(compinfo,_) -> *)
1178
(* JCPEcast(expr (stripCasts e),compinfo.cname) *)
1179
(* | _ -> assert false *)
1181
(Cil.error "Casting from type %a to type %a not allowed"
1182
!Ast_printer.d_type (typeOf e) !Ast_printer.d_type ptrty)
1185
| CastE(ty,e) as caste ->
1186
(* TODO: support other casts in Jessie as well, through low-level
1190
(Cil.error "Casting from type %a to type %a not allowed in %a with size %Ld and %Ld"
1191
!Ast_printer.d_type (typeOf e) !Ast_printer.d_type ty
1192
!Ast_printer.d_exp caste
1193
( bits_sizeof ty) ( bits_sizeof (typeOf e))
1197
Format.printf "%a@." !Ast_printer.d_lval _lv;
1198
assert false (* Should have been rewritten *)
1200
| StartOf lv -> (lval pos lv)#node
1204
(* Function called when expecting a boolean in Jessie, i.e. when translating
1205
a test or a sub-expression of an "or" or "and".
1207
and boolean_expr pos e =
1208
(* Precise the posation if possible *)
1209
let pos = match e with Info(_,einfo) -> einfo.exp_loc | _ -> pos in
1211
let expr = expr pos in
1212
let boolean_expr = boolean_expr pos in
1213
let boolean_node_from_expr ty e =
1214
if isPointerType ty then JCPEbinary(e,`Bneq,null_expr)
1215
else if isArithmeticType ty then JCPEbinary (e,`Bneq,zero_expr)
1219
let enode = match stripInfo e with
1220
| Info _ -> assert false
1222
| Const c -> JCPEconst(boolean_const c)
1224
| UnOp(LNot,e,_typ) -> JCPEunary(unop LNot,boolean_expr e)
1226
| BinOp((LAnd | LOr) as op,e1,e2,_typ) ->
1227
JCPEbinary(boolean_expr e1,binop op,boolean_expr e2)
1229
| BinOp((Eq | Ne) as op,e1,e2,_typ) ->
1230
JCPEbinary(expr e1,binop op,expr e2)
1232
| BinOp((Lt | Gt | Le | Ge) as op,e1,e2,_typ) ->
1233
let ty = typeOf e1 in
1234
if isArithmeticType ty then
1235
JCPEbinary(expr e1,binop op,expr e2)
1237
(* Pointer comparison is translated as subtraction *)
1238
let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) pos in
1239
JCPEbinary(sube,binop op,zero_expr)
1241
| _ -> boolean_node_from_expr (typeOf e) (expr e)
1245
(* Function called instead of plain [expr] when the evaluation result should
1246
* fit in a C integral type.
1248
and integral_expr pos e =
1250
let rec int_expr pos e =
1251
let expr = expr pos in
1252
let int_expr = int_expr pos in
1253
let boolean_expr = boolean_expr pos in
1254
let node_from_boolean_expr e = JCPEif(e,one_expr,zero_expr) in
1256
let enode = match e with
1257
| UnOp(LNot,e,_ty) ->
1258
let e = mkexpr (JCPEunary(unop LNot,boolean_expr e)) pos in
1259
node_from_boolean_expr e
1263
locate (mkexpr (JCPEunary(unop op,expr e)) pos)
1267
| BinOp((LAnd | LOr) as op,e1,e2,_ty) ->
1269
mkexpr (JCPEbinary(boolean_expr e1,binop op,boolean_expr e2)) pos
1271
node_from_boolean_expr e
1273
| BinOp((Lt | Gt | Le | Ge as op),e1,e2,_ty)
1274
when isPointerType (typeOf e1) ->
1275
(* Pointer comparison is translated as subtraction *)
1276
let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) pos in
1277
let e = mkexpr (JCPEbinary(sube,binop op,zero_expr)) pos in
1278
node_from_boolean_expr e
1280
(* | BinOp((Eq | Ne as op),e1,e2,_ty) *)
1281
(* when isPointerType (typeOf e1) && *)
1282
(* not (is_null_expr e2 || is_null_expr e1) -> *)
1283
(* (\* Pointer (dis-)equality is translated as subtraction *\) *)
1284
(* let sube = mkexpr (JCPEbinary(expr e1,`Bsub,expr e2)) pos in *)
1285
(* let e = mkexpr (JCPEbinary(sube,binop op,zero_expr)) pos in *)
1286
(* node_from_boolean_expr e *)
1288
| BinOp((Eq | Ne) as op,e1,e2,_ty) ->
1289
let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) pos in
1290
node_from_boolean_expr e
1292
| BinOp((Lt | Gt | Le | Ge) as op,e1,e2,_ty) ->
1293
let e = mkexpr (JCPEbinary(expr e1,binop op,expr e2)) pos in
1294
node_from_boolean_expr e
1296
| BinOp(Shiftrt,e1,e2,_ty) ->
1297
let e = match possible_value_of_integral_expr e2 with
1298
| Some i when i >= 0L && i < 63L ->
1299
(* Right shift by constant is division by constant *)
1300
let pow = constant_expr (power_of_two i) in
1301
locate (mkexpr (JCPEbinary(expr e1,`Bdiv,expr pow)) pos)
1304
if isSignedInteger (typeOf e1) then `Barith_shift_right
1305
else `Blogical_shift_right
1307
locate (mkexpr (JCPEbinary(expr e1,op,expr e2)) pos)
1311
| BinOp(Shiftlt as op,e1,e2,_ty) ->
1312
let e = match possible_value_of_integral_expr e2 with
1313
| Some i when i >= 0L && i < 63L ->
1314
(* Left shift by constant is multiplication by constant *)
1315
let pow = constant_expr (power_of_two i) in
1316
locate (mkexpr (JCPEbinary(expr e1,`Bmul,expr pow)) pos)
1318
locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) pos)
1322
| BinOp(op,e1,e2,_ty) ->
1324
locate (mkexpr (JCPEbinary(expr e1,binop op,expr e2)) pos)
1328
| CastE(ty,e1) when isFloatingType (typeOf e1) ->
1329
let e1' = locate (mkexpr (JCPEcast(expr e1,ltype Linteger)) pos) in
1330
if Cmdline.Jessie.IntModel.get_val () = Cmdline.Jessie.IMexact then
1333
let e2' = locate (mkexpr (JCPEcast(e1',ctype ty)) pos) in
1336
| CastE(ty,e) when isIntegralType (typeOf e) ->
1337
if Cmdline.Jessie.IntModel.get_val () = Cmdline.Jessie.IMexact then
1340
let e = locate (mkexpr (JCPEcast(int_expr e,ctype ty)) pos) in
1343
| _ -> (expr e)#node
1349
| CastE _ -> int_expr pos e
1350
| _ -> int_expr pos (CastE(typeOf e,e))
1352
and lval pos = function
1353
| Var v, NoOffset -> mkexpr (JCPEvar v.vname) pos
1355
| Var _v, _off -> assert false (* Should have been rewritten *)
1357
| Mem _e, NoOffset -> assert false (* Should have been rewritten *)
1359
| Mem e, Field(fi,off) ->
1360
assert (off = NoOffset); (* Others should have been rewritten *)
1361
let e = expr pos e in
1362
if not fi.fcomp.cstruct then (* field of union *)
1363
locate (mkexpr (JCPEcast(e,ctype fi.ftype)) pos)
1365
let repfi = Retype.FieldUnion.repr fi in
1367
if FieldinfoComparable.equal fi repfi then
1373
(JCPEcast(e,ctype (TPtr(TComp(repfi.fcomp,[]),[])))) pos)
1377
locate (mkexpr (JCPEderef(e,fi.fname)) pos)
1379
| Mem e, Index(ie,Field(fi,off)) ->
1380
assert (off = NoOffset); (* Others should have been rewritten *)
1381
(* Normalization made it equivalent to simple add *)
1382
let e = mkexpr (JCPEbinary(expr pos e,`Badd,expr pos ie)) pos in
1383
if not fi.fcomp.cstruct then (* field of union *)
1384
locate (mkexpr (JCPEcast(e,ctype fi.ftype)) pos)
1386
let repfi = Retype.FieldUnion.repr fi in
1388
if FieldinfoComparable.equal fi repfi then
1394
(JCPEcast(e,ctype (TPtr(TComp(repfi.fcomp,[]),[])))) pos)
1398
locate (mkexpr (JCPEderef(e,fi.fname)) pos)
1400
| Mem _e, Index _ as lv ->
1401
Format.printf "lval %a@." !Ast_printer.d_lval lv;
1402
assert false (* Should have been rewritten *)
1404
let keep_only_declared_nb_of_arguments vi l =
1405
let _,args,is_variadic, _ = splitFunctionTypeVI vi in
1407
(warn "skipping all arguments of implicit prototype %s" vi.vname;
1409
else if is_variadic then bug "unsupported variadic functions"
1412
let rec instruction = function
1414
let enode = JCPEassign(lval pos lv,expr pos e) in
1415
(locate (mkexpr enode pos))#node
1417
| Call(None,Lval(Var v,NoOffset),eargs,pos) ->
1418
if is_assert_function v then
1419
JCPEassert([],Aassert,locate (boolean_expr pos (as_singleton eargs)))
1422
if is_free_function v then
1423
let arg = as_singleton eargs in
1424
let subarg = stripCasts arg in
1425
let arg = if isPointerType (typeOf subarg) then subarg else arg in
1426
JCPEfree(expr pos arg)
1429
keep_only_declared_nb_of_arguments
1431
(List.map (expr pos) eargs))
1433
(locate (mkexpr enode pos))#node
1435
| Call(Some lv,Lval(Var v,NoOffset),eargs,pos) ->
1437
if is_malloc_function v || is_realloc_function v then
1438
let lvtyp = pointed_type (typeOfLval lv) in
1439
let lvsiz = (bits_sizeof lvtyp) lsr 3 in
1441
if is_malloc_function v then as_singleton eargs
1443
match eargs with [ _; arg ] -> arg | _ -> assert false
1445
let ty,arg = match stripInfo arg with
1446
| Info _ -> assert false
1447
| Const c as arg when is_integral_const c ->
1448
let allocsiz = (value_of_integral_expr arg) / lvsiz in
1449
let siznode = JCPEconst(JCCinteger(Int64.to_string allocsiz)) in
1450
lvtyp, mkexpr siznode pos
1451
| BinOp(Mult,(Const c as arg),nelem,_ty)
1452
| BinOp(Mult,nelem,(Const c as arg),_ty) when is_integral_const c ->
1453
let factor = (value_of_integral_expr arg) / lvsiz in
1455
if factor = Int64.one then
1458
let factor = constant_expr factor in
1459
expr pos (BinOp(Mult,nelem,factor,typeOf arg))
1463
if lvsiz = Int64.one then
1466
let esiz = constant_expr lvsiz in
1467
lvtyp, expr pos (BinOp(Div,arg,esiz,typeOf arg))
1469
let name_of_type = match unrollType ty with
1470
| TComp(compinfo,_) -> compinfo.cname
1473
JCPEalloc(arg,name_of_type)
1474
else if is_calloc_function v then
1475
let nelem,elsize = match eargs with
1476
| [nelem;elsize] -> nelem,elsize
1479
let ty,arg = match stripInfo elsize with
1480
| Info _ -> assert false
1481
| Const c as arg when is_integral_const c ->
1482
let lvtyp = pointed_type (typeOfLval lv) in
1483
let lvsiz = (bits_sizeof lvtyp) lsr 3 in
1484
let factor = (value_of_integral_expr arg) / lvsiz in
1486
if factor = Int64.one then
1489
let factor = constant_expr factor in
1490
expr pos (BinOp(Mult,nelem,factor,typeOf arg))
1494
let lvtyp = pointed_type (typeOfLval lv) in
1495
let lvsiz = (bits_sizeof lvtyp) lsr 3 in
1496
let esiz = constant_expr lvsiz in
1497
lvtyp, expr pos (BinOp(Div,
1498
BinOp(Mult,nelem,elsize,typeOf arg),
1501
let name_of_type = match unrollType ty with
1502
| TComp(compinfo,_) -> compinfo.cname
1505
JCPEalloc(arg,name_of_type)
1508
keep_only_declared_nb_of_arguments
1510
(List.map (expr pos) eargs))
1512
let lvty = typeOfLval lv in
1513
let call = locate (mkexpr enode pos) in
1515
if TypeComparable.equal lvty (getReturnType v.vtype)
1516
|| is_malloc_function v
1517
|| is_realloc_function v
1518
|| is_calloc_function v
1520
JCPEassign(lval pos lv,call)
1522
let tmpv = makeTempVar (get_curFundec()) (getReturnType v.vtype) in
1523
let tmplv = Var tmpv, NoOffset in
1524
let cast = CastE(lvty,Lval tmplv) in
1525
let tmpassign = JCPEassign(lval pos lv,expr pos cast) in
1526
JCPElet(None,tmpv.vname,Some call,locate (mkexpr tmpassign pos))
1528
(locate (mkexpr enode pos))#node
1530
| Call _ -> assert false
1532
| Asm _ -> assert false
1534
| Skip _pos -> JCPEconst JCCvoid
1536
| Code_annot _ -> JCPEconst JCCvoid
1537
(* Annotations should be retrieved from Db *)
1539
let rec statement s =
1540
let pos = get_stmtLoc s.skind in
1543
Annotations.get_filter Logic_const.is_assert s
1544
@ Annotations.get_filter Logic_const.is_stmt_invariant s
1546
let assert_before,assert_after =
1547
List.partition (function Before _ -> true | After _ -> false) assert_list
1550
List.flatten (List.map ((assert_ pos) $ before_after_content) assert_before)
1553
List.flatten (List.map ((assert_ pos) $ before_after_content) assert_after)
1556
let snode = match s.skind with
1557
| Instr i -> instruction i
1559
| Return(Some e,pos) ->
1560
JCPEreturn(expr pos e)
1562
| Return(None,_pos) ->
1563
JCPEreturn(mkexpr (JCPEconst JCCvoid) pos)
1565
| Goto(sref,_pos) ->
1566
(* Pick the first non-case label in the list of labels associated to
1567
* the target statement
1569
let labels = filter_out is_case_label !sref.labels in
1570
assert (not (labels = []));
1571
JCPEgoto(label (List.hd labels))
1574
assert false (* Should not occur after [prepareCFG] *)
1577
assert false (* Should not occur after [prepareCFG] *)
1579
| If(e,bl1,bl2,pos) ->
1580
JCPEif(boolean_expr pos e,block bl1,block bl2)
1582
| Switch(e,bl,slist,pos) ->
1583
let case_blocks stat_list case_list =
1584
let rec next_case curr_list final_list stat_list case_list =
1585
match stat_list,case_list with
1586
| curr_stat :: rest_stat, curr_case :: rest_case ->
1587
if curr_case.sid = curr_stat.sid then
1588
(* Beginning of a new case. Add previous case to list
1590
let add_to_list cond e l = if cond e then e::l else l in
1591
let not_empty_list = function [] -> false | _ -> true in
1593
add_to_list not_empty_list (List.rev curr_list) final_list
1595
let curr_list = [curr_stat] in
1596
next_case curr_list final_list rest_stat rest_case
1598
let curr_list = curr_stat :: curr_list in
1599
next_case curr_list final_list rest_stat case_list
1601
if List.length curr_list <> 0 then
1602
List.rev curr_list :: final_list
1606
(* More cases than available. *)
1609
(List.rev_append curr_list stat_list) :: final_list
1611
List.rev (next_case [] [] stat_list case_list)
1613
let switch_label = function
1614
| Label _ -> assert false
1615
| Case(e,pos) -> Some(expr pos e)
1619
| [] -> assert false
1620
| case_stmt :: _ as slist ->
1621
let switch_labels = List.filter is_case_label case_stmt.labels in
1622
let labs = List.map switch_label switch_labels in
1623
let slist = mkexpr (JCPEblock(statement_list slist)) pos in
1626
let case_list = List.map case (case_blocks bl.bstmts slist) in
1627
JCPEswitch(expr pos e,case_list)
1629
| Loop (_,bl,_pos,_continue_stmt,_break_stmt) ->
1630
let invariant_list =
1631
Annotations.get_filter Logic_const.is_invariant s
1633
let invariant_list =
1634
lift_annot_list_func (List.map invariant) invariant_list
1637
let variant_list = Annotations.get_filter Logic_const.is_variant s in
1639
lift_annot_list_func (List.map variant) variant_list
1641
(* At most one variant *)
1642
let variant = match variant_list with
1647
(* Issue a warning on loop assigns not yet supported *)
1648
let assigns_list = Annotations.get_filter Logic_const.is_assigns s in
1649
if assigns_list <> [] then
1650
Errormsg.warn "[Jessie plugin] loop assigns are ignored";
1652
(* Locate the beginning of the loop, to serve as location for generated
1653
* invariants and variants.
1655
(* let lab = reg_pos pos in *)
1656
(* TODO: add loop-assigns to Jessie *)
1657
JCPEwhile(true_expr,invariant_list,variant,block bl)
1660
JCPEblock(statement_list bl.bstmts)
1662
| UnspecifiedSequence seq ->
1663
(*[VP]TODO: take into account undefined behavior tied to the
1664
effects of the statements...
1666
JCPEblock(statement_list (List.map (fun (x,_,_) -> x) seq))
1668
| TryFinally _ | TryExcept _ -> assert false
1670
(* Prefix statement by all non-case labels *)
1671
let labels = filter_out is_case_label s.labels in
1672
let s = mkexpr snode pos in
1673
let s = match assert_before @ s :: assert_after with
1675
| slist -> mkexpr (JCPEblock slist) pos
1677
List.fold_left (fun s lab -> mkexpr (JCPElabel(label lab,s)) pos) s labels
1679
and statement_list slist = List.rev (List.rev_map statement slist)
1682
match bl.bstmts with
1683
| [] -> mkexpr (JCPEconst JCCvoid) Loc.dummy_position
1684
| [s] -> statement s
1685
| slist -> mkexpr (JCPEblock(statement_list slist)) Loc.dummy_position
1688
(*****************************************************************************)
1689
(* Cil to Jessie translation of global declarations *)
1690
(*****************************************************************************)
1692
let logic_variable v =
1693
let name = opt_app (fun v -> v.vname) v.lv_name v.lv_origin in
1694
ltype v.lv_type, name
1696
let rec annotation = function
1697
| Dfun_or_pred info ->
1699
let params = List.map logic_variable info.l_profile in
1701
match info.l_body with
1702
| LBreads reads_tsets ->
1703
let reads = List.flatten (List.map tsets reads_tsets) in
1705
| LBpred p -> JCexpr(pred p)
1706
| LBinductive indcases ->
1708
(fun (id,labs,_poly,p) ->
1709
(new identifier id,logic_labels labs,pred p)) indcases
1712
| LBterm t -> JCexpr(term t)
1714
[JCDlogic(Option_misc.map ltype info.l_type,
1716
logic_labels info.l_labels,
1718
with Errormsg.Error ->
1719
Format.printf "Dropping declaration of predicate %s@." info.l_name;
1724
| Dpredicate_reads(info,_poly,params,reads_tsets) ->
1726
let params = List.map logic_variable params in
1727
let reads = List.flatten (List.map tsets reads_tsets) in
1728
[JCDlogic(None,info.p_name,logic_labels info.p_labels,params,JCreads reads)]
1729
with Errormsg.Error ->
1730
Format.printf "Dropping declaration of predicate %s@." info.p_name;
1734
| Dpredicate_def(info,_poly,params,def) ->
1736
let params = List.map logic_variable params in
1737
[JCDlogic(None,info.p_name,logic_labels info.p_labels,params,JCexpr(pred def))]
1738
with Errormsg.Error ->
1739
Format.printf "Dropping definition of predicate %s@." info.p_name;
1743
| Dinductive_def(info,_poly,params,indcases) ->
1745
let params = List.map logic_variable params in
1748
(new identifier id,pred p)) indcases
1750
[JCDlogic(None,info.p_name,logic_labels info.p_labels,params,JCinductive l)]
1751
with Errormsg.Error ->
1752
Format.printf "Dropping definition of predicate %s@." info.p_name;
1756
| Dlogic_reads(info,_poly,params,return_type,reads_tsets) ->
1758
let params = List.map logic_variable params in
1759
let reads = List.flatten (List.map tsets reads_tsets) in
1761
Some(ltype return_type),
1762
info.l_name,logic_labels info.l_labels,params,JCreads reads)]
1763
with Errormsg.Error ->
1764
Format.printf "Dropping declaration of logic function %s@." info.l_name;
1768
| Dlogic_def(info,_poly,params,return_type,def) ->
1770
let params = List.map logic_variable params in
1772
Some(ltype return_type),info.l_name,logic_labels info.l_labels,params,
1774
with Errormsg.Error ->
1775
Format.printf "Dropping definition of logic function %s@." info.l_name;
1779
| Dlogic_axiomatic(info,_poly,params,return_type,axioms) ->
1781
let params = List.map logic_variable params in
1784
(new identifier id,pred p)) axioms
1787
Some(ltype return_type),info.l_name,logic_labels info.l_labels,
1788
params, JCaxiomatic l)]
1789
with Errormsg.Error ->
1790
Format.printf "Dropping definition of logic function %s@." info.l_name;
1794
| Dlemma(name,is_axiom,labels,_poly,property) ->
1796
[JCDlemma(name,is_axiom,logic_labels labels,pred property)]
1797
with Errormsg.Error ->
1798
Format.printf "Dropping lemma %s@." name;
1802
| Dinvariant property ->
1804
[JCDglobal_inv(property.l_name,
1805
pred (Logic_const.get_pred_body property))]
1806
with Errormsg.Error ->
1807
Format.printf "Dropping invariant %s@." property.l_name;
1811
| Dtype_annot annot ->
1814
None,annot.l_name, logic_labels annot.l_labels,
1815
List.map logic_variable annot.l_profile,
1816
JCexpr(pred (Logic_const.get_pred_body annot)))]
1817
with Errormsg.Error ->
1818
Format.printf "Dropping type invariant %s@." annot.l_name;
1822
| Dtype(name,[]) -> [JCDlogic_type name]
1824
| Dtype(_name,_) -> assert false (* TODO *)
1826
| Daxiomatic(id,l) ->
1828
Format.eprintf "Translating axiomatic %s into jessie code@." id;
1830
let l = List.fold_left (fun acc d -> (annotation d)@acc) [] l in
1831
[JCDaxiomatic(id,List.map (fun d -> mkdecl d Loc.dummy_position )
1834
let global vardefs g =
1835
let dnodes = match g with
1836
| GType _ -> [] (* No typedef in Jessie *)
1838
| GCompTag(compinfo,pos) when compinfo.cstruct -> (* struct type *)
1841
false, ctype ?bitsize:fi.fsize_in_bits fi.ftype,
1842
fi.fname, fi.fsize_in_bits
1845
match fi.fpadding_in_bits with None -> assert false | Some i -> i
1847
if padding_size = 0 then [this] else
1849
false, type_of_padding, unique_name "padding", fi.fpadding_in_bits
1854
List.fold_right (fun fi acc ->
1855
let repfi = Retype.FieldUnion.repr fi in
1856
if FieldinfoComparable.equal fi repfi then
1859
) compinfo.cfields []
1861
let _parent = None in
1862
(* find_or_none (Hashtbl.find Norm.type_to_parent_type) compinfo.cname *)
1864
let ty = TComp(compinfo,[]) in
1866
let parentty = TypeHashtbl.find Retype.type_to_parent_type ty in
1867
let parent = get_struct_name parentty in
1869
JCDtag(compinfo.cname,[],Some (parent,[]),fields,[])
1873
ignore(TypeHashtbl.find Norm.generated_union_types ty);
1874
[JCDtag(compinfo.cname,[],None,fields,[])]
1876
let id = mkidentifier compinfo.cname pos in
1878
JCDtag(compinfo.cname,[],None,fields,[]);
1879
JCDvariant_type(compinfo.cname,[id])
1883
| GCompTag(compinfo,pos) -> (* union type *)
1884
assert (not compinfo.cstruct);
1886
let ty = pointed_type fi.ftype in
1887
mkidentifier (get_struct_name ty) pos
1889
(* match pointed_type fi.ftype with *)
1890
(* | TComp(compinfo,_) -> *)
1891
(* let field fi = false, ctype fi.ftype, fi.fname in *)
1892
(* let fields = List.map field compinfo.cfields in *)
1893
(* (\* let parent = *\) *)
1894
(* (\* find_or_none (Hashtbl.find Norm.type_to_parent_type) *\) *)
1895
(* (\* compinfo.cname *\) *)
1897
(* mkidentifier fi.fname fi.floc, *)
1898
(* JCDtag(fi.fname,[],None,fields,[]) *)
1902
let union_id = mkidentifier compinfo.cname pos in
1903
let union_size = match compinfo.cfields with
1906
Pervasives.(+) (the fi.fsize_in_bits) (the fi.fpadding_in_bits)
1909
if union_size = 0 then [] else
1910
[false, type_of_padding, unique_name "padding", Some union_size]
1912
let union_tag = JCDtag(compinfo.cname,[],None,padding,[]) in
1913
let fields = List.map field compinfo.cfields in
1914
let rec has_pointer ty =
1915
match unrollType ty with
1916
| TComp(compinfo,_attr) ->
1917
List.exists (fun fi -> has_pointer fi.ftype) compinfo.cfields
1919
if is_reference_type ty then
1920
(* Possibly skip intermediate array type *)
1921
has_pointer (pointed_type ty)
1927
| TArray _ -> assert false (* Removed by translation *)
1930
(Cil.error "Function pointer type %a not allowed"
1931
!Ast_printer.d_type ty)
1932
| TNamed _ -> assert false
1933
| TBuiltin_va_list _ -> assert false (* not supported *)
1935
(* Union type with pointer as sub-field should be used as a
1936
discriminated union *)
1937
let discr = has_pointer (TComp(compinfo,[])) in
1938
[JCDunion_type(compinfo.cname,discr,union_id :: fields); union_tag]
1940
| GCompTagDecl _ -> [] (* No struct/union declaration in Jessie *)
1942
| GEnumTag(enuminfo,_pos) ->
1943
assert (not (enuminfo.eitems = []));
1946
(fun {eival = enum} -> value_of_integral_expr enum) enuminfo.eitems
1949
List.fold_left (fun acc enum ->
1950
if acc < enum then acc else enum) (List.hd enums) enums
1952
let min = Num.num_of_string (Int64.to_string emin) in
1954
List.fold_left (fun acc enum ->
1955
if acc > enum then acc else enum) (List.hd enums) enums
1957
let max = Num.num_of_string (Int64.to_string emax) in
1958
[JCDenum_type(enuminfo.ename,min,max)]
1960
| GEnumTagDecl _ -> [] (* No enumeration declaration in Jessie *)
1962
| GVarDecl(_,v,pos) ->
1963
(* Keep only declarations for which there is no definition *)
1964
if List.mem v vardefs
1965
|| (isFunctionType v.vtype &&
1966
(v.vname = name_of_assert
1967
|| v.vname = name_of_free
1968
|| v.vname = name_of_malloc))
1970
else if isFunctionType v.vtype then
1971
let rtyp = match unrollType v.vtype with
1972
| TFun(rt,_,_,_) -> rt
1975
let id = mkidentifier v.vname pos in
1976
let kf = Globals.Functions.get v in
1977
let funspec = Kernel_function.get_spec kf in
1978
let params = Globals.Functions.get_params kf in
1979
let formal v = ctype v.vtype, unique_name_if_empty v.vname in
1980
let formals = List.map formal params in
1981
[JCDfun(ctype rtyp,id,formals,spec funspec,None)]
1983
[JCDvar(ctype v.vtype,v.vname,None)]
1985
| GVar(v,{init=None},_pos) ->
1986
[JCDvar(ctype v.vtype,v.vname,None)]
1988
| GVar(_v,_iinfo,_pos) ->
1989
(* Initialization should have been rewritten as code in an
1990
* initialization function, that is called by the main function in
1991
* global analyses and ignored otherwise.
1997
if f.svar.vname = name_of_assert
1998
|| f.svar.vname = name_of_free then []
2000
let rty = match unrollType f.svar.vtype with
2001
| TFun(ty,_,_,_) -> ty
2004
let formal v = ctype v.vtype, v.vname in
2005
let formals = List.map formal f.sformals in
2006
let id = mkidentifier f.svar.vname f.svar.vdecl in
2008
Kernel_function.get_spec (Globals.Functions.get f.svar)
2012
mkexpr (JCPEdecl(ctype v.vtype,v.vname,None)) v.vdecl
2014
let locals = List.rev (List.rev_map local f.slocals) in
2015
let body = mkexpr (JCPEblock(statement_list f.sbody.bstmts)) pos in
2016
let body = locals @ [body] in
2017
let body = mkexpr (JCPEblock body) pos in
2019
(reg_pos ~id:f.svar.vname
2020
~name:("Function " ^ f.svar.vname) f.svar.vdecl);
2021
[JCDfun(ctype rty,id,formals,spec funspec,Some body)]
2022
with Errormsg.Error ->
2023
Format.printf "Dropping definition of function %s@." f.svar.vname;
2024
[JCDfun(ctype rty,id,formals,spec funspec,None)]
2027
| GAsm _ -> [] (* No assembly in Jessie *)
2029
| GPragma _ -> [] (* Pragmas treated separately *)
2031
| GText _ -> [] (* Ignore text in Jessie *)
2033
| GAnnot(la,_pos) -> annotation la
2036
let pos = get_globalLoc g in
2037
List.map (fun dnode -> mkdecl dnode pos) dnodes
2039
let integral_type name ty bitsize =
2040
let min = Num.num_of_big_int (min_value_of_integral_type ~bitsize ty) in
2041
let max = Num.num_of_big_int (max_value_of_integral_type ~bitsize ty) in
2042
mkdecl (JCDenum_type(name,min,max)) Loc.dummy_position
2044
(* let all_integral_kinds = *)
2045
(* let rec all_ik = function *)
2046
(* | IBool -> IBool :: (all_ik IChar) *)
2047
(* | IChar -> IChar :: (all_ik ISChar) *)
2048
(* | ISChar -> ISChar :: (all_ik IUChar) *)
2049
(* | IUChar -> IUChar :: (all_ik IInt) *)
2050
(* | IInt -> IInt :: (all_ik IUInt) *)
2051
(* | IUInt -> IUInt :: (all_ik IShort) *)
2052
(* | IShort -> IShort :: (all_ik IUShort) *)
2053
(* | IUShort -> IUShort :: (all_ik ILong) *)
2054
(* | ILong -> ILong :: (all_ik IULong) *)
2055
(* | IULong -> IULong :: (all_ik ILongLong) *)
2056
(* | ILongLong -> ILongLong :: (all_ik IULongLong) *)
2057
(* | IULongLong -> IULongLong :: [] *)
2061
let integral_types () =
2062
if Cmdline.Jessie.IntModel.get_val () = Cmdline.Jessie.IMexact then
2066
(fun name (ty,bitsize) acc -> integral_type name ty bitsize :: acc)
2067
all_integral_types []
2069
let type_conversions () =
2070
let typconv_axiom ty1 ty1_to_ty2 ty2_to_ty1 =
2071
let x = PExpr.mkvar ~name:"x" () in
2072
let app1 = PExpr.mkapp ~fun_name:ty1_to_ty2 ~args:[x] () in
2073
let app2 = PExpr.mkapp ~fun_name:ty2_to_ty1 ~args:[app1] () in
2074
let eq = PExpr.mkeq ~expr1:x ~expr2:app2 () in
2075
let forall = PExpr.mkforall ~typ:(ctype ty1) ~vars:["x"] ~body:eq () in
2076
PDecl.mklemma_def ~name:(unique_logic_name (ty1_to_ty2 ^ "_axiom")) ~axiom:true
2080
(fun _ (ty1,ty2,ty1_to_ty2,ty2_to_ty1) acc ->
2082
PDecl.mklogic_def ~typ:(ctype ty2) ~name:ty1_to_ty2
2083
~params:[ctype ty1, "x"] ~reads:[] ();
2084
PDecl.mklogic_def ~typ:(ctype ty1) ~name:ty2_to_ty1
2085
~params:[ctype ty2, "x"] ~reads:[] ();
2086
typconv_axiom ty1 ty1_to_ty2 ty2_to_ty1;
2087
typconv_axiom ty2 ty2_to_ty1 ty1_to_ty2
2089
) type_conversion_table []
2092
let filter_defined = function GFun _ | GVar _ -> true | _ -> false in
2094
function GFun(f,_) -> f.svar | GVar(vi,_,_) -> vi | _ -> assert false
2097
(* AVOID CHECKING THE GLOBAL INITIALIZATION FUNCTION, WHICH IS GUARANTEED *)
2098
(* if Globals.has_entry_point () then *)
2100
(* Kernel_function.get_definition (Globals.Functions.get_glob_init f) *)
2102
(* f.globals @ [GFun(gif,Loc.dummy_position)] *)
2106
List.rev (List.rev_map defined_var (List.filter filter_defined globals))
2108
(* Compute translation of [globals] before [integral_types] so that types
2111
List.flatten (List.rev (List.rev_map (global vardefs) globals))
2113
mkdecl (JCDaxiomatic("Padding",
2114
[mkdecl (JCDlogic_type name_of_padding_type)
2115
Loc.dummy_position]))
2117
(* Define all integral types as enumerated types in Jessie *)
2118
:: integral_types ()
2119
(* Define conversion functions and identity axiom for back
2120
and forth conversion *)
2121
@ type_conversions ()
2124
(* Translate pragmas separately as their is no declaration for pragmas in
2125
* the parsed AST of Jessie, only in its types AST.
2127
let pragma = function
2128
| GPragma(Attr(name,[AStr arg]),_)
2129
| GPragma(Attr(name,[ACons(arg,[])]),_) ->
2130
begin match name with
2131
| "InvariantPolicy" ->
2132
begin match String.lowercase arg with
2133
| "none" -> [Jc_output.JCinvariant_policy Jc_env.InvNone]
2135
[Jc_output.JCinvariant_policy Jc_env.InvArguments]
2137
[Jc_output.JCinvariant_policy Jc_env.InvOwnership]
2140
| "SeparationPolicy" ->
2141
begin match String.lowercase arg with
2142
| "none" -> [Jc_output.JCseparation_policy Jc_env.SepNone]
2143
| "regions" -> [Jc_output.JCseparation_policy Jc_env.SepRegions]
2146
| "AnnotationPolicy" ->
2147
begin match String.lowercase arg with
2148
| "none" -> [Jc_output.JCannotation_policy Jc_env.AnnotNone]
2150
[Jc_output.JCannotation_policy Jc_env.AnnotInvariants]
2152
[Jc_output.JCannotation_policy Jc_env.AnnotWeakPre]
2154
[Jc_output.JCannotation_policy Jc_env.AnnotStrongPre]
2157
| "AbstractDomain" ->
2158
begin match String.lowercase arg with
2159
| "none" -> [Jc_output.JCabstract_domain Jc_env.AbsNone]
2160
| "box" -> [Jc_output.JCabstract_domain Jc_env.AbsBox]
2161
| "oct" -> [Jc_output.JCabstract_domain Jc_env.AbsOct]
2162
| "pol" -> [Jc_output.JCabstract_domain Jc_env.AbsPol]
2166
begin match String.lowercase arg with
2167
| "real" -> float_model := `Real
2168
| "strict" -> float_model := `Strict
2169
| "full" -> float_model := `Full
2172
"Warning: pragma %s: identifier %s is not a valid value.\npragma is ignored.@." name s
2174
| "JessieIntegerModel" ->
2175
begin match String.lowercase arg with
2176
| "exact" | "math" ->
2177
Cmdline.Jessie.IntModel.set "exact"
2179
Cmdline.Jessie.IntModel.set "strict"
2181
Cmdline.Jessie.IntModel.set "modulo"
2184
"Warning: pragma %s: identifier %s is not a valid value.\npragma is ignored.@." name s
2189
"Warning: pragma %s is ignored by Jessie plugin.@." name;
2196
(match Cmdline.Jessie.IntModel.get_val () with
2197
| Cmdline.Jessie.IMexact -> []
2198
| Cmdline.Jessie.IMbounded -> [Jc_output.JCint_model Jc_env.IMbounded]
2199
| Cmdline.Jessie.IMmodulo -> [Jc_output.JCint_model Jc_env.IMmodulo])
2200
@ Jc_output.JCinvariant_policy Jc_env.InvArguments
2201
:: (if Cmdline.Jessie.SepRegions.get () then
2202
Jc_output.JCseparation_policy Jc_env.SepRegions
2204
Jc_output.JCseparation_policy Jc_env.SepNone)
2205
:: (match Cmdline.Jessie.InferAnnot.get () with
2206
| "" -> Jc_output.JCannotation_policy Jc_env.AnnotNone
2207
| "inv" -> Jc_output.JCannotation_policy Jc_env.AnnotInvariants
2208
| "pre" -> Jc_output.JCannotation_policy Jc_env.AnnotElimPre
2209
| "spre" -> Jc_output.JCannotation_policy Jc_env.AnnotStrongPre
2210
| "wpre" -> Jc_output.JCannotation_policy Jc_env.AnnotWeakPre
2212
Format.eprintf "unknown inference technique %s@." s; assert false)
2213
:: (match Cmdline.Jessie.AbsDomain.get () with
2214
| "box" -> Jc_output.JCabstract_domain Jc_env.AbsBox
2215
| "oct" -> Jc_output.JCabstract_domain Jc_env.AbsOct
2216
| "poly" -> Jc_output.JCabstract_domain Jc_env.AbsPol
2217
| s -> Format.eprintf "unknown abstract domain %s@." s; assert false)
2218
:: List.flatten (List.rev (List.rev_map pragma f.globals))
2223
compile-command: "LC_ALL=C make -C ../.. -j bin/toplevel.byte"
added
removed
src/jessie/interp.ml
