package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file cst_to_ast.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
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2019 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: you can redistribute it and/or modify     *)
(* it under the terms of the GNU Lesser General Public License as published *)
(* by the Free Software Foundation, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program is distributed in the hope that it will be useful,          *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of           *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the            *)
(* GNU Lesser General Public License for more details.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Translate a CST into a AST by resolving types, variables and
   functions defined in the project. *)

open Mopsa_utils
open Mopsa_c_parser
open Location
open Cst


let debug fmt = Debug.debug ~channel:"c_stubs_parser.passes.cst_to_ast" fmt


(** {2 Generic visitors} *)
(** ******************** *)

let rec visit_list visit l prj func =
  match l with
  | [] -> []
  | hd :: tl ->
    let hd' = visit hd prj func in
    let tl' = visit_list visit tl prj func in
    hd' :: tl'

let rec visit_list_ext visit l prj func =
  match l with
  | [] -> [], [], []
  | hd :: tl ->
    let hd', ext1, ext2 = visit hd prj func in
    let tl', ext1', ext2' = visit_list_ext visit tl prj func in
    hd' :: tl', ext1 @ ext1', ext2 @ ext2'

let visit_option visit o prj func =
  match o with
  | None -> None
  | Some x -> Some (visit x prj func)

let visit_pair visitor1 visitor2 (x, y) prj func =
  (visitor1 x prj func, visitor2 y prj func)


(** {2 Types} *)
(** ********* *)

let find_record r prj =
  let open C_AST in
  StringMap.bindings prj.proj_records |>
  List.split |>
  snd |>
  List.find (fun r' -> compare r'.record_org_name r.vname = 0)

let find_typedef t prj =
  let open C_AST in
  StringMap.bindings prj.proj_typedefs |>
  List.split |>
  snd |>
  List.find (fun t' -> compare t'.typedef_org_name t.vname = 0)

let find_enum e prj =
  let open C_AST in
  StringMap.bindings prj.proj_enums |>
  List.split |>
  snd |>
  List.find (fun e' -> compare e'.enum_org_name e.vname = 0)

let find_function f prj =
  try
    let open C_AST in
    bind_range f @@ fun f ->
    StringMap.bindings prj.proj_funcs |>
    List.split |>
    snd |>
    List.find (fun f' -> compare f'.func_org_name f.vname = 0)
  with Not_found ->
    Exceptions.panic_at f.range "function %s not found" f.content.vname

let rec unroll_type t =
  let open C_AST in
  match fst t with
  | T_typedef td -> unroll_type td.typedef_def
  | T_enum e -> T_integer (match e.enum_integer_type with Some s -> s | None -> assert false), snd t
  | _ -> t

let visit_qual q =
  C_AST.{
    qual_is_const = q.c_qual_const
  }

let rec visit_qual_typ t prj func : C_AST.type_qual=
  let (t0, q) = t in
  let t0' = visit_typ t0 prj func in
  let q' = visit_qual q in
  t0', q'

and visit_typ t prj func =
  match t with
  | T_void -> C_AST.T_void
  | T_char -> C_AST.(T_integer (Char SIGNED)) (* FIXME: get the signedness defined by the platform *)
  | T_signed_char -> C_AST.(T_integer SIGNED_CHAR)
  | T_unsigned_char -> C_AST.(T_integer UNSIGNED_CHAR)
  | T_signed_short -> C_AST.(T_integer SIGNED_SHORT)
  | T_unsigned_short -> C_AST.(T_integer UNSIGNED_SHORT)
  | T_signed_int -> C_AST.(T_integer SIGNED_INT)
  | T_unsigned_int -> C_AST.(T_integer UNSIGNED_INT)
  | T_signed_long -> C_AST.(T_integer SIGNED_LONG)
  | T_unsigned_long -> C_AST.(T_integer UNSIGNED_LONG)
  | T_signed_long_long -> C_AST.(T_integer SIGNED_LONG_LONG)
  | T_unsigned_long_long -> C_AST.(T_integer UNSIGNED_LONG_LONG)
  | T_signed_int128 -> C_AST.(T_integer SIGNED_INT128)
  | T_unsigned_int128 -> C_AST.(T_integer UNSIGNED_INT128)
  | T_float -> C_AST.(T_float FLOAT)
  | T_double -> C_AST.(T_float DOUBLE)
  | T_long_double -> C_AST.(T_float LONG_DOUBLE)
  | T_float128 -> C_AST.(T_float FLOAT128)
  | T_array(t, len) -> C_AST.T_array (visit_qual_typ t prj func , visit_array_length len prj func )
  | T_struct(s) -> C_AST.T_record (find_record s prj)
  | T_union(u) -> C_AST.T_record (find_record u prj)
  | T_typedef(t) -> C_AST.T_typedef (find_typedef t prj)
  | T_pointer(t) -> C_AST.T_pointer (visit_qual_typ t prj func )
  | T_enum(e) -> C_AST.T_enum (find_enum e prj)
  | T_unknown -> Exceptions.panic "unknown type not resolved"

