CHC: update for new Goblint-Cil int/float variants

Author: sipma

CodeHawk/CHC/cchlib/cCHBasicTypes.mli

@@ -49,12 +49,19 @@ type ikind =
 | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
 | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft
                   Visual C) *)
+| IInt128     (** added by Goblint-Cil *)
+| IUInt128    (** added by Goblint-Cil *)
+
 
 (** Various kinds of floating-point numbers*)
 type fkind =
 | FFloat      (** [float] *)
 | FDouble     (** [double] *)
 | FLongDouble (** [long double] *)
+| FComplexFloat
+| FComplexDouble
+| FComplexLongDouble
+
 
 type storage =
 | NoStorage
@@ -260,7 +267,14 @@ and asm_input_t = string option * string * exp (* name, constraint, exp *)
 and instr =
 | Set of lval * exp * location
 | Call of lval option * exp * exp list * location
-| Asm of attributes * int list * asm_output_t list * asm_input_t list * int list * location
+| VarDecl of varinfo * location
+| Asm of
+    attributes
+    * int list
+    * asm_output_t list
+    * asm_input_t list
+    * int list
+    * location
 
 and location = {
   line : int ;

CodeHawk/CHC/cchlib/cCHBasicTypesXml.ml

@@ -32,6 +32,7 @@ open CHLanguage
 open CHPretty
 
 (* chutil *)
+open CHLogger
 open CHPrettyUtil
 open CHXmlDocument
 
@@ -241,28 +242,34 @@ let read_xml_asm_input_list (node:xml_element_int) : asm_input_t list =
   List.map read_xml_asm_input (node#getTaggedChildren "asminput")
 
 
-let read_xml_instruction (node:xml_element_int) : instr =
+let read_xml_instruction (node:xml_element_int) : instr option =
   let hasc = node#hasOneTaggedChild in
   let get = node#getAttribute in
   let getc = node#getTaggedChild in
   let read_list tag reader = if hasc tag then reader (getc tag) else [] in
   match get "itag" with
   | "set" ->
-     Set (cd#read_xml_lval node,
-          cd#read_xml_exp node,
-          cdecls#read_xml_location node)
+     Some (
+         Set (cd#read_xml_lval node,
+              cd#read_xml_exp node,
+              cdecls#read_xml_location node))
   | "call" ->
-     Call (cd#read_xml_lval_opt node,
-           cd#read_xml_exp node,
-	   read_xml_exp_list (getc "args"),
-           cdecls#read_xml_location node)
+     Some (
+         Call (cd#read_xml_lval_opt node,
+               cd#read_xml_exp node,
+	       read_xml_exp_list (getc "args"),
+               cdecls#read_xml_location node))
   | "asm" ->
-     Asm (cd#read_xml_attributes node,
-	  read_list "templates" read_xml_string_index_list,
-	  read_list "asmoutputs" read_xml_asm_output_list,
-	  read_list "asminputs" read_xml_asm_input_list,
-	  read_list "registerclobbers" read_xml_string_index_list,
-	  cdecls#read_xml_location node)
+     Some (
+         Asm (cd#read_xml_attributes node,
+	      read_list "templates" read_xml_string_index_list,
+	      read_list "asmoutputs" read_xml_asm_output_list,
+	      read_list "asminputs" read_xml_asm_input_list,
+	      read_list "registerclobbers" read_xml_string_index_list,
+	      cdecls#read_xml_location node))
+
+  | "vardecl" -> None
+
   | s -> raise (Invalid_enumeration ("instruction", s))
 
 
@@ -286,7 +293,16 @@ let read_xml_label_list (node:xml_element_int) : label list =
 
 
 let read_xml_instruction_list (node:xml_element_int) : instr list =
-  List.map read_xml_instruction (node#getTaggedChildren "instr")
+  let revinstrs =
+    List.fold_left
+      (fun acc n ->
+        match read_xml_instruction n with
+        | Some instr -> instr :: acc
+        | _ ->
+           let _ =
+             chlog#add "ignoring vardecl instruction" (STR "No vardecl") in
+           acc) [] (node#getTaggedChildren "instr") in
+  List.rev revinstrs
 
 
 let rec read_xml_function_block (node:xml_element_int) : block =

CodeHawk/CHC/cchlib/cCHBasicTypesXml.mli

@@ -67,6 +67,6 @@ val read_xml_exp_option_list: ?tag:string -> xml_element_int -> exp option list
 
 val read_xml_cfile: xml_element_int -> file
 
-val read_xml_instruction: xml_element_int -> instr
+val read_xml_instruction: xml_element_int -> instr option
 
 val read_xml_function_definition: xml_element_int -> fundec

CodeHawk/CHC/cchlib/cCHCodewalker.ml

@@ -105,7 +105,8 @@ object (self:_)
 	List.iter (fun e -> self#walk_exp e) l;
 	self#walk_location loc
       end
-    | Asm (_,_,_,_,_,loc) -> self#walk_location loc
+    | Asm (_, _, _, _, _, loc) -> self#walk_location loc
+    | VarDecl (_, loc) -> self#walk_location loc
 
   method walk_lval (l:lval) =
     begin

CodeHawk/CHC/cchlib/cCHLibTypes.mli

@@ -54,12 +54,18 @@ type machine_sizes_t = {
   sizeof_long  : xpr_t;
 
   sizeof_longlong : xpr_t;
+  sizeof_int128   : xpr_t;
+
   sizeof_ptr      : xpr_t;
   sizeof_enum     : xpr_t;
   sizeof_float    : xpr_t;
   sizeof_double   : xpr_t;
 
   sizeof_longdouble  : xpr_t;
+  sizeof_complex_float: xpr_t;
+  sizeof_complex_double: xpr_t;
+  sizeof_complex_longdouble: xpr_t;
+
   sizeof_void        : xpr_t;
   sizeof_fun         : xpr_t;
 
@@ -69,12 +75,18 @@ type machine_sizes_t = {
   alignof_long   : xpr_t;
 
   alignof_longlong  : xpr_t;
+  alignof_int128    : xpr_t;
+
   alignof_ptr       : xpr_t;
   alignof_enum      : xpr_t;
   alignof_float     : xpr_t;
 
   alignof_double    : xpr_t;
   alignof_longdouble: xpr_t;
+  alignof_complex_float: xpr_t;
+  alignof_complex_double: xpr_t;
+  alignof_complex_longdouble: xpr_t;
+
   alignof_str       : xpr_t;
   alignof_fun       : xpr_t;
   alignof_aligned   : xpr_t;

CodeHawk/CHC/cchlib/cCHMachineSizes.ml

@@ -108,13 +108,15 @@ let ic2 = int_constant_expr 2
 let ic4 = int_constant_expr 4
 let ic8 = int_constant_expr 8
 let ic16 = int_constant_expr 16
+let ic32 = int_constant_expr 32
 
 
 let symbolic_sizes = {
   sizeof_short  = mkvar "sizeof_short";
   sizeof_int    = mkvar "sizeof_int";
   sizeof_bool   = mkvar "sizeof_bool";
   sizeof_long   = mkvar "sizeof_long";
+  sizeof_int128 = mkvar "sizeof_int128";
 
   sizeof_longlong = mkvar "sizeof_longlong";
   sizeof_ptr      = mkvar "sizeof_ptr";
@@ -123,13 +125,18 @@ let symbolic_sizes = {
   sizeof_double   = mkvar "sizeof_double";
 
   sizeof_longdouble = mkvar "sizeof_longdouble";
+  sizeof_complex_float = mkvar "sizeof_complex_float";
+  sizeof_complex_double = mkvar "sizeof_complex_double";
+  sizeof_complex_longdouble = mkvar "sizeof_complex_longdouble";
+
   sizeof_void       = mkvar "sizeof_void";
   sizeof_fun        = mkvar "sizeof_fun";
 
   alignof_short     = mkvar "alignof_short";
   alignof_int       = mkvar "alignof_int";
   alignof_bool      = mkvar "alignof_bool";
   alignof_long      = mkvar "alignof_long";
+  alignof_int128    = mkvar "alignof_int128";
 
   alignof_longlong  = mkvar "alignof_longlong";
   alignof_ptr       = mkvar "alignof_ptr";
@@ -138,74 +145,96 @@ let symbolic_sizes = {
 
   alignof_double     = mkvar "alignof_double";
   alignof_longdouble = mkvar "alignof_longdouble";
+  alignof_complex_float = mkvar "alignof_complex_float";
+  alignof_complex_double = mkvar "alignof_complex_double";
+  alignof_complex_longdouble = mkvar "alignof_complex_longdouble";
+
   alignof_str        = mkvar "alignof_str";
   alignof_fun        = mkvar "alignof_fun";
   alignof_aligned    = mkvar "alignof_aligned"
   }
 
 
-let linux_64_machine_sizes = {           (* sizes in bytes for linux server, from cil output *)
+(* sizes in bytes for linux server, from cil output *)
+let linux_64_machine_sizes = {
     sizeof_short  = ic2;
     sizeof_int    = ic4;
     sizeof_bool   = ic1;
     sizeof_long   = ic8;
+    sizeof_int128 = ic16;
 
     sizeof_longlong = ic8;
     sizeof_ptr      = ic8;
     sizeof_enum     = ic4;
     sizeof_float    = ic4;
     sizeof_double   = ic8;
-
     sizeof_longdouble = ic16;
+    sizeof_complex_float = ic8;
+    sizeof_complex_double = ic16;
+    sizeof_complex_longdouble = ic32;
+
     sizeof_void       = ic1;
     sizeof_fun        = ic1;
 
     alignof_short  = ic2;
     alignof_int    = ic4;
     alignof_bool   = ic1;
     alignof_long   = ic8;
+    alignof_int128 = ic16;
 
     alignof_longlong = ic8;
     alignof_ptr      = ic8;
     alignof_enum     = ic4;
     alignof_float    = ic4;
-
     alignof_double     = ic8;
     alignof_longdouble = ic16;
+    alignof_complex_float = ic8;
+    alignof_complex_double = ic16;
+    alignof_complex_longdouble = ic32;
+
     alignof_str        = ic1;
     alignof_fun        = ic1;
     alignof_aligned    = ic16
   }
 
 
-let linux_32_machine_sizes = { (* sizes in bytes for linux 32 bits, derived from 64 bits *)
+(* sizes in bytes for linux 32 bits, derived from 64 bits *)
+let linux_32_machine_sizes = {
     sizeof_short  = ic2;
     sizeof_int    = ic4;
     sizeof_bool   = ic1;
     sizeof_long   = ic4;
+    sizeof_int128 = ic16;
 
     sizeof_longlong = ic8;
     sizeof_ptr      = ic4;
     sizeof_enum     = ic4;
     sizeof_float    = ic4;
     sizeof_double   = ic8;
-
     sizeof_longdouble = ic8;
+    sizeof_complex_float = ic8;
+    sizeof_complex_double = ic16;
+    sizeof_complex_longdouble = ic16;
+
     sizeof_void       = ic1;
     sizeof_fun        = ic1;
 
     alignof_short  = ic2;
     alignof_int    = ic4;
     alignof_bool   = ic1;
     alignof_long   = ic4;
+    alignof_int128 = ic16;
 
     alignof_longlong = ic8;
     alignof_ptr      = ic4;
     alignof_enum     = ic4;
     alignof_float    = ic4;
-
     alignof_double     = ic8;
     alignof_longdouble = ic8;
+    alignof_complex_float = ic8;
+    alignof_complex_double = ic16;
+    alignof_complex_longdouble = ic16;
+
     alignof_str        = ic1;
     alignof_fun        = ic1;
     alignof_aligned    = ic8
@@ -217,29 +246,37 @@ let linux_16_machine_sizes = {
     sizeof_int    = ic2;
     sizeof_bool   = ic1;
     sizeof_long   = ic4;
+    sizeof_int128 = ic16;
 
     sizeof_longlong = ic4;
     sizeof_ptr      = ic2;
     sizeof_enum     = ic2;
     sizeof_float    = ic2;
     sizeof_double   = ic4;
-
     sizeof_longdouble = ic4;
+    sizeof_complex_float = ic4;
+    sizeof_complex_double = ic8;
+    sizeof_complex_longdouble = ic8;
+
     sizeof_void       = ic1;
     sizeof_fun        = ic1;
 
     alignof_short  = ic2;
     alignof_int    = ic2;
     alignof_bool   = ic1;
     alignof_long   = ic4;
+    alignof_int128 = ic16;
 
     alignof_longlong = ic4;
     alignof_ptr      = ic2;
     alignof_enum     = ic2;
     alignof_float    = ic2;
-
     alignof_double     = ic4;
     alignof_longdouble = ic4;
+    alignof_complex_float = ic4;
+    alignof_complex_double = ic8;
+    alignof_complex_longdouble = ic8;
+
     alignof_str        = ic1;
     alignof_fun        = ic1;
     alignof_aligned    = ic4

CodeHawk/CHC/cchlib/cCHSumTypeSerializer.ml

@@ -56,13 +56,21 @@ let ikind_mfts: ikind mfts_int =
      (ILong, "ilong");
      (IULong, "iulong");
      (ILongLong, "ilonglong");
-     (IULongLong, "iulonglong")]
+     (IULongLong, "iulonglong");
+     (IInt128, "int128_t");
+     (IUInt128, "uint128_t")
+    ]
 
 
 let fkind_mfts: fkind mfts_int =
   mk_mfts
     "fkind"
-    [(FFloat, "float"); (FDouble, "fdouble"); (FLongDouble, "flongdouble")]
+    [(FFloat, "float");
+     (FDouble, "fdouble");
+     (FLongDouble, "flongdouble");
+     (FComplexFloat, "fcomplexfloat");
+     (FComplexDouble, "fcomplexdouble");
+     (FComplexLongDouble, "fcomplexlongdouble")]
 
 
 let unop_mfts: unop mfts_int =
@@ -324,8 +332,9 @@ object
     | Set _ -> "set"
     | Call _ -> "call"
     | Asm _ -> "asm"
+    | VarDecl _ -> "vardecl"
 
-  method! tags = ["asm"; "call"; "set"]
+  method! tags = ["asm"; "call"; "set"; "vardecl"]
 
 end