package mopsa

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

Source file frontend.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
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(**
   Universal frontend translates the parser's AST into Framework's AST.
*)

open Mopsa
open Mopsa_universal_parser

module NameG =
struct
  let compt = ref 0
  let fresh () =
    let rep = !compt in
    incr compt;
    rep
end

open Lexing
open Ast
open Mopsa

module T = Ast
module U = U_ast

module Float = ItvUtils.Float

(* vars to their unique identifier and declared types *)
module MS = MapExt.StringMap
type var_context = (int * typ) MS.t
type fun_context = (T.fundec) MS.t

let builtin_functions =
  [
    {name = "mopsa_assume"; args = [None]; output = T_unit};
    {name = "append"; args = [Some (T_array T_int); Some T_int]; output = T_unit};
  ]

let from_extent (e: U.extent) : Location.range = e

type uvar = {
  uvar_range: range;
  uvar_uid: int;
  uvar_orig_name: string;
  uvar_uniq_name: string;
}

type var_kind +=
  | V_uvar of uvar

let () = register_var {
    print = (fun next fmt v ->
        match vkind v with
        | V_uvar var ->
          if !Framework.Core.Ast.Var.print_uniq_with_uid then
            Format.fprintf fmt "%s:%a" var.uvar_orig_name pp_relative_range var.uvar_range
          else Format.fprintf fmt "%s" var.uvar_orig_name
        | _ -> next fmt v
      );

    compare = (fun next v1 v2 ->
        match vkind v1, vkind v2 with
        | V_uvar var1, V_uvar var2 ->
          Compare.compose [
            (fun () -> Stdlib.compare var1.uvar_uid var2.uvar_uid);
            (fun () -> Stdlib.compare var1.uvar_uniq_name var2.uvar_uniq_name)
          ]

        | _ -> next v1 v2
      );
  }
       

let from_var (v: string) (ext: U.extent) (var_ctx: var_context) =
  try
    let (id, typ) = MS.find v var_ctx in
    let uniq_name =  (v ^ ":" ^ string_of_int id) in 
    mkv uniq_name
      (V_uvar {
          uvar_range = ext;
          uvar_uid = id;
          uvar_orig_name = v;
          uvar_uniq_name = uniq_name
        })
      typ
  with
  | Not_found ->
    Exceptions.panic_at ext
      "%s was not found in typing/naming context"
      v

let rec from_typ (typ: U_ast.typ) : typ =
  match typ with
  | AST_INT     -> T_int
  | AST_REAL    -> T_float F_DOUBLE
  | AST_ARRAY t -> T_array (from_typ t)
  | AST_STRING  -> T_string
  | AST_CHAR    -> T_char

(* find a common type for the arguments of binary operations *)
let unify_typ (x:typ) (y:typ) : typ =
  match x,y with
  | T_int, T_float _ -> y
  | T_float _, T_int -> x
  | _ ->
     if compare_typ x y = 0 then x
     else Exceptions.panic "cannot unify types %a and %a" pp_typ x pp_typ y

(* cast expression to the given type (if needed) *)
let to_typ (t:typ) (e:expr) : expr =
  let range = erange e in
  let orgt = etyp e in
  if compare_typ orgt t = 0 then e
  else
    match ekind e, orgt, t with
    | _, (T_int | T_float _), (T_int | T_float _) ->
      mk_unop O_cast e ~etyp:t range
    | E_constant (C_top T_any), T_any, t ->
      {e with ekind = E_constant (C_top t); etyp = t}
    | _ -> 
      Exceptions.panic "cannot convert expression %a of type %a to type %a" pp_expr e pp_typ orgt pp_typ t

let from_binop (t: typ) (b: U.binary_op) : operator =
  match t, b with
  | T_int, AST_PLUS          -> O_plus
  | T_int, AST_MINUS         -> O_minus
  | T_int, AST_MULTIPLY      -> O_mult
  | T_int, AST_DIVIDE        -> O_div
  | T_int, AST_EQUAL         -> O_eq
  | T_int, AST_NOT_EQUAL     -> O_ne
  | T_int, AST_LESS          -> O_lt
  | T_int, AST_LESS_EQUAL    -> O_le
  | T_int, AST_GREATER       -> O_gt
  | T_int, AST_GREATER_EQUAL -> O_ge
  | T_int, AST_AND           -> O_log_and
  | T_int, AST_OR            -> O_log_or
  | T_string, AST_CONCAT        -> O_concat
  | T_string, AST_PLUS        -> O_concat
  | T_string, AST_EQUAL         -> O_eq
  | T_float _, AST_PLUS          -> O_plus
  | T_float _, AST_MINUS         -> O_minus
  | T_float _, AST_MULTIPLY      -> O_mult
  | T_float _, AST_DIVIDE        -> O_div
  | T_float _, AST_EQUAL         -> O_eq
  | T_float _, AST_NOT_EQUAL     -> O_ne
  | T_float _, AST_LESS          -> O_lt
  | T_float _, AST_LESS_EQUAL    -> O_le
  | T_float _, AST_GREATER       -> O_gt
  | T_float _, AST_GREATER_EQUAL -> O_ge
  | T_array _, AST_CONCAT -> O_concat
  | _ -> Exceptions.panic "operator %a cannot be used with type %a" U_ast_printer.print_binary_op b pp_typ t

let from_unop (t: typ) (b: U.unary_op) : operator =
  match t, b with
  | T_int, AST_UNARY_PLUS    -> O_plus
  | T_int, AST_UNARY_MINUS   -> O_minus
  | T_int, AST_NOT           -> O_log_not
  | T_float f, AST_UNARY_PLUS  -> O_plus
  | T_float f, AST_UNARY_MINUS -> O_minus
  | T_float f, AST_ROUND -> O_cast
  | _ -> Exceptions.panic "operator %a cannot be used with type %a" U_ast_printer.print_unary_op b pp_typ t

let rec from_expr (e: U.expr) (ext : U.extent) (var_ctx: var_context) (fun_ctx: fun_context option): expr =
  let range = from_extent ext in
  match e with
  | AST_unit_const -> mk_expr ~etyp:T_unit (E_constant (C_unit)) range
  | AST_fun_call((f, f_ext), args) ->
    begin
      let look_in_builtins (fun_ctx) =
        let exception Match of (expr list * fun_builtin) in
        try
          List.iter (fun (bi:fun_builtin) ->
              let () = Debug.debug ~channel:("remove_me") "builtin: %s, fun: %s, b: %b" bi.name f (bi.name = f) in
              if bi.name = f && List.length bi.args = List.length args then
                let exception NoMatch in
                try
                  let el = List.map2 (fun (e, ext) x ->
                      match x with
                      | Some x ->
                        let e' = from_expr e ext var_ctx (fun_ctx) in
                        let typ = etyp e' in
                        let () = Debug.debug ~channel:("remove_me") "x: %a, typ: %a" pp_typ x pp_typ typ in
                        if compare_typ typ x = 0 then
                          e'
                        else
                          raise NoMatch
                      | None -> from_expr e ext var_ctx (fun_ctx)
                    ) args bi.args
                  in
                  raise (Match (el, bi))
                with
                | NoMatch -> ()
            ) builtin_functions;
          Exceptions.panic_at ext
            "%s was not found in naming context nor in builtin functions"
            f
        with
        | Match(el, bi) ->
          (mk_expr ~etyp:(bi.output) (E_call(mk_expr (E_function (Builtin bi)) range, el)) range)
      in
      match fun_ctx with
      | None -> look_in_builtins (None)
      | Some fun_ctx ->
        begin
          try
            let fundec = MS.find f fun_ctx in
            if List.length fundec.fun_parameters = List.length args then
              let el = List.map2 (fun (e, ext) x ->
                  let e' = from_expr e ext var_ctx (Some fun_ctx) in
                  let typ = etyp e' in
                  if compare_typ x.vtyp typ = 0 then
                    e'
                  else
                    Exceptions.panic_at ext
                      "type of %a incompatible with declared function"
                      U_ast_printer.print_expr e
                ) args fundec.fun_parameters in
              let rettyp =
                match fundec.fun_return_type with
                | None -> T_int
                | Some t -> t
              in
              (mk_expr ~etyp:rettyp (E_call(mk_expr (E_function (User_defined fundec)) range, el)) range)
            else
              Exceptions.panic_at ext
                "%s number of arguments incompatible with call"
                f
          with
          | Not_found ->
            begin
              look_in_builtins (Some fun_ctx)
            end
        end
    end
  | AST_unary (op, (e, ext)) ->
    begin
      let e = from_expr e ext var_ctx fun_ctx in
      let typ = etyp e in
      let op = from_unop typ op in
      mk_unop op e ~etyp:typ range
    end
  | AST_binary (op, (e1, ext1), (e2, ext2)) ->
    begin
      let e1 = from_expr e1 ext1 var_ctx fun_ctx in
      let typ1 = etyp e1 in
      let e2 = from_expr e2 ext2 var_ctx fun_ctx in
      let typ2 = etyp e2 in
      let typ = unify_typ typ1 typ2 in
      let e1,e2 = to_typ typ e1, to_typ typ e2 in
      let op = from_binop typ op in
      mk_binop e1 op e2 ~etyp:typ range
    end

  | AST_identifier (v, ext) ->
    mk_var (from_var v ext var_ctx) range

  | AST_int_const (s, _) ->
    mk_z (Z.of_string s) range

  | AST_bool_const (b, _) ->
    mk_int (if b then 1 else 0) range

  | AST_real_const (s, _) ->
     (* double interval enclosing the real value *)
     let lo = Float.of_string `DOUBLE `DOWN s
     and up = Float.of_string `DOUBLE `UP s
     in
     mk_float_interval ~prec:F_DOUBLE lo up range

  | AST_string_const (s, _) ->
    mk_string s range

  | AST_char_const(c, _) ->
    mk_int ~typ:T_int (int_of_char c) range

  | AST_array_const(a, _) ->
     mk_expr (E_array (List.map (fun (e, ext) -> from_expr e ext var_ctx fun_ctx) (Array.to_list a))) range

  | AST_rand((l, _), (u, _)) ->
    mk_z_interval (Z.of_string l) (Z.of_string u) range

  | AST_randf((l, _), (u, _)) ->
    mk_float_interval (float_of_string l) (float_of_string u) range

  | AST_rand_string ->
    mk_top T_any range

  | AST_array_access((e1, ext1), (e2, ext2)) ->
    begin
      let e1o = e1 in
      let e1 = from_expr e1 ext1 var_ctx fun_ctx in
      let e2 = from_expr e2 ext2 var_ctx fun_ctx in
      let e2 = to_typ T_int e2 in
      match etyp e1 with
      | T_string -> mk_expr (E_subscript(e1, e2)) ~etyp:T_int range
      | T_array t -> mk_expr (E_subscript(e1, e2)) ~etyp:t range
      | _ -> Exceptions.panic_at ext
               "%a is of type %a and can not be subscripted"
               U_ast_printer.print_expr e1o
               (pp_typ) (etyp e1)
    end

  | AST_len (e, ext) ->
    begin
      let e1 = from_expr e ext var_ctx fun_ctx in
      match etyp e1 with
      | T_string
      | T_array _ -> mk_expr (E_len e1) ~etyp:T_int range
      | _ -> Exceptions.panic_at ext "%a is of type %a and can not be lengthed"
               U_ast_printer.print_expr e
               (pp_typ) (etyp e1)
    end

let rec from_stmt (s: U.stat) (ext: U.extent) (var_ctx: var_context) (fun_ctx: fun_context option): stmt =
  let range = from_extent ext in
  match s with
  | AST_block l ->
    mk_block (List.map (fun (x, ext) -> from_stmt x ext var_ctx fun_ctx) l) range

  | AST_assign((e1, ext1), (e2, ext2)) ->
    begin
      let e1o = e1 in
      match e1 with
      | AST_array_access(_, _)
      | AST_identifier _ ->
        let e1 = from_expr e1 ext1 var_ctx fun_ctx in
        let e2 = from_expr e2 ext2 var_ctx fun_ctx in
        let e2 = to_typ (etyp e1) e2 in
        mk_assign e1 e2 range
      | _ ->
        Exceptions.panic_at ext "%a not considered a left-value for now "
          U_ast_printer.print_expr e1o
    end

  | AST_if((e1, ext_e1), (s1, ext_s1), Some (s2, ext_s2)) ->
    let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
    let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
    let s2 = from_stmt s2 ext_s2 var_ctx fun_ctx in
    mk_if e1 s1 s2 range

  | AST_if((e1, ext_e1), (s1, ext_s1), None) ->
    let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
    let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
    mk_if e1 s1 (mk_nop range) range

  | AST_while((e1, ext_e1), (s1, ext_s1)) ->
    let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
    let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
    mk_while e1 s1 range

  | AST_for((v1, ext_v1), (e1, ext_e1), (e2, ext_e2), (s1, ext_s1)) ->
    let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
    let e2 = from_expr e2 ext_e2 var_ctx fun_ctx in
    let v  = from_var v1 ext_v1 var_ctx in
    let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
    mk_block
      [
        mk_assign
          (mk_var v (tag_range range "var_init_for_variable"))
          e1
          (tag_range range "expr_init_for_variable");
        mk_while
          (mk_binop
             (mk_var v (tag_range range "var_comp_for"))
             O_le
             e2
             ~etyp:(T_int)
             (tag_range range "comp_for")
          )
          (mk_block (
              [
                s1;
                mk_assign
                  (mk_var v (tag_range range "var_incr_for"))
                  (mk_binop
                     (mk_var v (tag_range range "var_incr_for"))
                     O_plus
                     (mk_z Z.one (tag_range range "one_for"))
                     ~etyp:(T_int)
                     (tag_range range "incr_for")
                  )
                  (tag_range range "assign_for")
              ])
              (tag_range range "body_for")
          )
          (tag_range range "total_for")
      ]
      range

  | AST_return (Some (e, ext)) ->
    let e = from_expr e ext var_ctx fun_ctx in
    {skind = S_return (Some e);
     srange = range
    }

  | AST_return None ->
    {skind = S_return None;
     srange = range
    }

  | AST_break ->
    {skind = S_break; srange = range}

  | AST_continue ->
    {skind = S_continue; srange = range}

  | AST_assert (e, ext) ->
    let e = from_expr e ext var_ctx fun_ctx in
    mk_assert e range

  | AST_assume (e, ext) ->
    let e = from_expr e ext var_ctx fun_ctx in
    mk_assume e range


  | AST_print ->
    mk_stmt S_print_state range

  | AST_expr(e, ext) ->
    let e' = from_expr e ext var_ctx fun_ctx in
    mk_expr_stmt e' range

let rec check_declaration_list (dl : U.declaration U.ext list) =
  match dl with
  | p::q -> aux p q; check_declaration_list q
  | [] -> ()
and aux (((((_,v),e),_),_) as p : U.declaration U.ext) (dl: U.declaration U.ext list) =
  match dl with
  | ((((_,v'),e'),_),_)::q when v = v' -> Exceptions.panic_at e "%s has already been declared at %a"
                                            v'
                                            pp_range e'
  | p':: q -> aux p q
  | [] -> ()

let var_ctx_of_declaration (dl : U_ast.declaration U.ext list) (var_ctx: var_context) =
  let () = check_declaration_list dl in
  let add_var var_ctx v t =
    try
      MS.add v (NameG.fresh (), t) var_ctx
    with
    | Not_found ->
      MS.add v (NameG.fresh (), t) var_ctx
  in
  let var_ctx, gvars = List.fold_left (fun (var_ctx, gvars) ((((t, v), extv ), o), e) ->
      let new_var_ctx = add_var var_ctx v (from_typ t) in
      let vv = from_var v extv new_var_ctx in
      (new_var_ctx, vv :: gvars)
    ) (var_ctx, []) dl in
  var_ctx, gvars

let var_ctx_init_of_declaration (dl : U_ast.declaration U.ext list) (var_ctx: var_context) (fun_ctx: fun_context option) (nvar_ctx)=
  let add_var var_ctx v t =
    try
      match nvar_ctx with
      | Some nvar_ctx -> MS.add v (MS.find v nvar_ctx) var_ctx
      | None -> MS.add v (NameG.fresh (), t) var_ctx
    with
    | Not_found ->
      assert false
  in
  let var_ctx, init, gvars = List.fold_left (fun (var_ctx, init, gvars) ((((t, v), extv ), o), e) ->
      let new_var_ctx = add_var var_ctx v (from_typ t) in
      let vv = from_var v extv new_var_ctx in
      let range = from_extent extv in 
      let stmt_add = mk_add
          (mk_var vv (tag_range range "initializer_var"))
          (tag_range range "initializer") in
      let init = stmt_add :: init in 
      match o with
      | Some (e, ext) ->
        let e = from_expr e ext var_ctx fun_ctx in
        let e = to_typ (from_typ t) e in
        let range = from_extent ext in
        let stmt_init =
          mk_assign
            (mk_var vv (tag_range range "initializer_var"))
            e
            (tag_range range "initializer")
        in
        (new_var_ctx, stmt_init :: init, vv :: gvars)
      | None   ->
        (new_var_ctx, init, vv :: gvars)
    ) (var_ctx, [], []) dl in
  var_ctx, List.rev init, gvars

let var_ctx_of_function (var_ctx: var_context) (fundec: U.fundec) =
  let add_var var_ctx v t =
    try
      MS.add v (NameG.fresh (), t) var_ctx
    with
    | Not_found ->
      MS.add v (NameG.fresh (), t) var_ctx
  in
  let var_ctx = List.fold_left (fun acc ((t, v), _) ->
      add_var acc v (from_typ t)
    ) var_ctx fundec.parameters in
  let var_ctx, _ =
    var_ctx_of_declaration fundec.locvars var_ctx
  in
  var_ctx

let var_init_of_function (var_ctx: var_context) var_ctx_map (fun_ctx: fun_context) (fundec: U.fundec) =
  let nvar_ctx = MS.find fundec.funname var_ctx_map in
  let add_var var_ctx n_var_ctx v t =
    try
      MS.add v (MS.find v n_var_ctx) var_ctx
    with
    | Not_found ->
      assert false
  in
  let var_ctx = List.fold_left (fun acc ((t, v), _) ->
      add_var acc nvar_ctx v (from_typ t)
    ) var_ctx fundec.parameters in
  let var_ctx, init, _ =
    var_ctx_init_of_declaration fundec.locvars var_ctx (Some (fun_ctx)) (Some nvar_ctx)
  in
  var_ctx, init


let from_fundec (f: U.fundec) (var_ctx: var_context): T.fundec =
  let typ = OptionExt.lift from_typ f.return_type in
  {
    fun_orig_name = f.funname;
    fun_uniq_name = f.funname;
    fun_range = from_extent f.range;
    fun_parameters = List.map (fun ((_, v), ext) -> from_var v ext var_ctx) f.parameters;
    fun_locvars = List.map (fun ((((_, v), _), _), ext) -> from_var v ext var_ctx) f.locvars;
    fun_body = mk_nop (from_extent (snd f.body));
    fun_return_type = typ;
    fun_return_var = None;
  }

let fun_ctx_of_global (fl: U_ast.fundec U.ext list) (var_ctx: var_context) =
  List.fold_left (fun (acc, var_ctx_map) (fundec, _) ->
      let var_ctx = var_ctx_of_function var_ctx fundec in
      (MS.add fundec.funname (from_fundec fundec var_ctx) acc, MS.add fundec.funname var_ctx var_ctx_map)
    ) (MS.empty, MS.empty) fl

let add_body (fl: fun_context) (f: string) (b: stmt): unit =
  try
    let fundec = MS.find f fl in
    fundec.fun_body <- b;
  with
  | Not_found -> Exceptions.panic "[Universal.frontend] should not happen"

let from_prog (p: U_ast.prog) : prog_kind =
  let ext = snd (p.main) in
  let var_ctx, init, gvars = var_ctx_init_of_declaration p.gvars MS.empty None None in
  let fun_ctx, var_ctx_map = fun_ctx_of_global p.funs var_ctx in
  List.iter (fun (fundec, ext) ->
      let var_ctx, init = var_init_of_function var_ctx var_ctx_map fun_ctx fundec in
      let body = from_stmt (fst fundec.body) (snd fundec.body) var_ctx (Some fun_ctx) in
      let total = mk_block (init @ [body]) (from_extent ext) in
      add_body fun_ctx fundec.funname total
    ) p.funs;
  let total = from_stmt (fst p.main) (snd p.main) var_ctx (Some fun_ctx) in
  let with_init = mk_block (init @ [total]) (from_extent ext) in
  P_universal
    {
      universal_gvars   = gvars;
      universal_fundecs = (MS.bindings fun_ctx) |> List.map (snd);
      universal_main    = with_init
    }

let rec parse_program (files: string list): program =
  match files with
  | [filename] ->
    let ast = U_file_parser.parse_file filename in
    {
      prog_kind = from_prog ast;
      prog_range = mk_program_range [filename];
    }

  | [] -> panic "no input file"

  | _ -> panic "analysis of multiple files not supported"


(* Front-end registration *)
let () =
  register_frontend {
    lang = "universal";
    parse = parse_program;
    on_panic = fun _ _ _ -> ();
  }
OCaml

Innovation. Community. Security.