Pointer support

[sisakb]

No description provided.

[leventeBajczi]

Thanks! I'm running some regression tests now, hopefully they'll finish until tomorrow. I'll let you know what its results are. You can see a subset of the results (5 per category if I recall correctly) in the output of the workflow "Linux build-test-deploy": artifact. I hope you have permission to download this, let me know otherwise.

In the meantime, could you please add some documentations and tests to the new parts of the codebase? Don't overdo it, just enough so that a year later we'll still know which part does what; and if parts will have become faulty due to other changes. Thanks!

Testing is best done on a subproject level, i.e., in every subproject with modifications you need to add/modify some test cases to cover at least the happy path of the new code. Of course, more elaborate tests are welcome, but try and stay within a few seconds of runtime on all of the new tests, don't add multiple minutes' worth of computation to the test steps.

Also, please format the branch using the formatting guide. The easiest method now is to run docker run -v $PWD:/github/workspace ghcr.io/leventebajczi/intellij-format:latest "*.java,*.kts,*.kt" "" "./doc/ThetaIntelliJCodeStyle.xml" from the repo's directory, but later it might also be advantageous to set up IntelliJ's automatic formatting on save/commit.
The same goes for the copyright headers as well: please include the standard copyright notice with the correct year at the top of your new files. See the output of the check-copyright CI job for more info on which files are missing the header.

[leventeBajczi]

regression tests are done, and unfortunately a number of tasks became erroneous:

unreach-call

bitvector/modulus-2.yml
eca-rers2012/Problem05_label32.yml
eca-rers2012/Problem05_label36.yml
eca-rers2012/Problem05_label44.yml
eca-rers2012/Problem11_label00.yml
eca-rers2012/Problem13_label06.yml
eca-rers2012/Problem13_label24.yml
eca-rers2012/Problem14_label22.yml
eca-rers2012/Problem14_label37.yml
eca-rers2012/Problem14_label44.yml
eca-rers2012/Problem14_label54.yml
eca-rers2012/Problem15_label33.yml
eca-rers2012/Problem16_label48.yml
eca-rers2012/Problem16_label54.yml
floats-cbmc-regression/float13.yml
loops/invert_string-1.yml
loops/invert_string-3.yml
loops-crafted-1/mono-crafted_10.yml
nla-digbench-scaling/egcd2-ll_unwindbound1.yml
seq-mthreaded/pals_STARTPALS_ActiveStandby.4_2.ufo.BOUNDED-10.pals.yml
seq-mthreaded/pals_STARTPALS_ActiveStandby.4_2.ufo.UNBOUNDED.pals.yml
seq-mthreaded/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.yml
seq-mthreaded/pals_lcr-var-start-time.3.1.ufo.UNBOUNDED.pals.yml
seq-mthreaded/pals_lcr.3.1.ufo.BOUNDED-6.pals.yml
seq-mthreaded/pals_lcr.3.ufo.BOUNDED-6.pals.yml
seq-mthreaded/pals_lcr.3.ufo.UNBOUNDED.pals.yml
systemc/token_ring.04.cil-1.yml
systemc/token_ring.04.cil-2.yml
combinations/Problem05_label42+token_ring.04.cil-2.yml
combinations/Problem05_label43+token_ring.04.cil-2.yml
combinations/Problem05_label45+token_ring.04.cil-2.yml
combinations/Problem05_label46+token_ring.04.cil-2.yml
combinations/Problem05_label49+token_ring.04.cil-2.yml
combinations/pc_sfifo_1.cil-2+token_ring.03.cil-2.yml
combinations/pc_sfifo_1.cil-2+token_ring.04.cil-2.yml
combinations/pc_sfifo_2.cil-1+token_ring.02.cil-1.yml
combinations/pc_sfifo_2.cil-1+token_ring.02.cil-2.yml
combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.yml
combinations/pc_sfifo_2.cil-1+token_ring.03.cil-2.yml
combinations/pc_sfifo_3.cil+token_ring.03.cil-1.yml
combinations/pc_sfifo_3.cil+token_ring.03.cil-2.yml
hardware-verification-bv/btor2c-lazyMod.anderson.1.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.anderson.3.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.diagonal.yml
hardware-verification-bv/btor2c-lazyMod.eq_sdp_v4.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.1.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.2.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.3.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.3.prop1-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.4.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.5.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.5.prop1-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.iprotocol.7.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.lup.1.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.lup.1.prop1-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.lup.2.prop1-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.lup.3.prop1-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.lup.4.prop1-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.protocols.3.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.protocols.4.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.protocols.5.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.resistance.1.prop3-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.resistance.2.prop2-func-interl.yml
hardware-verification-bv/btor2c-lazyMod.schedule_world.1.prop1-back-serstep.yml
hardware-verification-bv/btor2c-lazyMod.sdlx.yml
hardware-verification-bv/btor2c-lazyMod.twocount32.yml
hardware-verification-bv/btor2c-lazyMod.vcegar_QF_BV_pj_icu_icctl_p2.yml
hardware-verification-bv/btor2c-lazyMod.vcegar_QF_BV_sdlx_control.yml
hardware-verification-bv/btor2c-lazyMod.vis_arrays_am2910_p2.yml
hardware-verification-bv/btor2c-lazyMod.vis_arrays_vsaR_p06.yml
hardware-verification-bv/btor2c-lazyMod.vis_arrays_vsaR_p15.yml
hardness-nfm22/hardness_loopvsstraightlinecode_25-while_file-5.yml
hardness-nfm22/hardness_operatoramount_amount10_file-15.yml
hardness-nfm22/hardness_operatoramount_amount10_file-2.yml
hardness-nfm22/hardness_operatoramount_amount10_file-43.yml
hardness-nfm22/hardness_operatoramount_amount10_file-59.yml
hardness-nfm22/hardness_operatoramount_amount25_file-5.yml
hardness-nfm22/hardness_variablewrapping_wrapper-a_file-62.yml

I think we should postpone merging this PR until these problems have been addressed. If you need the result files, let me know!

[leventeBajczi]

I have run some tests, and there are some further problems:

1. DataRace is faulty (pointers should be followed). Either throw an error when encountering pointers together with the property datarace, or follow pointers in the target calculation.
2. sv-benchmarks/c/ldv-regression/test08.c is faulty, because p=&a is transformed into p=0, which makes it UNSAT to have the statements int* p = 0; p = &a; [p != 0].

[leventeBajczi]

When encountering a pointer action, do not pass it to the solver.

[leventeBajczi]

Please reopen against master.

[leventeBajczi]

Some modifcations I'd like to see:

• Instead of modifying the code of subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtTransFunc.java, create a new TransFunc class in the xcfa subproject (-analysis, I suppose), which wraps the ExplStmtTransFunc by delegation, and has access to a pointer store. Optimally, no code outside the xcfa and frontend folders would be changed (of course, besides the new statements, if necessary).
• Would it be possible to change the new Stmts to XcfaLabels? Other frontends won't really have any use for the new statements, so I would prefer they become XcfaLabels instead (similarly to, e.g., InvokeLabel).