Add parsing support for 'asm goto'

src/cil.ml

@@ -858,6 +858,7 @@ and instr =
                   (string option * string * exp) list *
                                         (* inputs with optional names and constraints *)
                   string list *         (* register clobbers *)
+                  string list *         (* GoToLabels *)
                   location
         (** An inline assembly instruction. The arguments are (1) a list of
             attributes (only const and volatile can appear here and only for
@@ -1125,7 +1126,7 @@ let get_instrLoc (inst : instr) =
   match inst with
       Set(_, _, loc, _) -> loc
     | Call(_, _, _, loc, _) -> loc
-    | Asm(_, _, _, _, _, loc) -> loc
+    | Asm(_, _, _, _, _, _, loc) -> loc
     | VarDecl(_,loc) -> loc
 let get_globalLoc (g : global) =
   match g with
@@ -1353,7 +1354,7 @@ let mkBlock (slst: stmt list) : block =
 let mkEmptyStmt () = mkStmt (Instr [])
 let mkStmtOneInstr (i: instr) = mkStmt (Instr [i])
 
-let dummyInstr = (Asm([], ["dummy statement!!"], [], [], [], lu))
+let dummyInstr = (Asm([], ["dummy statement!!"], [], [], [], [], lu))
 let dummyStmt =  mkStmt (Instr [dummyInstr])
 
 let compactStmts (b: stmt list) : stmt list =
@@ -2978,6 +2979,7 @@ let initGccBuiltins () : unit =
   H.add h "__builtin_inff" (floatType, [], false);
   H.add h "__builtin_infl" (longDoubleType, [], false);
   H.add h "__builtin_memcpy" (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
+  H.add h "__builtin_memchr" (voidPtrType, [voidConstPtrType; intType; ulongType], false);
   H.add h "__builtin_mempcpy" (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
   H.add h "__builtin_memset" (voidPtrType,
                               [ voidPtrType; intType; intType ], false);
@@ -3052,6 +3054,7 @@ let initGccBuiltins () : unit =
   H.add h "__builtin_sqrtl" (longDoubleType, [ longDoubleType ], false);
 
   H.add h "__builtin_stpcpy" (charPtrType, [ charPtrType; charConstPtrType ], false);
+  H.add h "__builtin_strcat" (charPtrType, [charPtrType; charConstPtrType], false);
   H.add h "__builtin_strchr" (charPtrType, [ charPtrType; intType ], false);
   H.add h "__builtin_strcmp" (intType, [ charConstPtrType; charConstPtrType ], false);
   H.add h "__builtin_strcpy" (charPtrType, [ charPtrType; charConstPtrType ], false);
@@ -3706,7 +3709,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
              ++ unalign)
         ++ text (")" ^ printInstrTerminator)
 
-    | Asm(attrs, tmpls, outs, ins, clobs, l) ->
+    | Asm(attrs, tmpls, outs, ins, clobs, gotos, l) ->
         self#pLineDirective l
           ++ text ("__asm__ ")
           ++ self#pAttrs () attrs
@@ -3751,6 +3754,11 @@ class defaultCilPrinterClass : cilPrinter = object (self)
                             (fun c -> text ("\"" ^ escape_string c ^ "\""))
                             ()
                             clobs)))
+                ++
+                (if gotos = [] then nil
+                else (
+                  text ": " ++ (docList ~sep:(chr ',' ++ break) (fun c -> text (escape_string c)) () gotos)
+                ))
                 ++ unalign)
           ++ text (")" ^ printInstrTerminator)
 
@@ -5323,15 +5331,15 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
       if lv' != lv || fn' != fn || args' != args
       then Call(Some lv', fn', args', l, el) else i
 
-  | Asm(sl,isvol,outs,ins,clobs,l) ->
+  | Asm(sl,isvol,outs,ins,clobs,gotos,l) ->
       let outs' = mapNoCopy (fun ((id,s,lv) as pair) ->
                                let lv' = fLval lv in
                                if lv' != lv then (id,s,lv') else pair) outs in
       let ins'  = mapNoCopy (fun ((id,s,e) as pair) ->
                                let e' = fExp e in
                                if e' != e then (id,s,e') else pair) ins in
       if outs' != outs || ins' != ins then
