Support for parsing extended assembly code including asm goto

src/cfg.ml

@@ -225,6 +225,7 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
       cfgBlock blk (Some s) next (Some s) nodeList rlabels
       (* Since all loops have terminating condition true, we don't put
          any direct successor to stmt following the loop *)
+  | Asm (_, _, _, _, _, labels, _) -> addOptionSucc next (* the extra edges are added inside goblint's cfg *)
 
 (*------------------------------------------------------------*)
 
@@ -247,7 +248,7 @@ and fasStmt (todo) (s : stmt) =
       | If (_, tb, fb, _, _) -> (fasBlock todo tb; fasBlock todo fb)
       | Switch (_, b, _, _, _) -> fasBlock todo b
       | Loop (b, _, _, _, _) -> fasBlock todo b
-      | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _) -> ()
+      | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _ | Asm _) -> ()
   end
 ;;
 
@@ -270,6 +271,7 @@ let d_cfgnodelabel () (s : stmt) =
       | Switch _ -> "switch"
       | Block _ -> "block"
       | Return _ -> "return"
+      | Asm _ -> "asm"
   end in
     dprintf "%d: %s" s.sid label
 

src/check.ml

@@ -808,9 +808,22 @@ and checkStmt (s: stmt) =
               findCase !statements)
             cases;
 
-      | Instr il -> List.iter checkInstr il)
+      | Instr il -> List.iter checkInstr il
+      | Asm (_, _, _, _, _, labels, l) ->
+        currentLoc := l;
+        List.iter (fun dest ->
+          List.iter (fun label ->
+            let name = match label with
+              | Label (name, _, true) -> name
+              | _ -> failwith "unreachable"
+            in
+            gotoTargets := (name, !dest) :: !gotoTargets
+          ) !dest.labels;
+        ) labels;
+      )
     () (* argument of withContext *)
 
+
 and checkBlock (b: block) : unit =
   List.iter checkStmt b.bstmts
 
@@ -883,8 +896,6 @@ and checkInstr (i: instr) =
       if not v.vhasdeclinstruction then
         E.s (bug "Encountered a VarDecl, but vhasdeclinstruction for the varinfo is not set")
 
-  | Asm _ -> ()  (* Not yet implemented *)
-
 let rec checkGlobal = function
     GAsm _ -> ()
   | GPragma _ -> ()

src/cil.ml

@@ -813,6 +813,34 @@ and stmtkind =
                                             as a way to keep some attributes
                                             local *)
 
+  (* See the GCC specification for the meaning of ASM.
+     If the source is MS VC then only the templates
+     are used *)
+  (* sm: I've added a notes.txt file which contains more
+     information on interpreting Asm instructions *)
+  | Asm        of attributes * (* Really only const and volatile can appear
+          here *)
+  string list *         (* templates (CR-separated) *)
+  (string option * string * lval) list *
+                   (* outputs must be lvals with
+                      optional names and constraints.
+                      I would like these
+                      to be actually variables, but I
+                      run into some trouble with ASMs
+                      in the Linux sources  *)
+  (string option * string * exp) list *
+                 (* inputs with optional names and constraints *)
+  string list *         (* register clobbers *)
+  stmt ref list *       (* referenced labels *)
+  location
+  (** An inline assembly instruction. The arguments are (1) a list of
+  attributes (only const and volatile can appear here and only for
+  GCC), (2) templates (CR-separated), (3) a list of
+  outputs, each of which is an lvalue with a constraint, (4) a list
+  of input expressions along with constraints, (5) clobbered
+  registers, (6) the labels list for asm goto, and (7) location information *)
+
+
 (** Instructions. They may cause effects directly but may not have control
     flow.*)
 and instr =
@@ -840,33 +868,6 @@ and instr =
                              result then an implicit cast exists.
                              Second location is just for expression when inside condition. *)
 