and visit_array_length len prj func =
  match len with
  | A_no_length -> C_AST.No_length
  | A_constant_length n -> C_AST.Length_cst n


let int_type = C_AST.(T_integer SIGNED_INT, no_qual)
let bool_type = C_AST.(T_bool, no_qual)
let float_type = C_AST.(T_float FLOAT, no_qual)
let double_type = C_AST.(T_float DOUBLE, no_qual)
let long_type = C_AST.(T_integer SIGNED_LONG, no_qual)
let unsigned_long_type = C_AST.(T_integer UNSIGNED_LONG, no_qual)
let long_long_type = C_AST.(T_integer SIGNED_LONG_LONG, no_qual)
let unsigned_long_long_type = C_AST.(T_integer UNSIGNED_LONG_LONG, no_qual)
let string_type s = C_AST.(T_array((T_integer(SIGNED_CHAR), no_qual), Length_cst (Z.of_int (1 + String.length s))), no_qual)
let char_type = C_AST.(T_integer (Char SIGNED), no_qual)
let pointer_type t = C_AST.(T_pointer t, no_qual)
let void_type = C_AST.(T_void, no_qual)

let is_int_typ t =
  match unroll_type t |> fst with
  | C_AST.T_integer _ -> true
  | _ -> false

let is_float_typ t =
  match unroll_type t |> fst with
  | C_AST.T_float _ -> true
  | _ -> false

let is_pointer_typ t =
  match unroll_type t |> fst with
  | C_AST.T_pointer _ -> true
  | _ -> false

let is_array_typ t =
  match unroll_type t |> fst with
  | C_AST.T_array _ -> true
  | _ -> false