-        Asm(sl,isvol,outs',ins',clobs,l) else i
+        Asm(sl,isvol,outs',ins',clobs,gotos,l) else i
 
 
 (* visit all nodes in a Cil statement tree in preorder *)
@@ -6004,7 +6012,7 @@ let dExp: doc -> exp =
   fun d -> Const(CStr(sprint ~width:!lineLength d, No_encoding))
 
 let dInstr: doc -> location -> instr =
-  fun d l -> Asm([], [sprint ~width:!lineLength d], [], [], [], l)
+  fun d l -> Asm([], [sprint ~width:!lineLength d], [], [], [], [], l)
 
 let dGlobal: doc -> location -> global =
   fun d l -> GAsm(sprint ~width:!lineLength d, l)

src/cil.mli

@@ -1049,6 +1049,7 @@ and instr =
                   (string option * string * exp) list *
                                         (* inputs with optional names and constraints *)
                   string list *         (* register clobbers *)
+                  string list *         (* GoToLabels *)
                   location
     (** There are for storing inline assembly. They follow the GCC
         specification:

src/ext/liveness/usedef.ml

@@ -150,7 +150,7 @@ class useDefVisitorClass : cilVisitor = object (self)
         E.s (bug "bad call to %s" vi.vname)
     | Call (lvo, f, args, _, _) ->
         doCall f lvo args
-    | Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) ->
+    | Asm(_,_,slvl,_,_,_,_) -> List.iter (fun (_,s,lv) ->
 	match lv with (Var v, off) ->
 	  if s.[0] = '+' then
 	    varUsed := VS.add v !varUsed;

src/ext/zrapp/availexps.ml

@@ -243,7 +243,7 @@ let eh_handle_inst i eh =
       (eh_kill_mem eh;
        eh_kill_addrof_or_global eh;
        eh)
-  | Asm(_,_,_,_,_,_) ->
+  | Asm(_,_,_,_,_,_,_) ->
       let _,d = UD.computeUseDefInstr i in
       (UD.VS.iter (fun vi ->
 	eh_kill_vi eh vi) d;

src/ext/zrapp/availexpslv.ml

@@ -305,7 +305,7 @@ let lvh_handle_inst i lvh =
       end;
       lvh
   end
-  | Asm(_,_,_,_,_,_) -> begin
+  | Asm(_,_,_,_,_,_,_) -> begin
       let _,d = UD.computeUseDefInstr i in
       UD.VS.iter (fun vi ->
 	lvh_kill_vi lvh vi) d;

src/ext/zrapp/deadcodeelim.ml

@@ -102,7 +102,7 @@ class usedDefsCollectorClass = object(self)
 
   method! vinst i =
     let handle_inst iosh i = match i with
-    | Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) ->
+    | Asm(_,_,slvl,_,_,_,_) -> List.iter (fun (_,s,lv) ->
 	match lv with (Var v, off) ->
 	  if s.[0] = '+' then
 	    self#add_defids iosh (Lval(Var v, off)) (UD.VS.singleton v)

src/ext/zrapp/reachingdefs.ml

@@ -270,7 +270,7 @@ let getDefRhs didstmh stmdat defId =
 		Set((Var vi',NoOffset),_,_,_) -> vi'.vid = vid (* _ -> NoOffset *)
 	      | Call(Some(Var vi',NoOffset),_,_,_,_) -> vi'.vid = vid (* _ -> NoOffset *)
 	      | Call(None,_,_,_,_) -> false
-	      | Asm(_,_,sll,_,_,_) -> List.exists
+	      | Asm(_,_,sll,_,_,_,_) -> List.exists
 		    (function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll
 	      | _ -> false)
 	  | None -> false) iihl in
@@ -284,7 +284,7 @@ let getDefRhs didstmh stmdat defId =
 	| Call(lvo,e,el,_,_) ->
 	    (IH.add rhsHtbl defId (Some(RDCall(i),stm.sid,iosh_in));
 	     Some(RDCall(i), stm.sid, iosh_in))
-	| Asm(a,sl,slvl,sel,sl',_) -> None
+	| Asm(a,sl,slvl,sel,sl',_,_) -> None
   | VarDecl _ -> None
   ) (* ? *)
 	with Not_found ->

src/ext/zrapp/rmciltmps.ml

@@ -994,7 +994,7 @@ class unusedRemoverClass : cilVisitor = object(self)
 	  (match IH.find iioh vi.vid with
 	    None -> true | Some _ -> false)
       end
-      | Asm(_,_,slvlst,_,_,_) -> begin
+      | Asm(_,_,slvlst,_,_,_,_) -> begin
 	  (* make sure the outputs are in the locals list *)
 	  List.iter (fun (_,s,lv) ->
 	    match lv with (Var vi,_) ->

src/frontc/cabs.ml

@@ -209,7 +209,8 @@ and block =
 and asm_details =
     { aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *)
       ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *)
-      aclobbers: string list (* clobbered registers *)
+      aclobbers: string list; (* clobbered registers *)
+      agotolabels: string list; (* GoToLabels *)
     }
 
 and statement =

src/frontc/cabs2cil.ml

@@ -822,7 +822,7 @@ module BlockChunk =
         | Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc)
         | VarDecl (v, loc) -> VarDecl (v, doLoc loc)
         | Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc)
-        | Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, doLoc loc)
+        | Asm (a, b, c, d, e, f, loc) -> Asm (a, b, c, d, e, f, doLoc loc)
 
       (** Change all stmt and instr locs to synthetic, except the first one.
           Expressions/initializers that expand to multiple instructions cannot have intermediate locations referenced. *)
@@ -6893,16 +6893,16 @@ and doStatement (s : A.statement) : chunk =
         currentLoc := loc';
         currentExpLoc := loc'; (* for argument doExp below *)
         let stmts : chunk ref = ref empty in
-	let (tmpls', outs', ins', clobs') =
+	let (tmpls', outs', ins', clobs', gotos') =
 	  match details with
 	  | None ->
 	      let tmpls' =
 		      let pattern = Str.regexp "%" in
 		      let escape = Str.global_replace pattern "%%" in
 		      Util.list_map escape tmpls
 	      in
-	      (tmpls', [], [], [])
-	  | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } ->
+	      (tmpls', [], [], [], [])
+	  | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotolabels = gotos } ->
               let outs' =
 		Util.list_map
 		  (fun (id, c, e) ->
@@ -6925,10 +6925,10 @@ and doStatement (s : A.statement) : chunk =
 		    (id, c, e'))
 		  ins
               in
-	      (tmpls, outs', ins', clobs)
+	      (tmpls, outs', ins', clobs, gotos)
 	in
         !stmts @@
-        (i2c (Asm(attr', tmpls', outs', ins', clobs', loc')))
+        (i2c (Asm(attr', tmpls', outs', ins', clobs', gotos', loc')))
 
   with e when continueOnError -> begin
     (ignore (E.log "Error in doStatement (%s)\n" (Printexc.to_string e)));

src/frontc/cabsvisit.ml

@@ -434,13 +434,13 @@ and childrenStatement vis s =
       in
       let details' = match details with
       | None -> details
-      | Some { aoutputs = outl; ainputs = inl; aclobbers = clobs } ->
+      | Some { aoutputs = outl; ainputs = inl; aclobbers = clobs; agotolabels = gotos } ->
 	  let outl' = mapNoCopy childrenIdentStringExp outl in
 	  let inl' = mapNoCopy childrenIdentStringExp inl in
 	  if outl' == outl && inl' == inl then
 	    details
 	  else
-	    Some { aoutputs = outl'; ainputs = inl'; aclobbers = clobs }
+	    Some { aoutputs = outl'; ainputs = inl'; aclobbers = clobs; agotolabels = gotos }
       in
       if details' != details then
         ASM (sl, b, details', l) else s

src/frontc/cparser.mly

@@ -981,6 +981,9 @@ statement_no_null:
 		                 {GOTO (fst $2, joinLoc $1 $3)}
 |   GOTO STAR comma_expression SEMICOLON
                                  { COMPGOTO (smooth_expression (fst $3), joinLoc $1 $4) }
+|   ASM asmattr GOTO asmattr LPAREN asmtemplate COLON asmoperands COLON asmoperands COLON asmclobberlst COLON asmgotolabelslst RPAREN SEMICOLON
+                        { ASM (("goto",[])::("volatile",[])::($2 @ $4), $6, Some {aoutputs = $8; ainputs = $10; aclobbers = $12; agotolabels = $14 }, joinLoc $1 $16) }
+                         /* 'asm goto' is implicitly considered 'volatile' according to: https://gcc.gnu.org/onlinedocs/gcc/Extended-Asm.html#GotoLabels */
 |   ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON
                         { ASM ($2, $4, $5, joinLoc $1 $7) }
 |   error location   SEMICOLON   { (NOP $2)}
@@ -1645,6 +1648,7 @@ asmattr:
      /* empty */                        { [] }
 |    VOLATILE  asmattr                  { ("volatile", []) :: $2 }
 |    CONST asmattr                      { ("const", []) :: $2 }
+|    INLINE asmattr                     { ("inline", []) :: $2 }
 ;
 asmtemplate:
     one_string_constant                          { [$1] }
@@ -1654,7 +1658,7 @@ asmoutputs:
   /* empty */           { None }
 | COLON asmoperands asminputs
                         { let (ins, clobs) = $3 in
-                          Some {aoutputs = $2; ainputs = ins; aclobbers = clobs} }
+                          Some {aoutputs = $2; ainputs = ins; aclobbers = clobs; agotolabels = []} }
 ;
 asmoperands:
      /* empty */                        { [] }
@@ -1682,15 +1686,20 @@ asmopname:
 
 asmclobber:
     /* empty */                         { [] }
-| COLON asmcloberlst                    { $2 }
+| COLON asmclobberlst                   { $2 }
 ;
-asmcloberlst:
+asmclobberlst:
     /* empty */                         { [] }
-| asmcloberlst_ne                       { $1 }
+| asmclobberlst_ne                       { $1 }
 ;
-asmcloberlst_ne:
+asmclobberlst_ne:
    one_string_constant                           { [$1] }
-|  one_string_constant COMMA asmcloberlst_ne     { $1 :: $3 }
+|  one_string_constant COMMA asmclobberlst_ne    { $1 :: $3 }
+;
+
+asmgotolabelslst:
+  IDENT                         { [fst $1] }
+| IDENT COMMA asmgotolabelslst  { (fst $1) :: $3 }
 ;
 
 %%

src/frontc/frontc.ml

@@ -106,6 +106,8 @@ let args : (string * Arg.spec * string) list =
 exception ParseError of string
 exception CabsOnly
 
+let resetErrors () = E.hadErrors := false
+
 (* parse, and apply patching *)
 let rec parse_to_cabs fname =
 begin

src/frontc/frontc.mli

@@ -47,6 +47,8 @@ val args: (string * Arg.spec * string) list
 
     (* the main command to parse a file. Return a thunk that can be used to 
        convert the AST to CIL. *)
+val resetErrors: unit -> unit
+
 val parse: string -> (unit -> Cil.file)
 
 val parse_with_cabs: string -> (unit -> Cabs.file * Cil.file)