analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Support for inline assembler & `goto` instructions in inline assembler

Open WernerDrasche opened this issue 7 months ago • 8 comments

Depends on https://github.com/goblint/cil/pull/161.


The tests with annotations will come in very few days. We are sorry for this (right now still) unpolished state.

Changes in goblint-cil:

  • asm is now statement
  • goto asm is parsed

Changes in analyzer: all changes are switched off by default and can be turned on by --disable asm_is_nop

  • CFG now has edges to labels referenced in goto asm label list
  • base emits new Invalidate {lvals} event (with the lvals of the out-clobbers)
  • We tried to the best of our abilities to handle this event and/or add asm transfer functions in the analyses where necessary

WernerDrasche avatar Jan 11 '24 19:01 WernerDrasche

Depends on https://github.com/goblint/cil/pull/161.

michael-schwarz avatar Jan 12 '24 09:01 michael-schwarz

Before we can continue reviewing, can you please merge master into this and temporarily pin goblint-cil in the opam file such that the CI can run?

michael-schwarz avatar Jan 12 '24 09:01 michael-schwarz

I don't know how to tell this to use our goblint-cil repo (the pinning and downgrading procedure as described on your website only works locally I think) Edit: I think it should work now.

WernerDrasche avatar Jan 12 '24 11:01 WernerDrasche

Edit: I think it should work now.

The pin should be repeated in the goblint.opam.locked file (for the locked jobs that run on every commit), other than that you found the right way to do it.

michael-schwarz avatar Jan 12 '24 13:01 michael-schwarz

This pull request sets up GitHub code scanning for this repository. Once the scans have completed and the checks have passed, the analysis results for this pull request branch will appear on this overview. Once you merge this pull request, the 'Security' tab will show more code scanning analysis results (for example, for the default branch). Depending on your configuration and choice of analysis tool, future pull requests will be annotated with code scanning analysis results. For more information about GitHub code scanning, check out the documentation.

This message from github about the semgrep jobs confuses me: I only approved the run as usual. Not sure what this is about...

michael-schwarz avatar Jan 16 '24 23:01 michael-schwarz

What shall we do in cfgTools.ml if we can't access GobConfig?

WernerDrasche avatar Jan 17 '24 13:01 WernerDrasche

What shall we do in cfgTools.ml if we can't access GobConfig?

What does that mean? CfgTools opens GobConfig and uses get_bool in a bunch of places just fine.

sim642 avatar Jan 22 '24 12:01 sim642