-                         (* See the GCC specification for the meaning of ASM.
-                            If the source is MS VC then only the templates
-                            are used *)
-                         (* sm: I've added a notes.txt file which contains more
-                            information on interpreting Asm instructions *)
-  | Asm        of attributes * (* Really only const and volatile can appear
-                                 here *)
-                  string list *         (* templates (CR-separated) *)
-                  (string option * string * lval) list *
-                                          (* outputs must be lvals with
-                                             optional names and constraints.
-                                             I would like these
-                                             to be actually variables, but I
-                                             run into some trouble with ASMs
-                                             in the Linux sources  *)
-                  (string option * string * exp) list *
-                                        (* inputs with optional names and constraints *)
-                  string list *         (* register clobbers *)
-                  location
-        (** An inline assembly instruction. The arguments are (1) a list of
-            attributes (only const and volatile can appear here and only for
-            GCC), (2) templates (CR-separated), (3) a list of
-            outputs, each of which is an lvalue with a constraint, (4) a list
-            of input expressions along with constraints, (5) clobbered
-            registers, and (5) location information *)
-
-
 
 (** Describes a location in a source file *)
 and location = {
@@ -1125,7 +1126,6 @@ let get_instrLoc (inst : instr) =
   match inst with
       Set(_, _, loc, _) -> loc
     | Call(_, _, _, loc, _) -> loc
-    | Asm(_, _, _, _, _, loc) -> loc
     | VarDecl(_,loc) -> loc
 let get_globalLoc (g : global) =
   match g with
@@ -1155,6 +1155,7 @@ let rec get_stmtLoc (statement : stmtkind) =
     | Loop (_, loc, _, _, _) -> loc
     | Block b -> if b.bstmts == [] then lu
                  else get_stmtLoc ((List.hd b.bstmts).skind)
+    | Asm (_, _, _, _, _, _, loc) -> loc
 
 
 (* The next variable identifier to use. Counts up *)
@@ -1353,8 +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 dummyStmt =  mkStmt (Instr [dummyInstr])
+let dummyStmt =  mkStmt (Asm([], ["dummy statement!!"], [], [], [], [], lu))
 
 let compactStmts (b: stmt list) : stmt list =
       (* Try to compress statements. Scan the list of statements and remember
@@ -3708,53 +3708,6 @@ class defaultCilPrinterClass : cilPrinter = object (self)
              ++ unalign)
         ++ text (")" ^ printInstrTerminator)
 
-    | Asm(attrs, tmpls, outs, ins, clobs, l) ->
-        self#pLineDirective l
-          ++ text ("__asm__ ")
-          ++ self#pAttrs () attrs
-          ++ text " ("
-          ++ (align
-                ++ (docList ~sep:line
-                      (fun x -> text ("\"" ^ escape_string x ^ "\""))
-                      () tmpls)
-                ++
-                (if outs = [] && ins = [] && clobs = [] then
-                  chr ':'
-              else
-                (text ": "
-                    ++ (docList ~sep:(chr ',' ++ break)
-                          (fun (idopt, c, lv) ->
-                          text(match idopt with
-                                None -> ""
-                              | Some id -> "[" ^ id ^ "] "
-                          ) ++
-                            text ("\"" ^ escape_string c ^ "\" (")
-                              ++ self#pLval () lv
-                              ++ text ")") () outs)))
-              ++
-                (if ins = [] && clobs = [] then
-                  nil
-                else
-                  (text ": "
-                      ++ (docList ~sep:(chr ',' ++ break)
-                            (fun (idopt, c, e) ->
-                              text(match idopt with
-                                    None -> ""
-                                  | Some id -> "[" ^ id ^ "] "
-                              ) ++
-                              text ("\"" ^ escape_string c ^ "\" (")
-                                ++ self#pExp () e
-                                ++ text ")") () ins)))
-                ++
-                (if clobs = [] then nil
-                else
-                  (text ": "
-                      ++ (docList ~sep:(chr ',' ++ break)
-                            (fun c -> text ("\"" ^ escape_string c ^ "\""))
-                            ()
-                            clobs)))
-                ++ unalign)
-          ++ text (")" ^ printInstrTerminator)
 
 
   (**** STATEMENTS ****)
@@ -3977,6 +3930,82 @@ class defaultCilPrinterClass : cilPrinter = object (self)
                   ++ self#pBlock () b)
     end
     | Block b -> align ++ self#pBlock () b
+    | Asm(attrs, tmpls, outs, ins, clobs, labels, l) ->
+        let rec names_of_stmtrefs stmtrefs =
+          match stmtrefs with
+          | [] -> []
+          | stmtref :: xs -> 
+            let s = !stmtref in
+            let rec names_of_labels = function
+              | [] -> []
+              | Label (name, _, true) :: ys -> name :: names_of_labels ys
+              | Label (_, _, false) :: ys -> names_of_labels ys
+              | _ -> failwith "unreachable"
+            in
+            let names = names_of_labels s.labels in
+            let rest = names_of_stmtrefs xs in
+            let rec prepend_new_names (names: string list) rest =
+              match names with
+              | [] -> rest
+              | name :: ys when not (List.mem name rest) -> prepend_new_names ys (name :: rest)
+              | _ :: ys -> prepend_new_names ys rest
+            in
+            prepend_new_names names rest
+        in
+        self#pLineDirective l
+          ++ text ("__asm__ ")
+          ++ self#pAttrs () attrs
+          ++ text " ("
+          ++ (align
+                ++ (docList ~sep:line
+                      (fun x -> text ("\"" ^ escape_string x ^ "\""))
+                      () tmpls)
+                ++
+                (if outs = [] && ins = [] && clobs = [] && labels = [] then
+                  nil
+              else
+                (text ": "
+                    ++ (docList ~sep:(chr ',' ++ break)
+                          (fun (idopt, c, lv) ->
+                          text(match idopt with
+                                None -> ""
+                              | Some id -> "[" ^ id ^ "] "
+                          ) ++
+                            text ("\"" ^ escape_string c ^ "\" (")
+                              ++ self#pLval () lv
+                              ++ text ")") () outs)))
+              ++
+                (if ins = [] && clobs = [] && labels = [] then
+                  nil
+                else
+                  (text ": "
+                      ++ (docList ~sep:(chr ',' ++ break)
+                            (fun (idopt, c, e) ->
+                              text(match idopt with
+                                    None -> ""
+                                  | Some id -> "[" ^ id ^ "] "
+                              ) ++
+                              text ("\"" ^ escape_string c ^ "\" (")
+                                ++ self#pExp () e
+                                ++ text ")") () ins)))
+                ++
+                (if clobs = [] && labels = [] then nil
+                else
+                  (text ": "
+                      ++ (docList ~sep:(chr ',' ++ break)
+                            (fun c -> text ("\"" ^ escape_string c ^ "\""))
+                            ()
+                            clobs)))
+                ++
+                (if labels = [] then nil
+                else
+                  (text ": "
+                      ++ (docList ~sep:(chr ',' ++ break)
+                            text
+                            ()
+                            (names_of_stmtrefs labels))))
+                ++ unalign)
+          ++ text (")" ^ printInstrTerminator)
 
 
   (*** GLOBALS ***)
@@ -4329,6 +4358,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
     | "aconst", [] -> text "__const__", true
     | "thread", [] -> text "__thread", false
     | "volatile", [] -> text "volatile", false
+    | "goto", [] -> text "goto", false
     | "restrict", [] -> text "__restrict", false
     | "missingproto", [] -> text "/* missing proto */", false
     | "asm", args ->
@@ -4355,7 +4385,6 @@ class defaultCilPrinterClass : cilPrinter = object (self)
     | "arraylen", [a] ->
         (* text "/*[" ++ self#pAttrParam () a ++ text "]*/" *) nil, false
 
-
     | _ -> (* This is the default case *)
         (* Add underscores to the name *)
         let an' =  "__" ^ an ^ "__" in
@@ -5325,16 +5354,6 @@ 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) ->
-      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
-
 
 (* visit all nodes in a Cil statement tree in preorder *)
 and visitCilStmt (vis: cilVisitor) (s: stmt) : stmt =
@@ -5397,6 +5416,15 @@ and childrenStmt (toPrepend: instr list ref) : cilVisitor -> stmt -> stmt =
     | Block b ->
         let b' = fBlock b in
         if b' != b then Block b' else s.skind
+    | Asm(sl,isvol,outs,ins,clobs,labels,l) ->
+        let outs' = mapNoCopy (fun ((id,s,lv) as pair) ->
+                                 let lv' = visitCilLval vis 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,labels,l) else s.skind
   in
   if skind' != s.skind then s.skind <- skind';
   (* Visit the labels *)
@@ -5884,7 +5912,7 @@ let rec peepHole1 (* Process one instruction and possibly replace it *)
       | Switch (e, b, _, _, _) -> peepHole1 doone b.bstmts
       | Loop (b, l, el, _, _) -> peepHole1 doone b.bstmts
       | Block b -> peepHole1 doone b.bstmts
-      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ())
+      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ -> ())
     ss
 
 let rec peepHole2  (* Process two instructions and possibly replace them both *)
