From 3ff22e89c00717c3dcea9f0255ad21ffbb2090cd Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Thu, 16 Nov 2023 17:44:01 +0100 Subject: [PATCH 01/26] support for asm goto; untested but compiles --- src/frontc/cabs.ml | 3 ++- src/frontc/cabsvisit.ml | 4 +-- src/frontc/cparser.mly | 59 ++++++++++++++++++++++++++++++++++++----- 3 files changed, 56 insertions(+), 10 deletions(-) diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index d13025b53..c6a318c02 100644 --- a/src/frontc/cabs.ml +++ b/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 *) + alabels: string list option; (* referenced labels *) } and statement = diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index f6344874c..49e168e43 100644 --- a/src/frontc/cabsvisit.ml +++ b/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; alabels = labels } -> 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; alabels = labels } in if details' != details then ASM (sl, b, details', l) else s diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 17fa5a34d..bcc6f48af 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -244,6 +244,36 @@ let transformOffsetOf (speclist, dtype) member = queue; Buffer.contents buffer + let checkAsm asm = match asm with + | ASM (attrs, _, details, _) -> + let no_labels_but_goto = ref false in + let no_goto_but_labels = ref false in + let _ = begin + match details with + | None -> + if Option.is_some (List.assoc_opt "goto" attrs) then + no_labels_but_goto := true + else () + | Some details -> + if Option.is_some (List.assoc_opt "goto" attrs) then + if Option.is_none details.alabels then + no_labels_but_goto := true + else () + else if Option.is_some details.alabels then + no_goto_but_labels := true + else () + ; + if !no_labels_but_goto then begin + parse_error "expected ':' for labels list in asm goto"; + raise Parsing.Parse_error + end else (); + if !no_goto_but_labels then begin + parse_error "labels provided in inline asm without goto attribute"; + raise Parsing.Parse_error + end else (); + end in asm + | _ -> failwith "called checkAsm with non-asm variant" + %} %token IDENT @@ -982,7 +1012,7 @@ statement_no_null: | GOTO STAR comma_expression SEMICOLON { COMPGOTO (smooth_expression (fst $3), joinLoc $1 $4) } | ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON - { ASM ($2, $4, $5, joinLoc $1 $7) } + { checkAsm (ASM ($2, $4, $5, joinLoc $1 $7)) } | error location SEMICOLON { (NOP $2)} ; @@ -1646,6 +1676,7 @@ asmattr: | VOLATILE asmattr { ("volatile", []) :: $2 } | CONST asmattr { ("const", []) :: $2 } | INLINE asmattr { ("inline", []) :: $2 } +| GOTO asmattr { ("goto", []) :: $2 } ; asmtemplate: one_string_constant { [$1] } @@ -1654,8 +1685,11 @@ asmtemplate: asmoutputs: /* empty */ { None } | COLON asmoperands asminputs - { let (ins, clobs) = $3 in - Some {aoutputs = $2; ainputs = ins; aclobbers = clobs} } + { let (ins, clobs, labels) = $3 in + Some {aoutputs = $2; + ainputs = ins; + aclobbers = clobs; + alabels = labels} } ; asmoperands: /* empty */ { [] } @@ -1672,9 +1706,9 @@ asmoperand: ; asminputs: - /* empty */ { ([], []) } + /* empty */ { ([], [], None) } | COLON asmoperands asmclobber - { ($2, $3) } + { ($2, fst $3, snd $3) } ; asmopname: /* empty */ { None } @@ -1682,8 +1716,8 @@ asmopname: ; asmclobber: - /* empty */ { [] } -| COLON asmclobberlst { $2 } + /* empty */ { ([], None) } +| COLON asmclobberlst asmlabels { ($2, $3) } ; asmclobberlst: /* empty */ { [] } @@ -1693,5 +1727,16 @@ asmclobberlst_ne: one_string_constant { [$1] } | one_string_constant COMMA asmclobberlst_ne { $1 :: $3 } ; +asmlabels: + /* empty */ { None } +| COLON asmlabelslst { $2 } +; +asmlabelslst: + /* empty */ { Some [] } +| asmlabelslst_ne { Some $1 } +; +asmlabelslst_ne: + IDENT { [fst $1] } +| IDENT COMMA asmlabelslst_ne { (fst $1) :: $3 } %% From a76f439bb26a434993ca1b9592aef7006c0eec47 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Fri, 17 Nov 2023 08:31:23 +0100 Subject: [PATCH 02/26] intermidiary commit, so that everyone has same type definition --- src/cil.ml | 55 ++++++++++++++--------------- src/cil.mli | 79 +++++++++++++++++++++--------------------- src/frontc/cabs2cil.ml | 2 +- src/frontc/cprint.ml | 20 +++++++---- src/frontc/frontc.mli | 3 ++ src/main.ml | 4 ++- 6 files changed, 89 insertions(+), 74 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 8a28dc19e..9d5ccbe92 100755 --- a/src/cil.ml +++ b/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, and (5) 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 = { diff --git a/src/cil.mli b/src/cil.mli index a2ee2d506..65a4c55c3 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1007,35 +1007,6 @@ and stmtkind = (** Just a block of statements. Use it as a way to keep some block attributes local *) -(** {b Instructions}. - An instruction {!instr} is a statement that has no local -(intraprocedural) control flow. It can be either an assignment, -function call, or an inline assembly instruction. *) - -(** Instructions. *) -and instr = - Set of lval * exp * location * location - (** An assignment. The type of the expression is guaranteed to be the same - with that of the lvalue. - Second location is just for expression when inside condition. *) - | VarDecl of varinfo * location - (** "Instruction" in the location where a varinfo was declared. - All varinfos for which such a VarDecl instruction exists have - vhasdeclinstruction set to true. - The motivation for the addition of this instruction was to support VLAs - for which declerations can not be pulled up like CIL used to do. - *) - | Call of lval option * exp * exp list * location * location - (** A function call with the (optional) result placed in an lval. It is - possible that the returned type of the function is not identical to - that of the lvalue. In that case a cast is printed. The type of the - actual arguments are identical to those of the declared formals. The - number of arguments is the same as that of the declared formals, except - for vararg functions. This construct is also used to encode a call to - "__builtin_va_arg". In this case the second argument (which should be a - type T) is encoded SizeOf(T). - Second location is just for expression when inside condition. *) - | Asm of attributes * (* Really only const and volatile can appear here *) string list * (* templates (CR-separated) *) @@ -1049,17 +1020,18 @@ and instr = (string option * string * exp) list * (* inputs with optional names and constraints *) string list * (* register clobbers *) + stmt ref list * (* referenced labels *) location (** There are for storing inline assembly. They follow the GCC specification: -{v + {v asm [volatile] ("...template..." "..template.." : "c1" (o1), "c2" (o2), ..., "cN" (oN) : "d1" (i1), "d2" (i2), ..., "dM" (iM) : "r1", "r2", ..., "nL" ); - v} + v} -where the parts are + where the parts are - [volatile] (optional): when present, the assembler instruction cannot be removed, moved, or otherwise optimized @@ -1080,24 +1052,53 @@ where the parts are - "rk": registers to be regarded as "clobbered" by the instruction; "memory" may be specified for arbitrary memory effects -an example (from gcc manual): -{v + an example (from gcc manual): + {v asm volatile ("movc3 %0,%1,%2" : /* no outputs */ : "g" (from), "g" (to), "g" (count) : "r0", "r1", "r2", "r3", "r4", "r5"); - v} + v} - Starting with gcc 3.1, the operands may have names: + Starting with gcc 3.1, the operands may have names: -{v + {v asm volatile ("movc3 %[in0],%1,%2" : /* no outputs */ : [in0] "g" (from), "g" (to), "g" (count) : "r0", "r1", "r2", "r3", "r4", "r5"); - v} + v} -*) + *) + +(** {b Instructions}. + An instruction {!instr} is a statement that has no local +(intraprocedural) control flow. It can be either an assignment, +function call, or an inline assembly instruction. *) + +(** Instructions. *) +and instr = + Set of lval * exp * location * location + (** An assignment. The type of the expression is guaranteed to be the same + with that of the lvalue. + Second location is just for expression when inside condition. *) + | VarDecl of varinfo * location + (** "Instruction" in the location where a varinfo was declared. + All varinfos for which such a VarDecl instruction exists have + vhasdeclinstruction set to true. + The motivation for the addition of this instruction was to support VLAs + for which declerations can not be pulled up like CIL used to do. + *) + | Call of lval option * exp * exp list * location * location + (** A function call with the (optional) result placed in an lval. It is + possible that the returned type of the function is not identical to + that of the lvalue. In that case a cast is printed. The type of the + actual arguments are identical to those of the declared formals. The + number of arguments is the same as that of the declared formals, except + for vararg functions. This construct is also used to encode a call to + "__builtin_va_arg". In this case the second argument (which should be a + type T) is encoded SizeOf(T). + Second location is just for expression when inside condition. *) (** Describes a location in a source file. *) and location = { diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 34e0c6f0d..e5250f3e1 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6924,7 +6924,7 @@ and doStatement (s : A.statement) : chunk = Util.list_map escape tmpls in (tmpls', [], [], []) - | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } -> + | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; alabels = labels } -> let outs' = Util.list_map (fun (id, c, e) -> diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 07a75ada5..05529a65f 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -117,8 +117,9 @@ let print_list print_sep print_elt lst = () let print_commas nl fct lst = - print_list (fun () -> print ","; if nl then new_line() else space()) fct lst; - print_maybe "," + print_list (fun () -> print ","; if nl then new_line() else space()) fct lst + (* todo: uncomment *) + (* print_maybe "," *) let print_string (s:string) = print ("\"" ^ escape_string s ^ "\"") @@ -718,15 +719,22 @@ and print_statement stat = begin match details with | None -> () - | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } -> + | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; alabels = labels } -> print ":"; space (); print_commas false print_asm_operand outs; - if ins <> [] || clobs <> [] then begin + let labels_exist = Option.is_some labels in + if ins <> [] || clobs <> [] || labels_exist then begin print ":"; space (); print_commas false print_asm_operand ins; - if clobs <> [] then begin + if clobs <> [] || labels_exist then begin print ":"; space (); - print_commas false print_string clobs + print_commas false print_string clobs; + if labels_exist then + let labels = Option.get labels in + if labels <> [] then begin + print ":"; space (); + print_commas false print labels + end; end; end end; diff --git a/src/frontc/frontc.mli b/src/frontc/frontc.mli index 001d36166..1bae586a5 100644 --- a/src/frontc/frontc.mli +++ b/src/frontc/frontc.mli @@ -51,6 +51,9 @@ val resetErrors: unit -> unit val parse: string -> (unit -> Cil.file) +(* todo: delete *) +val parse_to_cabs: string -> Cabs.file + val parse_with_cabs: string -> (unit -> Cabs.file * Cil.file) val parse_standalone_exp: string -> Cabs.expression diff --git a/src/main.ml b/src/main.ml index b257176ab..e359a0f24 100644 --- a/src/main.ml +++ b/src/main.ml @@ -248,7 +248,9 @@ let _ = Sys.set_signal Sys.sigsegv (Sys.Signal_handle handleSEGV); begin try - theMain (); + (* theMain (); *) + let cabs = F.parse_to_cabs "test_asm.c" in + Cprint.printFile stdout cabs with F.CabsOnly -> (* this is OK *) () end; cleanup (); From f1e3be575cc02a25c29360deaee049c690c1f6e2 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Fri, 17 Nov 2023 09:07:00 +0100 Subject: [PATCH 03/26] todo: move all asm instr matches to stmt matches --- src/frontc/cabs2cil.ml | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index e5250f3e1..9ab731c40 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6915,7 +6915,7 @@ 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', labels') = match details with | None -> let tmpls' = @@ -6923,7 +6923,7 @@ and doStatement (s : A.statement) : chunk = let escape = Str.global_replace pattern "%%" in Util.list_map escape tmpls in - (tmpls', [], [], []) + (tmpls', [], [], [], []) | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; alabels = labels } -> let outs' = Util.list_map @@ -6947,10 +6947,21 @@ and doStatement (s : A.statement) : chunk = (id, c, e')) ins in - (tmpls, outs', ins', clobs) + let labels' = + match labels with + | Some labels -> + Util.list_map (fun lname -> begin + let lref = ref dummyStmt in + addGoto lname lref; + lref + end) + labels + | None -> [] + in + (tmpls, outs', ins', clobs, labels') in !stmts @@ - (i2c (Asm(attr', tmpls', outs', ins', clobs', loc'))) + s2c (mkStmt (Asm(attr', tmpls', outs', ins', clobs', labels', loc'))) with e when continueOnError -> begin (ignore (E.log "Error in doStatement (%s)\n" (Printexc.to_string e))); From 26cc002a9e52ec7970e5c508a87b959086c2b06f Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Fri, 17 Nov 2023 10:45:45 +0100 Subject: [PATCH 04/26] ich hab absolut keinen bock mehr --- src/check.ml | 7 +- src/cil.ml | 130 ++++++++++++++++++---------------- src/cil.mli | 3 + src/ext/liveness/usedef.ml | 20 ++++-- src/ext/pta/ptranal.ml | 2 +- src/ext/zrapp/availexps.ml | 3 + src/ext/zrapp/availexpslv.ml | 3 + src/ext/zrapp/deadcodeelim.ml | 3 + src/ext/zrapp/reachingdefs.ml | 6 ++ src/ext/zrapp/rmciltmps.ml | 3 + src/frontc/cabs2cil.ml | 5 +- 11 files changed, 110 insertions(+), 75 deletions(-) diff --git a/src/check.ml b/src/check.ml index 2924fbe48..b51affefe 100644 --- a/src/check.ml +++ b/src/check.ml @@ -808,9 +808,12 @@ and checkStmt (s: stmt) = findCase !statements) cases; - | Instr il -> List.iter checkInstr il) + | Instr il -> List.iter checkInstr il + | Asm _ -> () (* Not yet implemented *) + ) () (* argument of withContext *) + and checkBlock (b: block) : unit = List.iter checkStmt b.bstmts @@ -883,8 +886,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 _ -> () diff --git a/src/cil.ml b/src/cil.ml index 9d5ccbe92..fb192d403 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -1126,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 @@ -1156,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 *) @@ -1354,8 +1354,8 @@ 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 dummyInstr = (Asm([], ["dummy statement!!"], [], [], [], [], lu)) +let dummyStmt = mkStmt dummyInstr let compactStmts (b: stmt list) : stmt list = (* Try to compress statements. Scan the list of statements and remember @@ -3709,53 +3709,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 ****) @@ -3978,6 +3931,54 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ self#pBlock () b) end | Block b -> align ++ self#pBlock () b + | Asm(attrs, tmpls, outs, ins, clobs, labels, l) -> + (* todo: labels are ignored during printing *) + 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) (*** GLOBALS ***) @@ -5326,16 +5327,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 = @@ -5398,6 +5389,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 *) @@ -5885,7 +5885,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 *) @@ -5913,7 +5913,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 @@ -6006,8 +6006,11 @@ let typeSigAttrs = function let dExp: doc -> exp = fun d -> Const(CStr(sprint ~width:!lineLength d, No_encoding)) +(* todo: is this even used anywhere *) +(* let dInstr: doc -> location -> instr = fun d l -> Asm([], [sprint ~width:!lineLength d], [], [], [], l) +*) let dGlobal: doc -> location -> global = fun d l -> GAsm(sprint ~width:!lineLength d, l) @@ -6518,6 +6521,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) = @@ -6582,7 +6586,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 -> diff --git a/src/cil.mli b/src/cil.mli index 65a4c55c3..ccd889c3a 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -2652,7 +2652,10 @@ val get_stmtLoc: stmtkind -> location val dExp: Pretty.doc -> exp (** Generate an {!instr} to be used in case of errors. *) +(* todo: commenting this out is probably a bad idea *) +(* val dInstr: Pretty.doc -> location -> instr +*) (** Generate a {!global} to be used in case of errors. *) val dGlobal: Pretty.doc -> location -> global diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml index 76afb839b..dbee1f069 100644 --- a/src/ext/liveness/usedef.ml +++ b/src/ext/liveness/usedef.ml @@ -150,12 +150,6 @@ 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) -> - match lv with (Var v, off) -> - if s.[0] = '+' then - varUsed := VS.add v !varUsed; - | _ -> ()) slvl; - DoChildren | _ -> DoChildren end @@ -200,6 +194,15 @@ let computeUseDefStmtKind ?(acc_used=VS.empty) | Instr il -> List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il | Block _ -> () + | Asm (_, _, outs, ins, _, _, _) -> + List.iter (fun (_, _, lval) -> match lval with + | (Var v, _) -> varUsed := VS.add v !varUsed + | _ -> () + ) outs; + List.iter (fun (_, _, exp) -> match exp with + | Lval(Var v, _) -> varUsed := VS.add v !varUsed + | _ -> () + ) ins; in !varUsed, !varDefs @@ -242,6 +245,11 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty) List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il; !varUsed, !varDefs | Block b -> handle_block b + | Asm (i, love, ocaml, this, is, so, amazing) -> + computeUseDefStmtKind + ~acc_used:!varUsed + ~acc_defs:!varDefs + (Asm (i, love, ocaml, this, is, so, amazing)) let computeUseLocalTypes ?(acc_used=VS.empty) (fd : fundec) diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index 2e8dffd6e..ca049367a 100644 --- a/src/ext/pta/ptranal.ml +++ b/src/ext/pta/ptranal.ml @@ -298,7 +298,6 @@ let analyze_instr (i : instr ) : unit = Some r -> A.assign_ret site (analyze_lval r) fnres | None -> () end - | Asm _ -> () | VarDecl _ -> () let rec analyze_stmt (s : stmt ) : unit = @@ -328,6 +327,7 @@ let rec analyze_stmt (s : stmt ) : unit = | Block b -> analyze_block b | Break l -> () | Continue l -> () + | Asm _ -> () and analyze_block (b : block ) : unit = diff --git a/src/ext/zrapp/availexps.ml b/src/ext/zrapp/availexps.ml index e9983e2cb..453e7e128 100644 --- a/src/ext/zrapp/availexps.ml +++ b/src/ext/zrapp/availexps.ml @@ -243,11 +243,14 @@ let eh_handle_inst i eh = (eh_kill_mem eh; eh_kill_addrof_or_global eh; eh) + (* todo: didn't find location where stmts are handled *) + (* | Asm(_,_,_,_,_,_) -> let _,d = UD.computeUseDefInstr i in (UD.VS.iter (fun vi -> eh_kill_vi eh vi) d; eh) + *) | VarDecl _ -> raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexps, to make availexps work for programs without VLA *) (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this. *) diff --git a/src/ext/zrapp/availexpslv.ml b/src/ext/zrapp/availexpslv.ml index 321b9f656..73939607e 100644 --- a/src/ext/zrapp/availexpslv.ml +++ b/src/ext/zrapp/availexpslv.ml @@ -305,12 +305,15 @@ let lvh_handle_inst i lvh = end; lvh end + (* todo *) + (* | Asm(_,_,_,_,_,_) -> begin let _,d = UD.computeUseDefInstr i in UD.VS.iter (fun vi -> lvh_kill_vi lvh vi) d; lvh end + *) | VarDecl _ -> raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexpslv, to make availexpslv work for programs without VLA *) (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this. *) diff --git a/src/ext/zrapp/deadcodeelim.ml b/src/ext/zrapp/deadcodeelim.ml index f1135fd8d..72716b03d 100644 --- a/src/ext/zrapp/deadcodeelim.ml +++ b/src/ext/zrapp/deadcodeelim.ml @@ -102,11 +102,14 @@ class usedDefsCollectorClass = object(self) method! vinst i = let handle_inst iosh i = match i with + (* todo *) + (* | 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) | _ -> ()) slvl + *) | Call(_,ce,el,_,_) when not (!callHasNoSideEffects i) -> List.iter (fun e -> let u = UD.computeUseExp e in diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml index 8a8a2a028..d708f926c 100644 --- a/src/ext/zrapp/reachingdefs.ml +++ b/src/ext/zrapp/reachingdefs.ml @@ -270,8 +270,11 @@ 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 + (* todo *) + (* | Asm(_,_,sll,_,_,_) -> List.exists (function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll + *) | _ -> false) | None -> false) iihl in (match i with @@ -284,7 +287,10 @@ 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)) + (* todo *) + (* | Asm(a,sl,slvl,sel,sl',_) -> None + *) | VarDecl _ -> None ) (* ? *) with Not_found -> diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index dad6dce77..aeec09ea1 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -994,6 +994,8 @@ class unusedRemoverClass : cilVisitor = object(self) (match IH.find iioh vi.vid with None -> true | Some _ -> false) end + (* todo *) + (* | Asm(_,_,slvlst,_,_,_) -> begin (* make sure the outputs are in the locals list *) List.iter (fun (_,s,lv) -> @@ -1004,6 +1006,7 @@ class unusedRemoverClass : cilVisitor = object(self) |_ -> ()) slvlst; true end + *) | _ -> true in diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 9ab731c40..9c5678372 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -843,7 +843,6 @@ 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) (** Change all stmt and instr locs to synthetic, except the first one. Expressions/initializers that expand to multiple instructions cannot have intermediate locations referenced. *) @@ -881,6 +880,7 @@ module BlockChunk = | Block b -> doBlock ~first b; s.skind + | Asm (a, b, c, d, e, l, loc) -> Asm (a, b, c, d, e, l, doLoc loc) and doBlock ~first b = doStmts ~first b.bstmts and doStmts ~first = function @@ -919,6 +919,7 @@ module BlockChunk = | Block b -> doBlock b; s.skind + | Asm (a, b, c, d, e, l, loc) -> Asm (a, b, c, d, e, l, doLoc loc) and doBlock b = doStmts b.bstmts and doStmts = function @@ -6370,7 +6371,6 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function else if hasAttribute "noreturn" e.vattr then false else true | Call _ -> true - | Asm _ -> true | VarDecl _ -> true in let rec stmtFallsThrough (s: stmt) : bool = @@ -6402,6 +6402,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function (* A loop falls through if it can break. *) blockCanBreak b | Block b -> blockFallsThrough b + | Asm _ -> true and blockFallsThrough b = let rec fall = function [] -> true From d01d6ec5e23e4c85f46f2572033694a8114362e4 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Fri, 17 Nov 2023 11:00:23 +0100 Subject: [PATCH 05/26] proposal to solve dInstr problem --- src/cil.ml | 5 +++-- src/cil.mli | 4 ++++ src/frontc/cabs2cil.ml | 2 +- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index fb192d403..514d2cc41 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -1354,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 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 @@ -6011,6 +6010,8 @@ let dExp: doc -> exp = 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) diff --git a/src/cil.mli b/src/cil.mli index ccd889c3a..6b7e2c63d 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1753,7 +1753,10 @@ val compactStmts: stmt list -> stmt list val mkEmptyStmt: unit -> stmt (** A instr to serve as a placeholder *) +(* todo: maybe this can be removed? *) +(* val dummyInstr: instr +*) (** A statement consisting of just [dummyInstr] *) val dummyStmt: stmt @@ -2656,6 +2659,7 @@ val dExp: Pretty.doc -> exp (* val dInstr: Pretty.doc -> location -> instr *) +val dStmt: Pretty.doc -> location -> stmt (** Generate a {!global} to be used in case of errors. *) val dGlobal: Pretty.doc -> location -> global diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 9c5678372..4d06bc1f4 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -4972,7 +4972,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) with e when continueOnError -> begin (*ignore (E.log "error in doExp (%s)" (Printexc.to_string e));*) E.hadErrors := true; - (i2c (dInstr (dprintf "booo_exp(%t)" d_thisloc) !currentLoc), + (s2c (dStmt (dprintf "booo_exp(%t)" d_thisloc) !currentLoc), integer 0, intType) end From d0dcf8cdd4355995544e314f1d60b1cf544dee11 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Fri, 17 Nov 2023 15:25:43 +0100 Subject: [PATCH 06/26] why goblint no work??? --- src/cfg.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cfg.ml b/src/cfg.ml index 8ce0c52a6..b07851155 100644 --- a/src/cfg.ml +++ b/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 _ -> addOptionSucc next (*------------------------------------------------------------*) @@ -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 From 7e5435dbebc63b0bcda6bc84fe874a2e9187c3c1 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Fri, 17 Nov 2023 16:41:39 +0100 Subject: [PATCH 07/26] normal gobint-cil main.exe works but from gobint --justcil doesn't --- src/dataflow.ml | 2 +- src/ext/syntacticsearch/funcVar.ml | 2 ++ src/frontc/cabs2cil.ml | 2 +- src/main.ml | 4 +++- src/mergecil.ml | 1 + 5 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/dataflow.ml b/src/dataflow.ml index cd19e3f34..eb3c3e792 100644 --- a/src/dataflow.ml +++ b/src/dataflow.ml @@ -221,7 +221,7 @@ module ForwardsDataFlow = List.fold_left handleInstruction curr il | Goto _ | ComputedGoto _ | Break _ | Continue _ | If _ - | Switch _ | Loop _ | Return _ | Block _ -> curr + | Switch _ | Loop _ | Return _ | Block _ | Asm _ -> curr in currentLoc := get_stmtLoc s.skind; diff --git a/src/ext/syntacticsearch/funcVar.ml b/src/ext/syntacticsearch/funcVar.ml index 857d0b042..2c90423c2 100644 --- a/src/ext/syntacticsearch/funcVar.ml +++ b/src/ext/syntacticsearch/funcVar.ml @@ -160,7 +160,9 @@ let rec search_instr_list_for_var list name varid includeCallTmp = @ search_expression_list exp_list name loc varid includeCallTmp @ search_instr_list_for_var xs name varid includeCallTmp (* Should I consider Asm too? *) + (* | _ :: xs -> search_instr_list_for_var xs name varid includeCallTmp + *) | [] -> [] (* Finds a variable in a list of statements *) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 4d06bc1f4..16c6bf68f 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6440,7 +6440,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function (* will we leave this statement or block with a break command? *) and stmtCanBreak (s: stmt) : bool = match s.skind with - Instr _ | Return _ | Continue _ | Goto _ | ComputedGoto _ -> false + Instr _ | Return _ | Continue _ | Goto _ | ComputedGoto _ | Asm _ -> false | Break _ -> true | If (_, b1, b2, _, _) -> blockCanBreak b1 || blockCanBreak b2 diff --git a/src/main.ml b/src/main.ml index e359a0f24..594289bcd 100644 --- a/src/main.ml +++ b/src/main.ml @@ -250,7 +250,9 @@ begin try (* theMain (); *) let cabs = F.parse_to_cabs "test_asm.c" in - Cprint.printFile stdout cabs + Cprint.printFile stdout cabs; + let cil = Cabs2cil.convFile cabs in + (C.dumpFile (!C.printerForMaincil) stdout "cil.out") cil; with F.CabsOnly -> (* this is OK *) () end; cleanup (); diff --git a/src/mergecil.ml b/src/mergecil.ml index 028649c7b..aa20ad9ff 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1165,6 +1165,7 @@ | Switch (_, b, _, _, _) -> 43 + (47 * stmtListSum b.bstmts) (* don't look at stmt list b/c is not part of tree *) | Loop (b, _, _, _, _) -> 49 + (53 * stmtListSum b.bstmts) | Block b -> 59 + (61 * stmtListSum b.bstmts) + | Asm _ -> 71 in (* disabled 2nd and 3rd measure because they appear to get different From a339860985a17511723917e36d2745289334b463 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Sun, 14 Jan 2024 12:33:44 +0100 Subject: [PATCH 08/26] fixed most complaints; (dummy instruction still todo) --- src/cfg.ml | 2 +- src/cil.ml | 2 +- src/ext/liveness/usedef.ml | 8 ++----- src/ext/syntacticsearch/funcVar.ml | 4 ---- src/frontc/cparser.mly | 38 ++++++++++++++++-------------- src/frontc/cprint.ml | 14 +++++------ src/frontc/frontc.mli | 3 --- src/main.ml | 6 +---- 8 files changed, 32 insertions(+), 45 deletions(-) diff --git a/src/cfg.ml b/src/cfg.ml index b07851155..31bb76115 100644 --- a/src/cfg.ml +++ b/src/cfg.ml @@ -225,7 +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 _ -> addOptionSucc next + | Asm _ -> addOptionSucc next (* the extra edges are added inside goblint's cfg *) (*------------------------------------------------------------*) diff --git a/src/cil.ml b/src/cil.ml index 514d2cc41..df82347d1 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -838,7 +838,7 @@ and stmtkind = 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 *) + registers, (5) location information, and (6) the labels list for asm goto *) (** Instructions. They may cause effects directly but may not have control diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml index dbee1f069..96af81fbe 100644 --- a/src/ext/liveness/usedef.ml +++ b/src/ext/liveness/usedef.ml @@ -195,10 +195,6 @@ let computeUseDefStmtKind ?(acc_used=VS.empty) List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il | Block _ -> () | Asm (_, _, outs, ins, _, _, _) -> - List.iter (fun (_, _, lval) -> match lval with - | (Var v, _) -> varUsed := VS.add v !varUsed - | _ -> () - ) outs; List.iter (fun (_, _, exp) -> match exp with | Lval(Var v, _) -> varUsed := VS.add v !varUsed | _ -> () @@ -245,11 +241,11 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty) List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il; !varUsed, !varDefs | Block b -> handle_block b - | Asm (i, love, ocaml, this, is, so, amazing) -> + | Asm (a, b, c, d, e, f, g) -> computeUseDefStmtKind ~acc_used:!varUsed ~acc_defs:!varDefs - (Asm (i, love, ocaml, this, is, so, amazing)) + (Asm (a, b, c, d, e, f, g)) let computeUseLocalTypes ?(acc_used=VS.empty) (fd : fundec) diff --git a/src/ext/syntacticsearch/funcVar.ml b/src/ext/syntacticsearch/funcVar.ml index 2c90423c2..ffd9af22c 100644 --- a/src/ext/syntacticsearch/funcVar.ml +++ b/src/ext/syntacticsearch/funcVar.ml @@ -159,10 +159,6 @@ let rec search_instr_list_for_var list name varid includeCallTmp = search_expression exp name loc varid includeCallTmp @ search_expression_list exp_list name loc varid includeCallTmp @ search_instr_list_for_var xs name varid includeCallTmp - (* Should I consider Asm too? *) - (* - | _ :: xs -> search_instr_list_for_var xs name varid includeCallTmp - *) | [] -> [] (* Finds a variable in a list of statements *) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index bcc6f48af..4be3b01bf 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -244,35 +244,37 @@ let transformOffsetOf (speclist, dtype) member = queue; Buffer.contents buffer - let checkAsm asm = match asm with + (* this makes sure that the labels are only allowed when goto annotation was provided *) + let checkAsm asm = + let is_some = function + | Some _ -> true + | None -> false + in + let is_none opt = not (is_some opt) in + match asm with | ASM (attrs, _, details, _) -> let no_labels_but_goto = ref false in let no_goto_but_labels = ref false in let _ = begin - match details with - | None -> - if Option.is_some (List.assoc_opt "goto" attrs) then - no_labels_but_goto := true - else () - | Some details -> - if Option.is_some (List.assoc_opt "goto" attrs) then - if Option.is_none details.alabels then - no_labels_but_goto := true - else () - else if Option.is_some details.alabels then - no_goto_but_labels := true - else () + match details, (List.assoc_opt "goto" attrs) with + | None, Some _ -> + no_labels_but_goto := true + | Some details, Some _ when is_none details.alabels -> + no_labels_but_goto := true + | Some details, None when is_some details.alabels -> + no_goto_but_labels := true + | _, _ -> () ; if !no_labels_but_goto then begin parse_error "expected ':' for labels list in asm goto"; raise Parsing.Parse_error - end else (); + end; if !no_goto_but_labels then begin parse_error "labels provided in inline asm without goto attribute"; raise Parsing.Parse_error - end else (); + end; end in asm - | _ -> failwith "called checkAsm with non-asm variant" + | _ -> failwith "called checkAsm with non-asm variant" %} @@ -1729,7 +1731,7 @@ asmclobberlst_ne: ; asmlabels: /* empty */ { None } -| COLON asmlabelslst { $2 } +| COLON asmlabelslst { $2 } /* This is not asmlabelslst_ne because we distinguish between no labels field (None) and no labels provided (Some []) */ ; asmlabelslst: /* empty */ { Some [] } diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 05529a65f..58cf85e45 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -117,9 +117,8 @@ let print_list print_sep print_elt lst = () let print_commas nl fct lst = - print_list (fun () -> print ","; if nl then new_line() else space()) fct lst - (* todo: uncomment *) - (* print_maybe "," *) + print_list (fun () -> print ","; if nl then new_line() else space()) fct lst; + print_maybe "," let print_string (s:string) = print ("\"" ^ escape_string s ^ "\"") @@ -722,7 +721,7 @@ and print_statement stat = | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; alabels = labels } -> print ":"; space (); print_commas false print_asm_operand outs; - let labels_exist = Option.is_some labels in + let labels_exist = match labels with Some _ -> true | None -> false in if ins <> [] || clobs <> [] || labels_exist then begin print ":"; space (); print_commas false print_asm_operand ins; @@ -730,11 +729,12 @@ and print_statement stat = print ":"; space (); print_commas false print_string clobs; if labels_exist then - let labels = Option.get labels in - if labels <> [] then begin + match labels with + | Some [] -> () + | Some labels -> print ":"; space (); print_commas false print labels - end; + | None -> () end; end end; diff --git a/src/frontc/frontc.mli b/src/frontc/frontc.mli index 1bae586a5..001d36166 100644 --- a/src/frontc/frontc.mli +++ b/src/frontc/frontc.mli @@ -51,9 +51,6 @@ val resetErrors: unit -> unit val parse: string -> (unit -> Cil.file) -(* todo: delete *) -val parse_to_cabs: string -> Cabs.file - val parse_with_cabs: string -> (unit -> Cabs.file * Cil.file) val parse_standalone_exp: string -> Cabs.expression diff --git a/src/main.ml b/src/main.ml index 594289bcd..b257176ab 100644 --- a/src/main.ml +++ b/src/main.ml @@ -248,11 +248,7 @@ let _ = Sys.set_signal Sys.sigsegv (Sys.Signal_handle handleSEGV); begin try - (* theMain (); *) - let cabs = F.parse_to_cabs "test_asm.c" in - Cprint.printFile stdout cabs; - let cil = Cabs2cil.convFile cabs in - (C.dumpFile (!C.printerForMaincil) stdout "cil.out") cil; + theMain (); with F.CabsOnly -> (* this is OK *) () end; cleanup (); From 7236437a1540b1f71b0c9bd87a942ef2b045fb36 Mon Sep 17 00:00:00 2001 From: WernerDrasche <79748606+WernerDrasche@users.noreply.github.com> Date: Mon, 15 Jan 2024 10:14:24 +0100 Subject: [PATCH 09/26] Update cparser.mly --- src/frontc/cparser.mly | 22 ++++++---------------- 1 file changed, 6 insertions(+), 16 deletions(-) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 4be3b01bf..3aeec1a18 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -253,27 +253,17 @@ let transformOffsetOf (speclist, dtype) member = let is_none opt = not (is_some opt) in match asm with | ASM (attrs, _, details, _) -> - let no_labels_but_goto = ref false in - let no_goto_but_labels = ref false in - let _ = begin + let _ = match details, (List.assoc_opt "goto" attrs) with | None, Some _ -> - no_labels_but_goto := true | Some details, Some _ when is_none details.alabels -> - no_labels_but_goto := true - | Some details, None when is_some details.alabels -> - no_goto_but_labels := true - | _, _ -> () - ; - if !no_labels_but_goto then begin - parse_error "expected ':' for labels list in asm goto"; + parse_error "expected ':' for labels list in asm goto"; raise Parsing.Parse_error - end; - if !no_goto_but_labels then begin - parse_error "labels provided in inline asm without goto attribute"; + | Some details, None when is_some details.alabels -> + parse_error "labels provided in inline asm without goto attribute"; raise Parsing.Parse_error - end; - end in asm + | _, _ -> () + in asm | _ -> failwith "called checkAsm with non-asm variant" %} From 8037c21b6942908a3d2200b3cfee97098a492be7 Mon Sep 17 00:00:00 2001 From: WernerDrasche <79748606+WernerDrasche@users.noreply.github.com> Date: Mon, 15 Jan 2024 10:16:30 +0100 Subject: [PATCH 10/26] Update cparser.mly --- src/frontc/cparser.mly | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 3aeec1a18..76e8d8c2a 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -255,7 +255,7 @@ let transformOffsetOf (speclist, dtype) member = | ASM (attrs, _, details, _) -> let _ = match details, (List.assoc_opt "goto" attrs) with - | None, Some _ -> + | None, Some _ | Some details, Some _ when is_none details.alabels -> parse_error "expected ':' for labels list in asm goto"; raise Parsing.Parse_error From cb969661a8ae2ba2153c8c8dc3c29dd73ae4dc49 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 15 Jan 2024 11:06:57 +0100 Subject: [PATCH 11/26] have to commit to test in goblint I think --- src/cil.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index df82347d1..f4c0f6d19 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -3941,7 +3941,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) (fun x -> text ("\"" ^ escape_string x ^ "\"")) () tmpls) ++ - (if outs = [] && ins = [] && clobs = [] then + (if outs = [] && ins = [] && clobs = [] && labels = [] then chr ':' else (text ": " @@ -3955,7 +3955,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ self#pLval () lv ++ text ")") () outs))) ++ - (if ins = [] && clobs = [] then + (if ins = [] && clobs = [] && labels = [] then nil else (text ": " @@ -3969,13 +3969,21 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ self#pExp () e ++ text ")") () ins))) ++ - (if clobs = [] then nil + (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) + (fun l -> self#pStmt () l) + () + (Util.list_map (!) labels)))) ++ unalign) ++ text (")" ^ printInstrTerminator) From 5de562b7256eeb945f21a4915ff56c82d4095b1e Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 15 Jan 2024 11:58:59 +0100 Subject: [PATCH 12/26] test --- src/cil.ml | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index f4c0f6d19..b3fcadc78 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -3931,7 +3931,27 @@ class defaultCilPrinterClass : cilPrinter = object (self) end | Block b -> align ++ self#pBlock () b | Asm(attrs, tmpls, outs, ins, clobs, labels, l) -> - (* todo: labels are ignored during printing *) + 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 @@ -3981,9 +4001,9 @@ class defaultCilPrinterClass : cilPrinter = object (self) else (text ": " ++ (docList ~sep:(chr ',' ++ break) - (fun l -> self#pStmt () l) + text () - (Util.list_map (!) labels)))) + (names_of_stmtrefs labels)))) ++ unalign) ++ text (")" ^ printInstrTerminator) From ced0532a866899fdfe23aceeaf20fb260514bfc9 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 15 Jan 2024 12:36:07 +0100 Subject: [PATCH 13/26] apparently asm goto ("nop") compiles --- src/frontc/cparser.mly | 36 +++++++++++++++++------------------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 76e8d8c2a..915ef6ee4 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -245,26 +245,24 @@ let transformOffsetOf (speclist, dtype) member = Buffer.contents buffer (* this makes sure that the labels are only allowed when goto annotation was provided *) - let checkAsm asm = - let is_some = function - | Some _ -> true - | None -> false - in - let is_none opt = not (is_some opt) in - match asm with + let checkAsm asm = + let _ = match asm with | ASM (attrs, _, details, _) -> - let _ = - match details, (List.assoc_opt "goto" attrs) with - | None, Some _ - | Some details, Some _ when is_none details.alabels -> - parse_error "expected ':' for labels list in asm goto"; - raise Parsing.Parse_error - | Some details, None when is_some details.alabels -> - parse_error "labels provided in inline asm without goto attribute"; - raise Parsing.Parse_error - | _, _ -> () - in asm - | _ -> failwith "called checkAsm with non-asm variant" + let is_some = function + | Some _ -> true + | None -> false + in + let is_none opt = not (is_some opt) in + (match details, (List.assoc_opt "goto" attrs) with + | Some details, Some _ when is_none details.alabels -> + parse_error "expected ':' for labels list in asm goto"; + raise Parsing.Parse_error + | Some details, None when is_some details.alabels -> + parse_error "labels provided in inline asm without goto attribute"; + raise Parsing.Parse_error + | _, _ -> ()) + | _ -> failwith "called checkAsm on non-ASM variant" + in asm %} From 35969c6d56f040b38e0b73db6bbceb299b3373bc Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 29 Jan 2024 17:47:28 +0100 Subject: [PATCH 14/26] to test inside analyzer --- src/frontc/cabs.ml | 2 +- src/frontc/cabs2cil.ml | 15 ++++++--------- src/frontc/cparser.mly | 39 +++++++++++++++------------------------ src/frontc/cprint.ml | 35 +++++++++++++++-------------------- test/testcil.pl | 6 ++++++ 5 files changed, 43 insertions(+), 54 deletions(-) diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index c6a318c02..12927ce9a 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -210,7 +210,7 @@ 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 *) - alabels: string list option; (* referenced labels *) + alabels: string list; (* referenced labels *) } and statement = diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 16c6bf68f..8b9090668 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6949,15 +6949,12 @@ and doStatement (s : A.statement) : chunk = ins in let labels' = - match labels with - | Some labels -> - Util.list_map (fun lname -> begin - let lref = ref dummyStmt in - addGoto lname lref; - lref - end) - labels - | None -> [] + Util.list_map (fun lname -> begin + let lref = ref dummyStmt in + addGoto lname lref; + lref + end) + labels in (tmpls, outs', ins', clobs, labels') in diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 915ef6ee4..af7a13581 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -246,23 +246,18 @@ let transformOffsetOf (speclist, dtype) member = (* this makes sure that the labels are only allowed when goto annotation was provided *) let checkAsm asm = - let _ = match asm with + (match asm with | ASM (attrs, _, details, _) -> - let is_some = function - | Some _ -> true - | None -> false - in - let is_none opt = not (is_some opt) in (match details, (List.assoc_opt "goto" attrs) with - | Some details, Some _ when is_none details.alabels -> - parse_error "expected ':' for labels list in asm goto"; + | Some details, Some _ when details.alabels = [] -> + parse_error "expected non-empty labels list in asm goto"; raise Parsing.Parse_error - | Some details, None when is_some details.alabels -> + | Some details, None when details.alabels <> [] -> parse_error "labels provided in inline asm without goto attribute"; raise Parsing.Parse_error | _, _ -> ()) - | _ -> failwith "called checkAsm on non-ASM variant" - in asm + | _ -> failwith "called checkAsm on non-ASM variant"); + asm %} @@ -1696,7 +1691,7 @@ asmoperand: ; asminputs: - /* empty */ { ([], [], None) } + /* empty */ { ([], [], []) } | COLON asmoperands asmclobber { ($2, fst $3, snd $3) } ; @@ -1706,27 +1701,23 @@ asmopname: ; asmclobber: - /* empty */ { ([], None) } -| COLON asmclobberlst asmlabels { ($2, $3) } + /* empty */ { ([], []) } +| COLON asmclobberlst asmlabellst { ($2, $3) } ; asmclobberlst: /* empty */ { [] } -| asmclobberlst_ne { $1 } +| asmclobberlst_ne { $1 } ; asmclobberlst_ne: one_string_constant { [$1] } | one_string_constant COMMA asmclobberlst_ne { $1 :: $3 } ; -asmlabels: - /* empty */ { None } -| COLON asmlabelslst { $2 } /* This is not asmlabelslst_ne because we distinguish between no labels field (None) and no labels provided (Some []) */ -; -asmlabelslst: - /* empty */ { Some [] } -| asmlabelslst_ne { Some $1 } +asmlabellst: + /* empty */ { [] } +| COLON asmlabellst_ne { $2 } ; -asmlabelslst_ne: +asmlabellst_ne: IDENT { [fst $1] } -| IDENT COMMA asmlabelslst_ne { (fst $1) :: $3 } +| IDENT COMMA asmlabellst_ne { (fst $1) :: $3 } %% diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 58cf85e45..704c62602 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -715,30 +715,25 @@ and print_statement stat = print_attributes attrs; print "("; print_list (fun () -> new_line()) print_string tlist; (* templates *) - begin - match details with - | None -> () + begin + match details with + | None -> () | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; alabels = labels } -> print ":"; space (); print_commas false print_asm_operand outs; - let labels_exist = match labels with Some _ -> true | None -> false in - if ins <> [] || clobs <> [] || labels_exist then begin - print ":"; space (); - print_commas false print_asm_operand ins; - if clobs <> [] || labels_exist then begin - print ":"; space (); + if ins <> [] || clobs <> [] || labels <> [] then begin + print ":"; space (); + print_commas false print_asm_operand ins; + if clobs <> [] || labels <> [] then begin + print ":"; space (); print_commas false print_string clobs; - if labels_exist then - match labels with - | Some [] -> () - | Some labels -> - print ":"; space (); - print_commas false print labels - | None -> () - end; - end - end; - print ");" + if labels <> [] then + print ":"; space (); + print_commas false print labels + end; + end; + end; + print ");"; end; new_line () diff --git a/test/testcil.pl b/test/testcil.pl index a33e9af7a..46ce5341b 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -180,6 +180,12 @@ sub addToGroup { addTest("test/asm4 _GNUCC=1"); addTest("test/asm_emptyclobberallowed _GNUCC=1"); addTest("testobj/asm5 _GNUCC=1"); +addTest("test/asm_goto1"); +addTestFail("test/asm_goto2", "expected non-empty labels list in asm goto"); +addTest("test/asm_goto3"); +addTestFail("test/asm_goto4", "labels provided in inline asm without goto attribute"); +addTestFail("test/asm_goto5", "Error: Label start not found"); +addTestFail("test/asm_goto6", "expected non-empty labels list in asm goto"); addTest("testrun/offsetof"); addTest("testrun/offsetof1"); From 5871101cb8b83a39180ae2100ae316ad07495c47 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 29 Jan 2024 17:56:48 +0100 Subject: [PATCH 15/26] testing cprint because bug I think?????????? --- src/frontc/cprint.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 704c62602..0b17d9afa 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -783,7 +783,8 @@ and print_substatement stat = and print_attribute (name,args) = if args = [] then printu name else begin - print name; + (*print name;*) + print "SHIT"; print "("; if name = "__attribute__" then print "("; (match args with [VARIABLE "aconst"] -> printu "const" From 4cb1f6b1cc4e7499827148f88a16c4a8fb489fdc Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 29 Jan 2024 18:35:21 +0100 Subject: [PATCH 16/26] ???????????????????????????????????/ --- src/frontc/cprint.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 0b17d9afa..c26e31a24 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -781,6 +781,7 @@ and print_substatement stat = ** GCC Attributes *) and print_attribute (name,args) = + print "HIHIHIHIHIHI"; if args = [] then printu name else begin (*print name;*) From cb4d68cf0f399d944b18af3e97110efc3964d8b1 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 29 Jan 2024 18:40:38 +0100 Subject: [PATCH 17/26] !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! --- src/frontc/cprint.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index c26e31a24..29bce86f0 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -781,11 +781,11 @@ and print_substatement stat = ** GCC Attributes *) and print_attribute (name,args) = - print "HIHIHIHIHIHI"; + print_endline "HIHIHIHIHIHI"; if args = [] then printu name else begin - (*print name;*) - print "SHIT"; + print_endline "SHIT"; + print name; print "("; if name = "__attribute__" then print "("; (match args with [VARIABLE "aconst"] -> printu "const" From c31ad66b87d21403514a238d0fd836a31d6977a8 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 29 Jan 2024 18:46:30 +0100 Subject: [PATCH 18/26] wtf --- src/frontc/cprint.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 29bce86f0..f6dd1fe64 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -781,10 +781,9 @@ and print_substatement stat = ** GCC Attributes *) and print_attribute (name,args) = - print_endline "HIHIHIHIHIHI"; + exit 69; if args = [] then printu name else begin - print_endline "SHIT"; print name; print "("; if name = "__attribute__" then print "("; (match args with From 1928ed71bae0e6e641343b6436e8ae157083098b Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 29 Jan 2024 19:04:14 +0100 Subject: [PATCH 19/26] I think I found the bug? --- src/cil.ml | 4 ++-- src/frontc/cprint.ml | 1 - 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index b3fcadc78..8a7e037a6 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -3962,7 +3962,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) () tmpls) ++ (if outs = [] && ins = [] && clobs = [] && labels = [] then - chr ':' + nil else (text ": " ++ (docList ~sep:(chr ',' ++ break) @@ -4358,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 -> @@ -4384,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 diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index f6dd1fe64..704c62602 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -781,7 +781,6 @@ and print_substatement stat = ** GCC Attributes *) and print_attribute (name,args) = - exit 69; if args = [] then printu name else begin print name; From bddb0762ec01430273417e5d3703ce3c7f96624f Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Mon, 29 Jan 2024 19:24:39 +0100 Subject: [PATCH 20/26] suicide commit (debugging ocaml is so fun :) :) :) :) :) --- test/small1/asm_goto1.c | 6 ++++++ test/small1/asm_goto2.c | 6 ++++++ test/small1/asm_goto3.c | 9 +++++++++ test/small1/asm_goto4.c | 10 ++++++++++ test/small1/asm_goto5.c | 8 ++++++++ test/small1/asm_goto6.c | 9 +++++++++ 6 files changed, 48 insertions(+) create mode 100644 test/small1/asm_goto1.c create mode 100644 test/small1/asm_goto2.c create mode 100644 test/small1/asm_goto3.c create mode 100644 test/small1/asm_goto4.c create mode 100644 test/small1/asm_goto5.c create mode 100644 test/small1/asm_goto6.c diff --git a/test/small1/asm_goto1.c b/test/small1/asm_goto1.c new file mode 100644 index 000000000..3a5ea3e6b --- /dev/null +++ b/test/small1/asm_goto1.c @@ -0,0 +1,6 @@ +#include "testharness.h" + +int main() { + __asm__ goto ("nop"); + SUCCESS; +} diff --git a/test/small1/asm_goto2.c b/test/small1/asm_goto2.c new file mode 100644 index 000000000..dc1e1ada0 --- /dev/null +++ b/test/small1/asm_goto2.c @@ -0,0 +1,6 @@ +#include "testharness.h" + +void code() { + asm goto ("nop" : ); + E(1); +} diff --git a/test/small1/asm_goto3.c b/test/small1/asm_goto3.c new file mode 100644 index 000000000..0e7d9b6b7 --- /dev/null +++ b/test/small1/asm_goto3.c @@ -0,0 +1,9 @@ +#include "testharness.h" + +void code() { +start: + asm goto ("nop" : : : : start, exit); +exit: + SUCCESS; +} + diff --git a/test/small1/asm_goto4.c b/test/small1/asm_goto4.c new file mode 100644 index 000000000..290d1689c --- /dev/null +++ b/test/small1/asm_goto4.c @@ -0,0 +1,10 @@ +#include "testharness.h" + +void code() { +start: + asm("nop" : : : : start, exit); +exit: + E(1); +} + + diff --git a/test/small1/asm_goto5.c b/test/small1/asm_goto5.c new file mode 100644 index 000000000..208119256 --- /dev/null +++ b/test/small1/asm_goto5.c @@ -0,0 +1,8 @@ +#include "testharness.h" + +void code() { + asm goto ("nop" : : : : start, exit); + E(1); +} + + diff --git a/test/small1/asm_goto6.c b/test/small1/asm_goto6.c new file mode 100644 index 000000000..a2cab4b2a --- /dev/null +++ b/test/small1/asm_goto6.c @@ -0,0 +1,9 @@ +#include "testharness.h" + +void code() { + asm goto ("nop" : : : :); + E(1); +} + + + From c81580c204c586f4f4da8fbacb06ce2a6ee594c4 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Tue, 30 Jan 2024 07:36:02 +0100 Subject: [PATCH 21/26] fixed the expected : before bug; todo fix label printing in cil.ml --- src/frontc/cparser.mly | 3 +++ test/small1/asm_goto1.c | 4 ++-- test/testcil.pl | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index af7a13581..0ee071f01 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -249,6 +249,9 @@ let transformOffsetOf (speclist, dtype) member = (match asm with | ASM (attrs, _, details, _) -> (match details, (List.assoc_opt "goto" attrs) with + | None, Some _ -> + parse_error "expected non-empty labels list in asm goto"; + raise Parsing.Parse_error | Some details, Some _ when details.alabels = [] -> parse_error "expected non-empty labels list in asm goto"; raise Parsing.Parse_error diff --git a/test/small1/asm_goto1.c b/test/small1/asm_goto1.c index 3a5ea3e6b..071d7db64 100644 --- a/test/small1/asm_goto1.c +++ b/test/small1/asm_goto1.c @@ -1,6 +1,6 @@ #include "testharness.h" int main() { - __asm__ goto ("nop"); - SUCCESS; + asm goto ("nop"); + E(1); } diff --git a/test/testcil.pl b/test/testcil.pl index 46ce5341b..78e0924a0 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -180,7 +180,7 @@ sub addToGroup { addTest("test/asm4 _GNUCC=1"); addTest("test/asm_emptyclobberallowed _GNUCC=1"); addTest("testobj/asm5 _GNUCC=1"); -addTest("test/asm_goto1"); +addTestFail("test/asm_goto1", "expected non-empty labels list in asm goto"); addTestFail("test/asm_goto2", "expected non-empty labels list in asm goto"); addTest("test/asm_goto3"); addTestFail("test/asm_goto4", "labels provided in inline asm without goto attribute"); From 24d806cf8f3659f63e95ee3545dee2f98369cc39 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Thu, 1 Feb 2024 14:27:53 +0100 Subject: [PATCH 22/26] commiting to test in goblint --- src/cil.ml | 2 +- src/frontc/cparser.mly | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 8a7e037a6..b966cddf3 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -838,7 +838,7 @@ and stmtkind = 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, (5) location information, and (6) the labels list for asm goto *) + registers, (6) the labels list for asm goto, and (7) location information *) (** Instructions. They may cause effects directly but may not have control diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 0ee071f01..1868277ed 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -246,17 +246,19 @@ let transformOffsetOf (speclist, dtype) member = (* this makes sure that the labels are only allowed when goto annotation was provided *) let checkAsm asm = + let labels_no_goto = "labels provided in inline asm without goto attribute" in + let goto_no_labels = "expected non-empty labels list in asm goto" in (match asm with | ASM (attrs, _, details, _) -> (match details, (List.assoc_opt "goto" attrs) with | None, Some _ -> - parse_error "expected non-empty labels list in asm goto"; + parse_error goto_no_labels; raise Parsing.Parse_error | Some details, Some _ when details.alabels = [] -> - parse_error "expected non-empty labels list in asm goto"; + parse_error goto_no_labels; raise Parsing.Parse_error | Some details, None when details.alabels <> [] -> - parse_error "labels provided in inline asm without goto attribute"; + parse_error labels_no_goto; raise Parsing.Parse_error | _, _ -> ()) | _ -> failwith "called checkAsm on non-ASM variant"); From da74c6ca9301a4d7794253295f7a618014c2f125 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Thu, 1 Feb 2024 15:09:30 +0100 Subject: [PATCH 23/26] repo is broken? --- test/small1/asm_goto6.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/small1/asm_goto6.c b/test/small1/asm_goto6.c index a2cab4b2a..6d9109993 100644 --- a/test/small1/asm_goto6.c +++ b/test/small1/asm_goto6.c @@ -1,7 +1,7 @@ #include "testharness.h" void code() { - asm goto ("nop" : : : :); + asm goto ("nop" : : : ); E(1); } From d54ca439fa731deb48ca38fecbd7c8a75165fd2b Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Wed, 7 Feb 2024 17:49:41 +0100 Subject: [PATCH 24/26] fixed bug --- src/cfg.ml | 2 +- src/check.ml | 12 +++++++++++- src/cil.ml | 6 +++++- src/rmUnused.ml | 9 ++++++++- test/small1/asm_goto3.c | 2 +- 5 files changed, 26 insertions(+), 5 deletions(-) diff --git a/src/cfg.ml b/src/cfg.ml index 31bb76115..74d3bb825 100644 --- a/src/cfg.ml +++ b/src/cfg.ml @@ -225,7 +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 _ -> addOptionSucc next (* the extra edges are added inside goblint's cfg *) + | Asm (_, _, _, _, _, labels, _) -> addOptionSucc next (* the extra edges are added inside goblint's cfg *) (*------------------------------------------------------------*) diff --git a/src/check.ml b/src/check.ml index b51affefe..66e7cc46e 100644 --- a/src/check.ml +++ b/src/check.ml @@ -809,7 +809,17 @@ and checkStmt (s: stmt) = cases; | Instr il -> List.iter checkInstr il - | Asm _ -> () (* Not yet implemented *) + | 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 *) diff --git a/src/cil.ml b/src/cil.ml index b966cddf3..76414639e 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -6550,7 +6550,11 @@ and succpred_stmt s fallthrough rlabels = | hd :: tl -> link s hd ; succpred_block b fallthrough rlabels end - | Asm _ -> trylink s fallthrough + | Asm (_, _, _, _, _, labels, _) -> + List.iter (fun label -> + link s !label + ) labels; + trylink s fallthrough let caseRangeFold (l: label list) = diff --git a/src/rmUnused.ml b/src/rmUnused.ml index 834e1b9db..8897b6311 100644 --- a/src/rmUnused.ml +++ b/src/rmUnused.ml @@ -642,7 +642,14 @@ class markUsedLabels (labelMap: (string, unit) H.t) = object (* Mark it as used *) H.replace labelMap ln (); DoChildren - + | Asm (_, _, _, _, _, labels, _) -> + List.iter (fun dest -> + let (ln, _, _), _ = labelsToKeep !dest.labels in + if ln = "" then + E.s (E.bug "rmUnused: destination of statement does not have labels"); + H.replace labelMap ln (); + ) labels; + DoChildren | _ -> DoChildren method! vexpr e = match e with diff --git a/test/small1/asm_goto3.c b/test/small1/asm_goto3.c index 0e7d9b6b7..a5d6aa433 100644 --- a/test/small1/asm_goto3.c +++ b/test/small1/asm_goto3.c @@ -1,6 +1,6 @@ #include "testharness.h" -void code() { +int main(void) { start: asm goto ("nop" : : : : start, exit); exit: From 39a4d1bd9308086474298da54c2892ae5064fbc8 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Wed, 7 Feb 2024 17:58:23 +0100 Subject: [PATCH 25/26] dummy instruction deleted, revert if necessary --- src/cil.ml | 11 +---------- src/cil.mli | 14 ++------------ 2 files changed, 3 insertions(+), 22 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 76414639e..679dba247 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -6033,11 +6033,6 @@ let typeSigAttrs = function let dExp: doc -> exp = fun d -> Const(CStr(sprint ~width:!lineLength d, No_encoding)) -(* todo: is this even used anywhere *) -(* -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)) @@ -6550,11 +6545,7 @@ and succpred_stmt s fallthrough rlabels = | hd :: tl -> link s hd ; succpred_block b fallthrough rlabels end - | Asm (_, _, _, _, _, labels, _) -> - List.iter (fun label -> - link s !label - ) labels; - trylink s fallthrough + | Asm _ -> trylink s fallthrough let caseRangeFold (l: label list) = diff --git a/src/cil.mli b/src/cil.mli index 6b7e2c63d..87d74494b 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1752,13 +1752,7 @@ val compactStmts: stmt list -> stmt list (** Returns an empty statement (of kind [Instr]) *) val mkEmptyStmt: unit -> stmt -(** A instr to serve as a placeholder *) -(* todo: maybe this can be removed? *) -(* -val dummyInstr: instr -*) - -(** A statement consisting of just [dummyInstr] *) +(** A statement to serve as a placeholder *) val dummyStmt: stmt (** Make a while loop. Can contain Break or Continue *) @@ -2654,11 +2648,7 @@ val get_stmtLoc: stmtkind -> location (** Generate an {!exp} to be used in case of errors. *) val dExp: Pretty.doc -> exp -(** Generate an {!instr} to be used in case of errors. *) -(* todo: commenting this out is probably a bad idea *) -(* -val dInstr: Pretty.doc -> location -> instr -*) +(** Generate an {!stmt} to be used in case of errors. *) val dStmt: Pretty.doc -> location -> stmt (** Generate a {!global} to be used in case of errors. *) From 2030d40a54b9f833fcdc86d3462940adcdb22f88 Mon Sep 17 00:00:00 2001 From: Simon Tietz Date: Wed, 7 Feb 2024 18:01:16 +0100 Subject: [PATCH 26/26] removed zrapp asm; revert if necessary --- src/ext/zrapp/availexps.ml | 8 -------- src/ext/zrapp/availexpslv.ml | 9 --------- src/ext/zrapp/deadcodeelim.ml | 8 -------- src/ext/zrapp/reachingdefs.ml | 9 --------- src/ext/zrapp/rmciltmps.ml | 13 ------------- 5 files changed, 47 deletions(-) diff --git a/src/ext/zrapp/availexps.ml b/src/ext/zrapp/availexps.ml index 453e7e128..48dc8a740 100644 --- a/src/ext/zrapp/availexps.ml +++ b/src/ext/zrapp/availexps.ml @@ -243,14 +243,6 @@ let eh_handle_inst i eh = (eh_kill_mem eh; eh_kill_addrof_or_global eh; eh) - (* todo: didn't find location where stmts are handled *) - (* - | Asm(_,_,_,_,_,_) -> - let _,d = UD.computeUseDefInstr i in - (UD.VS.iter (fun vi -> - eh_kill_vi eh vi) d; - eh) - *) | VarDecl _ -> raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexps, to make availexps work for programs without VLA *) (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this. *) diff --git a/src/ext/zrapp/availexpslv.ml b/src/ext/zrapp/availexpslv.ml index 73939607e..8b42eb1c1 100644 --- a/src/ext/zrapp/availexpslv.ml +++ b/src/ext/zrapp/availexpslv.ml @@ -305,15 +305,6 @@ let lvh_handle_inst i lvh = end; lvh end - (* todo *) - (* - | Asm(_,_,_,_,_,_) -> begin - let _,d = UD.computeUseDefInstr i in - UD.VS.iter (fun vi -> - lvh_kill_vi lvh vi) d; - lvh - end - *) | VarDecl _ -> raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexpslv, to make availexpslv work for programs without VLA *) (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this. *) diff --git a/src/ext/zrapp/deadcodeelim.ml b/src/ext/zrapp/deadcodeelim.ml index 72716b03d..50ab8f5d7 100644 --- a/src/ext/zrapp/deadcodeelim.ml +++ b/src/ext/zrapp/deadcodeelim.ml @@ -102,14 +102,6 @@ class usedDefsCollectorClass = object(self) method! vinst i = let handle_inst iosh i = match i with - (* todo *) - (* - | 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) - | _ -> ()) slvl - *) | Call(_,ce,el,_,_) when not (!callHasNoSideEffects i) -> List.iter (fun e -> let u = UD.computeUseExp e in diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml index d708f926c..4a953bdd6 100644 --- a/src/ext/zrapp/reachingdefs.ml +++ b/src/ext/zrapp/reachingdefs.ml @@ -270,11 +270,6 @@ 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 - (* todo *) - (* - | Asm(_,_,sll,_,_,_) -> List.exists - (function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll - *) | _ -> false) | None -> false) iihl in (match i with @@ -287,10 +282,6 @@ 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)) - (* todo *) - (* - | Asm(a,sl,slvl,sel,sl',_) -> None - *) | VarDecl _ -> None ) (* ? *) with Not_found -> diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index aeec09ea1..3809bd821 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -994,19 +994,6 @@ class unusedRemoverClass : cilVisitor = object(self) (match IH.find iioh vi.vid with None -> true | Some _ -> false) end - (* todo *) - (* - | Asm(_,_,slvlst,_,_,_) -> begin - (* make sure the outputs are in the locals list *) - List.iter (fun (_,s,lv) -> - match lv with (Var vi,_) -> - if List.mem vi cur_func.slocals - then () - else cur_func.slocals <- vi::cur_func.slocals - |_ -> ()) slvlst; - true - end - *) | _ -> true in