plugins/cfg/cfg_parser.mly

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 %{
  13
  14   open Why3
  15   open Cfg_ast
  16
  17   let floc s e = Loc.extract (s,e)
  18
  19   let mk_cfginstr d s e = { cfg_instr_desc = d; cfg_instr_loc = floc s e }
  20   let mk_cfgterm d s e = { cfg_term_desc = d; cfg_term_loc = floc s e }
  21
  22 %}
  23
  24 (* extra tokens *)
  25 %token CFG GOTO VAR SWITCH
  26
  27 %start cfgfile
  28 %type <Cfg_ast.cfg_file> cfgfile
  29 %type <Cfg_ast.cfg_instr list * Cfg_ast.cfg_term> sequence
  30 %type <Cfg_ast.switch_branch list> cases
  31
  32 %%
  33
  34 cfgfile:
  35   | ml=cfgmodule* EOF { ml }
  36 ;
  37
  38 cfgmodule:
  39   | id=module_head_parsing_only dl=cfgdecl* END
  40     { (id,dl) }
  41
  42 cfgdecl:
  43   | scope_head_parsing_only cfgdecl* END
  44       { let loc,import,qid = $1 in (Cfg_ast.Dscope(loc,import,qid,$2))}
  45   | IMPORT uqualid { (Dmlw_decl (Dimport $2)) }
  46   | d = pure_decl | d = prog_decl | d = meta_decl { Dmlw_decl d }
  47   | use_clone_parsing_only { Dmlw_decl $1 }
  48   | LET CFG f=recdefn { Dletcfg f }
  49   | LET REC CFG dl=with_list1(recdefn) { Dreccfg dl }
  50 ;
  51
  52 recdefn:
  53   | cf_name=attrs(lident_rich) cf_args=binders COLON ret=return_named sp=spec EQUAL
  54       cf_attrs=attr* cf_locals=vardecls cf_block0=block cf_blocks=labelblock*
  55     { let cf_pat, cf_retty, cf_mask = ret in
  56       let cf_spec = apply_return cf_pat sp in
  57       { cf_name; cf_args; cf_retty; cf_pat; cf_mask; cf_spec; cf_attrs;
  58         cf_locals; cf_block0; cf_blocks } }
  59 ;
  60
  61 vardecls:
  62   | /* epsilon */ { [] }
  63   | vardecl vardecls { $1 @ $2 }
  64 ;
  65
  66 vardecl:
  67   | g=ghost_opt VAR vl=attrs(lident_nq)* COLON t=ty init=init_opt SEMICOLON
  68     { List.map (fun id -> (g,id,t, init)) vl }
  69 ;
  70
  71 init_opt:
  72 | /* epsilon */ { None }
  73 | EQUAL contract_expr { Some($2) }
  74
  75 ghost_opt:
  76   | /* epsilon */ { false }
  77   | GHOST         { true }
  78
  79 labelblock:
  80   | id = attrs(uident) b=block  { (id,b) }
  81 ;
  82
  83 block:
  84   | LEFTBRC sequence RIGHTBRC { $2 }
  85 ;
  86
  87 sequence:
  88   | terminator { ([], $1) }
  89   | x=instr SEMICOLON xl = sequence { (x :: fst xl, snd xl) }
  90 ;
  91
  92 instr:
  93   | contract_expr
  94     { mk_cfginstr (CFGexpr $1) $startpos $endpos }
  95   | VARIANT LEFTBRC t=term RIGHTBRC
  96     { mk_cfginstr (CFGinvariant [Variant, None, t, ref None]) $startpos $endpos }
  97   | INVARIANT nm=option(ident) LEFTBRC t=term RIGHTBRC
  98     { mk_cfginstr (CFGinvariant [Invariant, nm, t, ref None]) $startpos $endpos }
  99 ;
 100
 101 terminator :
 102   | GOTO uident
 103     { mk_cfgterm (CFGgoto $2) $startpos $endpos }
 104   | SWITCH LEFTPAR contract_expr RIGHTPAR cases END
 105     { mk_cfgterm (CFGswitch ($3,$5)) $startpos $endpos }
 106   | RETURN contract_expr
 107     { mk_cfgterm (CFGreturn $2) $startpos $endpos }
 108   | ABSURD
 109     { mk_cfgterm CFGabsurd $startpos $endpos }
 110 ;
 111
 112 cases:
 113   | BAR match_case(terminator)
 114     { [$2] }
 115   | BAR match_case(terminator) cases
 116     { $2 :: $3 }
 117 ;