Support for parsing extended assembly code including `asm goto` #161

WernerDrasche · 2024-01-11T19:54:03Z

See #81

michael-schwarz

Thank you for this PR, it is nice to see CIL (and in turn Goblint) getting support for this feature!

On top of the inline comments, here's a few remarks:

It would be good to include additional tests for the new features.
We will internally discuss what to do with zrapp
We should leave a comment somewhere that for the purpose of computing the successors, we do not consider the gotos that could happen in inline assembly so this is clear to everyone. Probably even in the documentation.

src/main.ml

src/frontc/frontc.mli

src/frontc/cprint.ml

src/ext/liveness/usedef.ml

src/ext/syntacticsearch/funcVar.ml

src/frontc/cabs.ml

michael-schwarz · 2024-01-13T18:00:18Z

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 *)


We'll have to look up zrapp again to decide what to do there.

…d_try

WernerDrasche · 2024-01-15T11:45:25Z

The main.ml changes were unintentionally forgotten testing utilities.
asmlabelslst_ne is not used in first step because we semantically distinguish between:
- labels field was provided (Some [...])
- labels field was omitted (None)
the check asm function ensures that goto attribute <=> labels field (otherwise we would need state in the parser).
it doesn't return unit because for whatever reason when I write in cparser.mly inside asm rule:
{ let asm = ASM ($1 ....) in checkAsm asm; asm } dune build fails with a syntax error in cparser.ml (can't really debug that because it's generated.
as cil cfg is only used to make the goblint cfg, we don't do anything special for the cil one
ASM a does not work for some reason (replying to the comment in email)
I don't know what to do for the dummy instruction (do we need to introduce a new instruction type for that?)

WernerDrasche · 2024-01-17T13:38:32Z

The dummyInstr can be safely deleted from cil.mli I think, as after grepping for it inside gobling-analyzer and goblint-cil no matches were found. Otherwise I have no clue on how to implement a dummy instruction using either set | vardecl | call.

michael-schwarz · 2024-01-27T11:18:49Z

src/frontc/cprint.ml

 		  print ":"; space ();
-		  print_commas false print_string clobs
+                  print_commas false print_string clobs;
+                  if labels_exist then 


Why do you still need the if here, the match should catch all cases.

src/frontc/cparser.mly

michael-schwarz · 2024-01-27T11:31:34Z

It would be good to include additional tests for the new features.

I think has not been addressed yet, if I see correctly?

src/cil.ml

michael-schwarz · 2024-01-27T11:38:31Z

The dummyInstr can be safely deleted from cil.mli I think, as after grepping for it inside gobling-analyzer and goblint-cil no matches were found. Otherwise I have no clue on how to implement a dummy instruction using either set | vardecl | call.

I think it would still be useful to keep it, as there are other users of goblint-cil. Maybe you can add a vardecl instruction for a new dummy variable? I think this is the best option.

michael-schwarz · 2024-01-27T11:39:30Z

Also, feel free to mark suggestions that you have implemented and there's nothing more to discuss as resolved, that makes it easier for us to keep track of what remains still TODO.

src/ext/syntacticsearch/funcVar.ml

sim642

There's a lot of TODOs with commented out Asm instr cases that need to be moved to Asm stmtkind cases. It's probably that they're included in some default match cases, which is why addition of Asm to stmtkind didn't cause compilation errors there.

sim642 · 2024-02-05T15:44:15Z

src/cil.mli

 (** A instr to serve as a placeholder *)
+(* todo: maybe this can be removed? *)
+(*
 val dummyInstr: instr
+*)


There isn't any no-op instr though, that's why Asm was abused for it. It's not needed by anyone in the OCaml ecosystem, so I would be fine with removing it until #145 can provide a replacement no-op instruction.

src/cil.ml

sim642 · 2024-02-05T15:50:39Z

src/cil.ml

@@ -6517,6 +6550,7 @@ and succpred_stmt s fallthrough rlabels =
                | hd :: tl -> link s hd ;
                    succpred_block b fallthrough rlabels
                end
+  | Asm _ -> trylink s fallthrough


If Asm now includes labels, shouldn't CFG construction do something with those?

sim642 · 2024-02-05T15:52:36Z

src/ext/liveness/usedef.ml

+    | Asm (_, _, outs, ins, _, _, _) ->
+        List.iter (fun (_, _, exp) -> match exp with
+          | Lval(Var v, _) -> varUsed := VS.add v !varUsed
+          | _ -> ()
+        ) ins;


Why is this different than the Asm code removed from above?

It now only adds read variables, which was a request from our supervisors if I remember correctly.

sim642 · 2024-02-05T15:57:59Z

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 (* the extra edges are added inside goblint's cfg *)


This should be done here for consistency because everything else is done here. Otherwise the support appears broken by anyone else wanting to use CIL.

It is unclear how to insert such edges, as these are only edges that are taken potentially and such a ASM block has several successors and jumps to these locations may happen at arbitrary locations within the inline assembly.

I cannot think of a general one-size-fits-all approach to include edges here, it depends on what one wants to do. In the case of Goblint over-approximating by taking any of the edges after the block has executed is what we want -- other tools might to inspect what goes on inside the assembly block or may want to underapproximate reachability etc.
I think the solution is proposed here is the best we can do.

Isn't the handling of computed goto-s already that way, though? I think CIL overapproximates their targets as well, yielding more than maybe necessary.

Following in the same spirit, it would make sense to use the overapproximation here as well. That way CIL's CFG is at least sound, i.e. it includes all possible control flows. Otherwise, it's neither sound nor complete, which is very ambiguous and unreliable. Downstream tools can always be more precise about it and exclude some targets if they want.

Are you sure? I can find no reference for this. I was under the impression that CIL assigns each label that has it's address taken an integer and then computes with these and goes to a jump table to decide where to jump to. The resulting CFG is still a "normal" CFG that corresponds to a C program.

Even if we insert these edges into the CFG, the resulting CFG would not be sound: Jumps from inline Assembly do not necessarily happen at the end or the beginning of an inline ask block. To obtain a CFG that is actually sound, we would have to look into the ASM block to insert edges appropriately, which I don't think we want to do.

Are you sure? I can find no reference for this. I was under the impression that CIL assigns each label that has it's address taken an integer and then computes with these and goes to a jump table to decide where to jump to. The resulting CFG is still a "normal" CFG that corresponds to a C program.

But that is an overapproximation! Instead of computing which exact labels a computed goto might jump to, it overapproximates that to all the labels. Of course not all computed gotos can jump to all those targets in the concrete, but that's fine: some edges are simply never used.

It would be similar for ASM gotos: have all the possible targets (which are explicitly listed by the user) in the CFG, but some of those might never be used. Without analyzing the assembly, we just cannot be any more precise.
Which exact instruction does which exact jumps is also a matter of precision, as opposed to having all of them jump to everywhere.

It was decided to have a flag to toggle this behavior on or off at Gobcon.

michael-schwarz · 2024-02-07T09:44:14Z

The currently still failing task is CC=gcc make test/asm_goto3.

michael-schwarz · 2024-02-07T09:49:32Z

The error message is

Entering directory '/home/michael/Documents/goblint-cil/cil'
cd ./small1; /home/michael/Documents/goblint-cil/cil/_build/default/test/../bin/cilly --mode=GNUCC --decil --save-temps  --strictcheck --stats --nomerge --commPrintLn \
       -c -std=gnu90 -D_GNUCC -Wall -g -ggdb -D_DEBUG -S -o asm_goto3.s asm_goto3.c
First CIL check
Timings:
TOTAL                           0.001 s
  parse                           0.000 s
  convert to CIL                  0.000 s
  printCIL                        0.000 s
Timing used
Memory statistics: total=5.10MB, max=1.02MB, minor=4.93MB, major=0.91MB, promoted=0.74MB
    minor collections=4  major collections=0 compactions=0
./asm_goto3.cil.c: In function ‘code’:
./asm_goto3.cil.c:15:30: error: expected identifier before ‘)’ token
   __asm__  goto   ("nop": : : : );
                              ^
Makefile:175: recipe for target 'test/asm_goto3' failed
make: *** [test/asm_goto3] Error 1

michael-schwarz · 2024-02-07T09:53:22Z

/* Generated by Goblint-CIL v. %%VERSION_NUM%% */
/* print_CIL_Input is false */

//#line  3 "testharness.h"
extern int printf(char const   *format  , ...) ;
//#line  12
extern void exit(int  ) ;
//#line  3 "asm_goto3.c"
void code(void) 
{ 


  {
//#line  5
  __asm__  goto   ("nop": : : : );
//#line  7
  printf((char const   *)"Success\n");
//#line  7
  exit(0);
}
}

This the produced C program.

michael-schwarz · 2024-02-07T09:57:35Z

And the error message is

gcc small1/asm_goto3.cil.c
small1/asm_goto3.cil.c: In function ‘code’:
small1/asm_goto3.cil.c:15:33: error: expected identifier before ‘)’ token
   __asm__  goto   ("nop": : : : );
                                 ^