let pointed_type range t =
  match fst (unroll_type t) with
  | C_AST.T_pointer t' -> t'
  | C_AST.T_array(t', _) -> t'
  | _ -> Exceptions.panic_at range "pointed_type(cst_to_ast.ml): unsupported type %s" (C_print.string_of_type_qual t)

let is_record_typ t =
  match fst (unroll_type t) with
  | C_AST.T_record _ -> true
  | _ -> false
  

let subscript_type t = pointed_type t

let attribute_type obj f =
  Exceptions.warn "attribute_typ: supporting only int attributes";
  int_type

let builtin_type f args =
  match f with
  | LENGTH   -> unsigned_long_type
  | BYTES    -> unsigned_long_type
  | OFFSET -> long_type
  | INDEX  -> long_type
  | BASE   -> pointer_type C_AST.(T_void, no_qual)
  | PRIMED -> let arg = List.hd args in arg.content.Ast.typ
  | VALID_FLOAT | FLOAT_INF | FLOAT_NAN -> int_type
  | ALIVE    -> int_type
  | RESOURCE -> int_type


(** {2 Records} *)
(** *********** *)

let rec find_field range t f =
  match fst (unroll_type t) with
  | C_AST.T_record r ->
    let rec aux = function
      | [] -> raise Not_found

      | field::tl when field.C_AST.field_org_name = f ->
        field

      (* case of anonymous records *)
      | field::tl when field.field_org_name = "" && is_record_typ field.field_type ->
        begin
          try find_field range field.field_type f
          with Not_found -> aux tl
        end

      | _::tl -> aux tl
    in
    aux (Array.to_list r.C_AST.record_fields)

  | _ -> Exceptions.panic_at range "field_type(cst_to_ast.ml): unsupported type %s"
           (C_print.string_of_type_qual t)

let find_field_check t f range =
  try find_field range t f
  with Not_found ->
    Exceptions.panic_at range "type %s has no field named %s" (C_print.string_of_type_qual t) f


(** {2 Expressions} *)
(** *************** *)

let visit_var v range prj func =
  let open C_AST in
  if v.vlocal then
    {
      var_uid = v.vuid; (** FIXME: ensure that v.vuid is unique in the entire project *)
      var_org_name = v.vname;
      var_unique_name = v.vname ^ (string_of_int v.vuid); (** FIXME: give better unique names *)
      var_kind = Variable_local func;
      var_type = visit_qual_typ v.vtyp prj func;
      var_init = None;
      var_range = Clang_AST.{
          range_begin = {
            loc_file = get_range_start v.vrange |> get_pos_file;
            loc_line = get_range_start v.vrange |> get_pos_line;
            loc_column = get_range_start v.vrange |> get_pos_column;
          };
          range_end = {
            loc_file = get_range_end v.vrange |> get_pos_file;
            loc_line = get_range_end v.vrange |> get_pos_line;
            loc_column = get_range_end v.vrange |> get_pos_column;
          }
        };
      var_com = [];
      var_before_stmts = [];
      var_after_stmts = [];
    }
  else
    (* Search for the variable in the parameters of the function or
       the globals of the project *)
    let vars = Array.to_list func.func_parameters @
               (StringMap.bindings prj.proj_vars |> List.split |> snd)
    in
    try List.find (fun v' -> compare v'.var_org_name v.vname = 0) vars
    with Not_found -> Exceptions.panic_at range "undeclared variable %a" pp_var v

let int_rank =
  let open C_AST in
  function
  | Char _ | UNSIGNED_CHAR | SIGNED_CHAR -> 0
  | UNSIGNED_SHORT | SIGNED_SHORT -> 1
  | UNSIGNED_INT | SIGNED_INT -> 2
  | UNSIGNED_LONG | SIGNED_LONG -> 3
  | UNSIGNED_LONG_LONG | SIGNED_LONG_LONG -> 4
  | UNSIGNED_INT128 | SIGNED_INT128 -> 5

let int_sign =
  let open C_AST in
  function
  | SIGNED_CHAR | SIGNED_SHORT | SIGNED_INT | SIGNED_LONG
  | SIGNED_LONG_LONG | SIGNED_INT128 -> true
  | UNSIGNED_CHAR | UNSIGNED_SHORT | UNSIGNED_INT | UNSIGNED_LONG
  | UNSIGNED_LONG_LONG | UNSIGNED_INT128 -> false
  | Char SIGNED -> true
  | Char UNSIGNED -> false

let make_unsigned =
  let open C_AST in
  function
  | Char _ | UNSIGNED_CHAR | SIGNED_CHAR -> UNSIGNED_CHAR
  | UNSIGNED_SHORT | SIGNED_SHORT -> UNSIGNED_SHORT
  | UNSIGNED_INT | SIGNED_INT -> UNSIGNED_INT
  | UNSIGNED_LONG | SIGNED_LONG -> UNSIGNED_LONG
  | UNSIGNED_LONG_LONG | SIGNED_LONG_LONG -> UNSIGNED_LONG_LONG
  | UNSIGNED_INT128 | SIGNED_INT128 -> UNSIGNED_INT128

let rank_float =
  let open C_AST in
  function
  | FLOAT -> 0
  | DOUBLE -> 1
  | LONG_DOUBLE -> 2
  | FLOAT128 -> 3

let is_int_binop = function
  | EQ | NEQ | LT | LE | GT | GE | LAND | LOR -> true
  | _ -> false

let binop_type range prj t1 t2 =
  let open C_AST in
  let open C_utils in
  match fst (unroll_type t1), fst (unroll_type t2) with
  | x1, x2 when type_compatible prj.proj_target x1 x2 -> t1

  | T_float a, T_float b ->
     if rank_float a >= rank_float b then t1 else t2

  | T_float _, T_integer _ -> t1
  | T_integer _, T_float _ -> t2

  | T_integer a, T_integer b ->
     (* Usual arithmetic conversions (C99 6.3.1.8) *)
     (* same sign: the highest ranked wins *)
     if int_sign a = int_sign b then
       if int_rank a >= int_rank b then t1 else t2
     (* if the unsigned has greater or equal rank, it wins *)
     else if not (int_sign a) && int_rank a >= int_rank b then t1
     else if not (int_sign b) && int_rank b >= int_rank a then t2
     (* if the signed can hold all unsigned values, it wins *)
     else if int_sign a && sizeof_int prj.proj_target a > sizeof_int prj.proj_target b then t1
     else if int_sign b && sizeof_int prj.proj_target b > sizeof_int prj.proj_target a then t2
     (* otherwise, use an unsigned version of the signed type *)
     else if int_sign a then T_integer (make_unsigned a), snd t1
     else T_integer (make_unsigned b), snd t2

  | T_pointer _, T_integer _ -> t1
  | T_integer _, T_pointer _ -> t2

  | T_array _, T_integer _ -> t1
  | T_integer _, T_array _ -> t2

  | T_pointer (T_void,_), (T_pointer _ | T_array _) -> t2
  | (T_pointer _ | T_array _), T_pointer (T_void,_) -> t1
  | T_pointer (p1,_), T_pointer (p2,_) when type_equal prj.proj_target p1 p2 -> t1

  | T_pointer p, T_array (e,_) when type_qual_compatible prj.proj_target p e -> t1
  | T_array (e,_), T_pointer p when type_qual_compatible prj.proj_target p e -> t2

  | _ -> Exceptions.warn_at range "binop_type: unsupported case: %s and %s"
           (C_print.string_of_type_qual t1)
           (C_print.string_of_type_qual t2); t1

 (* Integer promotions (C99 6.3.1.1) *)
let integer_promotion prj (e: Ast.expr with_range) =
  let open C_AST in
  let open C_utils in
  bind_range e @@ fun ee ->
  let t = unroll_type ee.typ in
  match fst t with
  | T_integer (SIGNED_INT | UNSIGNED_INT |
               SIGNED_LONG | UNSIGNED_LONG |
               SIGNED_LONG_LONG | UNSIGNED_LONG_LONG |
               SIGNED_INT128 | UNSIGNED_INT128
              ) ->
    ee

  | T_integer (Char SIGNED | SIGNED_CHAR | SIGNED_SHORT) | T_bool ->
    let tt = (T_integer SIGNED_INT), snd t in
    { kind = E_cast(tt, false, e); typ = tt }

  | T_integer ((Char UNSIGNED | UNSIGNED_CHAR | UNSIGNED_SHORT) as i) ->
    (* signed int wins if it can represent all unsigned values *)
    let ii =
      if sizeof_int prj.proj_target i < sizeof_int prj.proj_target SIGNED_INT
      then SIGNED_INT
      else UNSIGNED_INT
    in
    let tt = (T_integer ii), snd t in
    { kind = E_cast(tt, false, e); typ = tt }

  | T_float _ -> ee

  | T_pointer _ -> ee

  | T_array _ -> ee

  | _ -> Exceptions.panic_at e.range "promote_expression_type: unsupported type %s"
           (C_print.string_of_type_qual t)

let promote_expression_type prj target_type (e: Ast.expr with_range) =
  if is_float_typ target_type then
    let t = e.content.typ in
    if target_type == t then e
    else
      with_range
        Ast.{ kind = E_cast(target_type, false, e); typ = target_type }
        e.range
  else
   integer_promotion prj e


let rec visit_expr e prj func : Ast.expr with_range =
  bind_range e @@ fun ee ->
  let kind, typ = match ee with
    | E_top t ->
      let t = visit_qual_typ t prj func in
      Ast.E_top t, t

    | E_int(n, NO_SUFFIX) -> Ast.E_int(n), int_type

    | E_int(n, LONG) -> Ast.E_int(n), long_type

    | E_int(n, UNSIGNED_LONG) -> Ast.E_int(n), unsigned_long_type

    | E_int(n, LONG_LONG) -> Ast.E_int(n), long_long_type

    | E_int(n, UNSIGNED_LONG_LONG) -> Ast.E_int(n), unsigned_long_long_type

    | E_float(f) -> Ast.E_float(f), float_type

    | E_string(s) -> Ast.E_string(s), string_type s

    | E_char(c) -> Ast.E_char(c), char_type

    | E_invalid -> Ast.E_invalid, pointer_type void_type

    | E_var(v) ->
      let v = visit_var v e.range prj func in
      Ast.E_var v, v.var_type

    | E_unop(op, e') ->
      let e' = visit_expr e' prj func in
      let e' = promote_expression_type prj e'.content.typ e' in
      let ee' =
        with_range
          Ast.{ kind = E_unop(op, e'); typ = e'.content.typ }
          e.range
      in
      E_cast(e'.content.typ, false, ee'), e'.content.typ

    | E_binop(op, e1, e2) ->
      let e1 = visit_expr e1 prj func in
      let e2 = visit_expr e2 prj func in

      let t = binop_type e.range prj e1.content.typ e2.content.typ in

      let e1 = promote_expression_type prj t e1 in
      let e2 = promote_expression_type prj t e2 in

      if is_int_binop op then
        E_binop(op, e1, e2), int_type
      else
        let ee = with_range Ast.{ kind = E_binop(op, e1, e2); typ = t } e.range in
        E_cast(t, false, ee), t

    | E_addr_of(e')       ->
      let e' = visit_expr e' prj func in
      Ast.E_addr_of e', pointer_type e'.content.typ

    | E_deref(e')         ->
      let e' = visit_expr e' prj func in
      Ast.E_deref e', pointed_type e.range e'.content.typ

    | E_cast(t, e') ->
      let t = visit_qual_typ t prj func in
      Ast.E_cast(t, true, visit_expr e' prj func ), t

    | E_subscript(a, i)   ->
      let a  = visit_expr a prj func in
      Ast.E_subscript(a, visit_expr i prj func ), subscript_type e.range a.content.typ

    | E_member(s, f)      ->
      let s = visit_expr s prj func in
      let field = find_field_check s.content.typ f e.range in
      Ast.E_member(s, field.field_index, f), field.field_type

    | E_arrow(p, f) ->
      let p = visit_expr p prj func in
      let field = find_field_check (pointed_type e.range p.content.typ) f e.range in
      Ast.E_arrow(p, field.field_index, f), field.field_type

    | E_conditional(c, e1, e2) ->
      let c = visit_expr c prj func in
      let e1 = visit_expr e1 prj func in
      let e2 = visit_expr e2 prj func in
      E_conditional(c, e1, e2), e1.content.typ (* FIXME: handle the case when e1 and e2 have different types *)

    | E_sizeof_expr(e) ->
      let e = visit_expr e prj func in
      let typ = match unroll_type e.content.typ |> fst with
        | C_AST.T_void -> C_AST.(T_integer SIGNED_CHAR)
        | t -> t in
      let size = C_utils.sizeof_type !target_info typ in
      Ast.E_int(size), int_type

    | E_sizeof_type(t) ->
      let typ, _ = visit_qual_typ t.content prj func in
      let size = C_utils.sizeof_type !target_info typ in
      Ast.E_int(size), int_type

    | E_builtin_call(f,args) ->
      let args = List.map (fun a -> visit_expr a prj func) args in
      Ast.E_builtin_call(f, args), builtin_type f args

    | E_return -> Ast.E_return, func.func_return

    | E_raise msg -> Ast.E_raise(msg), int_type
  in
  Ast.{ kind; typ }


(** {2 Formulas} *)
(** ************ *)

let visit_interval i prj func =
  { Ast.itv_lb = visit_expr i.itv_lb prj func;
    itv_open_lb = i.itv_open_lb;
    itv_ub = visit_expr i.itv_ub prj func;
    itv_open_ub = i.itv_open_ub;}


let visit_set s prj func =
  match s with
  | S_interval(itv) -> Ast.S_interval(visit_interval itv prj func)
  | S_resource(r) -> Ast.S_resource(r.vname)

let rec visit_formula f prj func =
  bind_range f @@ fun ff ->
  match ff with
  | F_expr(e) -> Ast.F_expr (visit_expr e prj func )
  | F_bool(b) -> Ast.F_bool b
  | F_binop(op, f1, f2) -> Ast.F_binop(op, visit_formula f1 prj func , visit_formula f2 prj func )
  | F_not f' -> Ast.F_not (visit_formula f' prj func)
  | F_forall(v, t, s, f') ->
    let v' = visit_var v f.range prj func in
    Ast.F_forall(v', visit_set s prj func, visit_formula f' prj func)
  | F_exists(v, t, s, f') ->
    let v' = visit_var v f.range prj func in
    Ast.F_exists(v', visit_set s prj func, visit_formula f' prj func)
  | F_in(e, s) -> Ast.F_in(visit_expr e prj func, visit_set s prj func)
  | F_otherwise(f, e) -> Ast.F_otherwise(visit_formula f prj func , visit_expr e prj func)
  | F_if(c, f1, f2) -> Ast.F_if(visit_formula c prj func , visit_formula f1 prj func, visit_formula f2 prj func)


(** {2 Stub sections} *)
(** **************** *)

let visit_requires req prj func =
  bind_range req @@ fun req ->
  visit_formula req prj func

let visit_assumes asm prj func =
  bind_range asm @@ fun asm ->
  visit_formula asm prj func

let visit_assigns a prj func =
  bind_range a @@ fun a ->
  Ast.{
    assign_target = visit_expr a.Cst.assign_target prj func;
    assign_offset = (visit_list @@ visit_interval) a.Cst.assign_offset prj func;
  }

let visit_ensures ens prj func =
  bind_range ens @@ fun ens ->
  visit_formula ens prj func

let visit_free free prj func =
  bind_range free @@ fun free ->
  visit_expr free prj func

let visit_local loc prj func =
  bind_range loc @@ fun l ->
  let lvar = visit_var l.lvar loc.range prj func in
  let lval =
    match l.lval with
    | L_new r -> Ast.L_new r.vname
    | L_call (f, args) ->
      let f = find_function f prj in
      (* Check arguments number *)
      let given = List.length args in
      let accepted = Array.length f.content.func_parameters in
      if not f.content.func_variadic then
        ( if given <> accepted then
            Exceptions.panic_at loc.range "function '%s' accepts %d argument%a, but %d given"
              f.content.func_org_name
              accepted Debug.plurial_int accepted
              given )
      else
        ( if given < accepted then
            Exceptions.panic_at loc.range "function '%s' accepts at least %d argument%a, but %d given"
              f.content.func_org_name
              accepted Debug.plurial_int accepted
              given );
      Ast.L_call (f, visit_list visit_expr args prj func)
  in
  Ast.{ lvar; lval }

let visit_message msg prj func =
  bind_range msg @@ fun m ->
  { Ast.message_kind = m.message_kind;
    message_body = m.message_body; }

let visit_leaf leaf prj func =
  match leaf with
  | Cst.S_local local ->
    let local = visit_local local prj func in
    Ast.S_local local, [local], []

  | S_assumes assumes ->
    S_assumes (visit_assumes assumes prj func), [], []

  | S_requires requires ->
    S_requires (visit_requires requires prj func), [], []

  | S_assigns assigns ->
    let assigns = visit_assigns assigns prj func in
    S_assigns assigns, [], [assigns]

  | S_ensures ensures ->
    S_ensures (visit_ensures ensures prj func), [], []

  | S_free free ->
    S_free (visit_free free prj func), [], []

  | S_message msg ->
    S_message (visit_message msg prj func), [], []

let visit_case case prj func =
  let body, locals, assigns = visit_list_ext visit_leaf case.content.case_body prj func in
  Ast.{
    case_label = case.content.case_label;
    case_body = body;
    case_locals = locals;
    case_assigns = assigns;
    case_range = case.range;
  }, assigns

let visit_section sect prj func =
  match sect with
  | Cst.S_leaf leaf ->
    let leaf, locals, assigns = visit_leaf leaf prj func in
    Ast.S_leaf leaf, locals, assigns

  | S_case case ->
    let case, assigns = visit_case case prj func in
    S_case (case), [], assigns


(** {2 Entry point} *)
(** *************** *)

let doit
    (prj:C_AST.project)
    (func: C_AST.func)
    (stub:Cst.stub)
  : Ast.stub
  =
  let body, locals, assigns = visit_list_ext visit_section stub.content prj func in
  Ast.{
    stub_name = func.C_AST.func_org_name;
    stub_params = Array.to_list func.C_AST.func_parameters;
    stub_body = body;
    stub_locals = locals;
    stub_assigns = assigns;
    stub_range = stub.range;
  }
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct