Possibility to control if VarDecl should be generated for all variables or not

via alwaysGenerateVarDecl in cabs2cil.ml
and cleanup of print code

Author: michael-schwarz

src/cil.ml

@@ -3238,12 +3238,6 @@ class type cilPrinter = object
      * in formals of function types, and the formals and locals for function
      * definitions. *)
 
-  method pVDeclPhony: unit -> varinfo -> bool -> doc
-    (** Invoked for each variable declaration. Note that variable
-     * declarations are all the [GVar], [GVarDecl], [GFun], all the [varinfo]
-     * in formals of function types, and the formals and locals for function
-     * definitions. *)
-
   method pVar: varinfo -> doc
     (** Invoked on each variable use. *)
 
@@ -3346,32 +3340,14 @@ class defaultCilPrinterClass : cilPrinter = object (self)
 
   (* variable declaration *)
   method pVDecl () (v:varinfo) =
-    if not v.vhasdeclinstruction then
-      let stom, rest = separateStorageModifiers v.vattr in
-      (* First the storage modifiers *)
-      text (if v.vinline then "__inline " else "")
-        ++ d_storage () v.vstorage
-        ++ (self#pAttrs () stom)
-        ++ (self#pType (Some (text v.vname)) () v.vtype)
-        ++ text " "
-        ++ self#pAttrs () rest
-    else
-      text " "
-
-
-  (* variable declaration *)
-  method pVDeclPhony () (v:varinfo) ph =
-    if ph || not v.vhasdeclinstruction then
-      let stom, rest = separateStorageModifiers v.vattr in
-      (* First the storage modifiers *)
-      text (if v.vinline then "__inline " else "")
-        ++ d_storage () v.vstorage
-        ++ (self#pAttrs () stom)
-        ++ (self#pType (Some (text v.vname)) () v.vtype)
-        ++ text " "
-        ++ self#pAttrs () rest
-    else
-      text " "
+    let stom, rest = separateStorageModifiers v.vattr in
+    (* First the storage modifiers *)
+    text (if v.vinline then "__inline " else "")
+      ++ d_storage () v.vstorage
+      ++ (self#pAttrs () stom)
+      ++ (self#pType (Some (text v.vname)) () v.vtype)
+      ++ text " "
+      ++ self#pAttrs () rest
 
   (*** L-VALUES ***)
   method pLval () (lv:lval) =  (* lval (base is 1st field)  *)
@@ -3626,10 +3602,13 @@ class defaultCilPrinterClass : cilPrinter = object (self)
               ++ text printInstrTerminator
 
     end
-    | VarDecl(varinfo,l) ->
-      self#pLineDirective l
-      ++ self#pVDeclPhony () varinfo true
-      ++ chr ';'
+    | VarDecl(v, l) ->
+        self#pLineDirective l
+        ++ self#pVDecl () v
+        ++ (match v.vinit.init with
+            | None -> text ";"
+            | Some i -> text " = " ++
+                self#pInit () i ++ text ";")
       (* In cabs2cil we have turned the call to builtin_va_arg into a
        * three-argument call: the last argument is the address of the
        * destination *)
@@ -3813,15 +3792,21 @@ class defaultCilPrinterClass : cilPrinter = object (self)
 
   method private pStmtNext (next: stmt) () (s: stmt) =
     (* print the labels *)
-    ((docList ~sep:line (fun l -> self#pLabel () l)) () s.labels)
-      (* print the statement itself. If the labels are non-empty and the
-      * statement is empty, print a semicolon  *)
-      ++
-      (if s.skind = Instr [] && s.labels <> [] then
-        text ";"
-      else
-        (if s.labels <> [] then line else nil)
-          ++ self#pStmtKind next () s.skind)
+    let labels = ((docList ~sep:line (fun l -> self#pLabel () l)) () s.labels) in
+    if s.skind = Instr [] && s.labels <> [] then
+      (* If the labels are non-empty and the statement is empty, print a semicolon  *)
+      labels ++ text ";"
+    else
+      let pre =
+        if s.labels <> [] then
+          (match s.skind with
+          | Instr (VarDecl(_)::_)-> text ";" (* first instruction is VarDecl, insert semicolon *)
+          | _ -> nil)
+          ++ line
+        else
+          nil (* no labels, no new line needed *)
+      in
+      labels ++ pre ++ self#pStmtKind next () s.skind
 
   method private pLabel () = function
       Label (s, _, true) -> text (s ^ ": ")
@@ -4248,7 +4233,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
                 | None -> self#pVDecl () vi ++ text ";"
                 | Some i -> self#pVDecl () vi ++ text " = " ++
                     self#pInit () i ++ text ";")
-                () f.slocals)
+                () (List.filter (fun v -> not v.vhasdeclinstruction) f.slocals))
             ++ line ++ line
             (* the body *)
             ++ ((* remember the declaration *) currentFormals <- f.sformals;

src/cil.mli

@@ -2163,8 +2163,6 @@ class type cilPrinter = object
      * in formals of function types, and the formals and locals for function
      * definitions. *)
 
-  method pVDeclPhony: unit -> varinfo -> bool -> Pretty.doc
-
   method pVar: varinfo -> Pretty.doc
     (** Invoked on each variable use. *)
 

src/frontc/cabs2cil.ml

@@ -67,6 +67,15 @@ let forceRLArgEval = ref false
 (** Leave a certain global alone. Use a negative number to disable. *)
 let nocil: int ref = ref (-1)
 
+(** Set to true to generate VarDecl "instructions" for all local variables
+  * In some circumstances, it is unavoidable to generate VarDecls (namely
+  * for variable length arrays (VLAs)). In these cases, we generate a VarDecl
+  * even if alwaysGenerateVarDecl is false.
+  * Under certain conditions (involving GNU computed gotos), it is not possible
+  * to generate VarDecls for all locals, in these cases we do not generate them
+  * *)
+let alwaysGenerateVarDecl = true
+
 (** Indicates whether we're allowed to duplicate small chunks. *)
 let allowDuplication: bool ref = ref true
 
@@ -2662,7 +2671,6 @@ and makeVarSizeVarInfo (ldecl : location)
                         ldecl spec_res (n,ndt,a), empty, false
     | Some (ndt', se, len) ->
         let vi = makeVarInfoCabs ~isformal:false ~isglobal:false ldecl spec_res (n,ndt',a) in
-        vi.vhasdeclinstruction <- true;
         vi.vtype <- insertArrayLengths vi.vtype len; (* patch the correct length for the array back-in *)
         vi, se, true
   else
@@ -5467,7 +5475,7 @@ and createGlobal (specs : (typ * storage * bool * A.attribute list))
 *)
 
 (* Must catch the Static local variables. Make them global *)
-and createLocal ((_, sto, _, _) as specs)
+and createLocal ?allow_var_decl:(allow_var_decl=true) ((_, sto, _, _) as specs)
                 ((((n, ndt, a, cloc) : A.name),
                   (inite: A.init_expression)) as init_name)
   : chunk =
@@ -5554,15 +5562,23 @@ and createLocal ((_, sto, _, _) as specs)
       let vi,se0,isvarsize =
         makeVarSizeVarInfo loc specs (n, ndt, a) in
       let vi = alphaConvertVarAndAddToEnv true vi in        (* Replace vi *)
-      let se1 =
-        if isvarsize then begin (* Variable-sized array *)
-          ignore (warn "Variable-sized local variable %s" vi.vname);
-          if inite != A.NO_INIT then
-            E.s (error "Variable-sized array cannot have initializer");
-          se0 +++ VarDecl(vi, !currentLoc)
-        end else
-        empty
+      let sevarsize = (* Chunk that is needed to pull out things for variable-length arrays *)
+        if isvarsize then
+          begin
+            ignore (warn "Variable-sized local variable %s" vi.vname);
+            if inite != A.NO_INIT then
+              E.s (error "Variable-sized array cannot have initializer")
+            else if not allow_var_decl then
+              E.s (error "VLAs in conjunction with computed gotos are unsupported.")
+            else
+              se0
+          end
+        else
+          empty
       in
+      let makevdecl = (isvarsize || alwaysGenerateVarDecl && allow_var_decl) in
+      let se1 = if makevdecl then sevarsize +++ VarDecl(vi, !currentLoc) else sevarsize in
+      vi.vhasdeclinstruction <- makevdecl;
       if inite = A.NO_INIT then
         se1 (* skipChunk *)
       else begin
@@ -6518,8 +6534,9 @@ and doStatement (s : A.statement) : chunk =
             @@ s2c(mkStmt(Goto (ref switch, loc')))
 
         | None -> begin
-            (* Make a temporary variable *)
-            let vchunk = createLocal
+            (* Make a temporary variable, avoiding generation of VarDecl if possible *)
+            (* as this is unsupported (see below)                                    *)
+            let vchunk = createLocal ~allow_var_decl:false
                 (!upointType, NoStorage, false, [])
                 (("__compgoto", A.JUSTBASE, [], loc), A.NO_INIT)
             in