Simon Tietz added 7 commits November 16, 2023 17:44

support for asm goto; untested but compiles

3ff22e8

intermidiary commit, so that everyone has same type definition

a76f439

todo: move all asm instr matches to stmt matches

f1e3be5

ich hab absolut keinen bock mehr

26cc002

proposal to solve dInstr problem

d01d6ec

why goblint no work???

d0dcf8c

normal gobint-cil main.exe works but from gobint --justcil doesn't

7e5435d

michael-schwarz requested review from michael-schwarz and jerhard January 12, 2024 09:50

michael-schwarz added enhancement c11 labels Jan 12, 2024

michael-schwarz mentioned this pull request Jan 12, 2024

Support for inline assembler & goto instructions in inline assembler goblint/analyzer#1326

Open

michael-schwarz linked an issue Jan 12, 2024 that may be closed by this pull request

Support for asm goto #81

Open

michael-schwarz changed the title ~~practical-asm~~ Support for parsing extended assembly code including asm goto Jan 13, 2024

michael-schwarz requested changes Jan 13, 2024

View reviewed changes

michael-schwarz added this to the 2.0.4 milestone Jan 13, 2024

Simon Tietz and others added 7 commits January 14, 2024 12:33

fixed most complaints; (dummy instruction still todo)

a339860

Update cparser.mly

7236437

Update cparser.mly

8037c21

have to commit to test in goblint I think

cb96966

test

5de562b

Merge branch 'second_try' of github.com:N0W0RK/goblint-cil into secon…

9e02615

…d_try

apparently asm goto ("nop") compiles

ced0532

michael-schwarz reviewed Jan 27, 2024

View reviewed changes

src/frontc/cparser.mly Outdated Show resolved Hide resolved

michael-schwarz reviewed Jan 27, 2024

View reviewed changes

src/frontc/cparser.mly Outdated Show resolved Hide resolved

michael-schwarz reviewed Jan 27, 2024

View reviewed changes

src/cil.ml Outdated Show resolved Hide resolved

michael-schwarz reviewed Jan 27, 2024

View reviewed changes

src/ext/syntacticsearch/funcVar.ml Show resolved Hide resolved

Simon Tietz added 10 commits January 29, 2024 17:47

to test inside analyzer

35969c6

testing cprint because bug I think??????????

5871101

???????????????????????????????????/

4cb1f6b

!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

cb4d68c

wtf

c31ad66

I think I found the bug?

1928ed7

suicide commit (debugging ocaml is so fun :) :) :) :) :)

bddb076

fixed the expected : before bug; todo fix label printing in cil.ml

c81580c

commiting to test in goblint

24d806c

repo is broken?

da74c6c

sim642 self-requested a review February 5, 2024 15:39

sim642 requested changes Feb 5, 2024

View reviewed changes

Simon Tietz added 3 commits February 7, 2024 17:49

fixed bug

d54ca43

dummy instruction deleted, revert if necessary

39a4d1b

removed zrapp asm; revert if necessary

2030d40

michael-schwarz mentioned this pull request Feb 10, 2024

Add parsing support for 'asm goto' #150

Closed

sim642 modified the milestones: 2.0.4, 2.0.5 Jul 24, 2024

jerhard self-assigned this Jul 30, 2024

sim642 modified the milestones: 2.0.5, 2.0.6 Nov 25, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for parsing extended assembly code including `asm goto` #161

Support for parsing extended assembly code including `asm goto` #161

WernerDrasche commented Jan 11, 2024 •

edited by michael-schwarz

Loading

michael-schwarz left a comment

michael-schwarz Jan 13, 2024

WernerDrasche commented Jan 15, 2024

WernerDrasche commented Jan 17, 2024

michael-schwarz Jan 27, 2024

michael-schwarz commented Jan 27, 2024

michael-schwarz commented Jan 27, 2024

michael-schwarz commented Jan 27, 2024

sim642 left a comment

sim642 Feb 5, 2024

sim642 Feb 5, 2024

michael-schwarz Feb 12, 2024

sim642 Feb 5, 2024

WernerDrasche Feb 6, 2024

sim642 Feb 5, 2024

michael-schwarz Feb 12, 2024

sim642 Feb 12, 2024

michael-schwarz Feb 13, 2024

sim642 Feb 13, 2024

michael-schwarz Feb 13, 2024

michael-schwarz commented Feb 7, 2024

michael-schwarz commented Feb 7, 2024

michael-schwarz commented Feb 7, 2024

michael-schwarz commented Feb 7, 2024

Support for parsing extended assembly code including asm goto #161

Are you sure you want to change the base?

Support for parsing extended assembly code including asm goto #161

Conversation

WernerDrasche commented Jan 11, 2024 • edited by michael-schwarz Loading

michael-schwarz left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

WernerDrasche commented Jan 15, 2024

WernerDrasche commented Jan 17, 2024

Choose a reason for hiding this comment

michael-schwarz commented Jan 27, 2024

michael-schwarz commented Jan 27, 2024

michael-schwarz commented Jan 27, 2024

sim642 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michael-schwarz commented Feb 7, 2024

michael-schwarz commented Feb 7, 2024

michael-schwarz commented Feb 7, 2024

michael-schwarz commented Feb 7, 2024

Support for parsing extended assembly code including `asm goto` #161

Support for parsing extended assembly code including `asm goto` #161

WernerDrasche commented Jan 11, 2024 •

edited by michael-schwarz

Loading