cparser/Cabshelper.ml

   1 (* *********************************************************************)
   2 (*                                                                     *)
   3 (*              The Compcert verified compiler                         *)
   4 (*                                                                     *)
   5 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
   6 (*                                                                     *)
   7 (*  Copyright Institut National de Recherche en Informatique et en     *)
   8 (*  Automatique.  All rights reserved.  This file is distributed       *)
   9 (*  under the terms of the GNU General Public License as published by  *)
  10 (*  the Free Software Foundation, either version 2 of the License, or  *)
  11 (*  (at your option) any later version.  This file is also distributed *)
  12 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
  13 (*                                                                     *)
  14 (* *********************************************************************)
  15
  16
  17 open Cabs
  18
  19 let nextident = ref 0
  20 let getident () =
  21     nextident := !nextident + 1;
  22     !nextident
  23
  24 let currentLoc_lexbuf lb =
  25   let p = Lexing.lexeme_start_p lb in
  26   { lineno   = p.Lexing.pos_lnum;
  27     filename = p.Lexing.pos_fname;
  28     byteno   = p.Lexing.pos_cnum;
  29     ident    = getident ();}
  30
  31 let currentLoc () =
  32   let p = Parsing.symbol_start_pos() in
  33   { lineno   = p.Lexing.pos_lnum;
  34     filename = p.Lexing.pos_fname;
  35     byteno   = p.Lexing.pos_cnum;
  36     ident    = getident ();}
  37
  38 let cabslu = {lineno = -10;
  39               filename = "cabs loc unknown";
  40               byteno = -10;
  41               ident = 0}
  42
  43 (*********** HELPER FUNCTIONS **********)
  44
  45 let missingFieldDecl = ("___missing_field_name", JUSTBASE, [], cabslu)
  46
  47 let rec isStatic = function
  48     [] -> false
  49   | (SpecStorage STATIC) :: _ -> true
  50   | _ :: rest -> isStatic rest
  51
  52 let rec isExtern = function
  53     [] -> false
  54   | (SpecStorage EXTERN) :: _ -> true
  55   | _ :: rest -> isExtern rest
  56
  57 let rec isInline = function
  58     [] -> false
  59   | SpecInline :: _ -> true
  60   | _ :: rest -> isInline rest
  61
  62 let rec isTypedef = function
  63     [] -> false
  64   | SpecTypedef :: _ -> true
  65   | _ :: rest -> isTypedef rest
  66
  67
  68 let get_definitionloc (d : definition) : cabsloc =
  69   match d with
  70   | FUNDEF(_, _, l, _) -> l
  71   | DECDEF(_, l) -> l
  72   | TYPEDEF(_, l) -> l
  73   | ONLYTYPEDEF(_, l) -> l
  74   | GLOBASM(_, l) -> l
  75   | PRAGMA(_, l) -> l
  76   | LINKAGE (_, l, _) -> l
  77
  78 let get_statementloc (s : statement) : cabsloc =
  79 begin
  80   match s with
  81   | NOP(loc) -> loc
  82   | COMPUTATION(_,loc) -> loc
  83   | BLOCK(_,loc) -> loc
  84 (*  | SEQUENCE(_,_,loc) -> loc *)
  85   | IF(_,_,_,loc) -> loc
  86   | WHILE(_,_,loc) -> loc
  87   | DOWHILE(_,_,loc) -> loc
  88   | FOR(_,_,_,_,loc) -> loc
  89   | BREAK(loc) -> loc
  90   | CONTINUE(loc) -> loc
  91   | RETURN(_,loc) -> loc
  92   | SWITCH(_,_,loc) -> loc
  93   | CASE(_,_,loc) -> loc
  94   | CASERANGE(_,_,_,loc) -> loc
  95   | DEFAULT(_,loc) -> loc
  96   | LABEL(_,_,loc) -> loc
  97   | GOTO(_,loc) -> loc
  98   | COMPGOTO (_, loc) -> loc
  99   | DEFINITION d -> get_definitionloc d
 100   | ASM(_,_,_,loc) -> loc
 101   | TRY_EXCEPT(_, _, _, loc) -> loc
 102   | TRY_FINALLY(_, _, loc) -> loc
 103 end
 104
 105
 106 let explodeStringToInts (s: string) : int64 list =
 107   let rec allChars i acc =
 108     if i < 0 then acc
 109     else allChars (i - 1) (Int64.of_int (Char.code (String.get s i)) :: acc)
 110   in
 111   allChars (-1 + String.length s) []
 112
 113 let valueOfDigit chr =
 114   let int_value =
 115     match chr with
 116       '0'..'9' -> (Char.code chr) - (Char.code '0')
 117     | 'a'..'z' -> (Char.code chr) - (Char.code 'a') + 10
 118     | 'A'..'Z' -> (Char.code chr) - (Char.code 'A') + 10
 119     | _ -> assert false in
 120   Int64.of_int int_value
 121
 122 let string_of_cabsloc l =
 123   Printf.sprintf "%s:%d" l.filename l.lineno
 124
 125 let format_cabsloc pp l =
 126   Format.fprintf pp "%s:%d" l.filename l.lineno