@@ -5912,7 +5940,7 @@ let rec peepHole2  (* Process two instructions and possibly replace them both *)
       | Loop (b, l, el, _, _) -> peepHole2 dotwo b.bstmts
       | Block b -> peepHole2 dotwo b.bstmts
 
-      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ())
+      | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ -> ())
     ss
 
 
@@ -6005,8 +6033,8 @@ let typeSigAttrs = function
 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)
+let dStmt: doc -> location -> stmt =
+  fun d l -> mkStmt (Asm([], [sprint ~width:!lineLength d], [], [], [], [], l))
 
 let dGlobal: doc -> location -> global =
   fun d l -> GAsm(sprint ~width:!lineLength d, l)
@@ -6517,6 +6545,7 @@ and succpred_stmt s fallthrough rlabels =
                 | hd :: tl -> link s hd ;
                     succpred_block b fallthrough rlabels
                 end
+  | Asm _ -> trylink s fallthrough
 
 
 let caseRangeFold (l: label list) =
@@ -6581,7 +6610,7 @@ let rec xform_switch_stmt s break_dest cont_dest = begin
   | Default(l,el) -> Label(freshLabel "switch_default",l,false)
   ) s.labels ;
   match s.skind with
-  | Instr _ | Return _ | Goto _ | ComputedGoto _ -> ()
+  | Instr _ | Return _ | Goto _ | ComputedGoto _ | Asm _ -> ()
   | Break(l) -> begin try
                   s.skind <- Goto(break_dest (),l)
                 with e ->