search

UQ-PAC / BASIL

Apache License 2.0
8 stars 0 forks source link

Data Structure Analysis #222

Open sadrabt opened 2 months ago

sadrabt commented 2 months ago

includes symbolic access analysis and a reaching definitions analysis that works slightly differently from the one already implemented. (registers changed by a procedure call are defined by the call instruction)

l-kent commented 2 months ago

I'm a bit confused by the commit history here - some of Yousif's commits that are not ready to merge in yet have been included, but then later reverted? Is there a neater way to do things than that?

l-kent commented 2 months ago

It'll take some time to get across all the details of this, so detailed comments would really help to make it easier to understand.

One thing that makes the code more difficult to follow at the moment is the widespread use of tuples - is it possible that replacing those with case classes would make sense?

l-kent commented 1 week ago

https://github.com/UQ-PAC/BASIL/blob/c806362d0f7e867968c39808c2bc559eb06543cd/src/main/scala/analysis/solvers/IDESolver.scala#L105

The call to exitToEntry here causes a ClassCastException: class ir.Procedure cannot be cast to class ir.IndirectCall for the tests correct/syscall/clang_O2:GTIRB and correct/syscall/gcc_O2:GTIRB when run with the analysis on.

l-kent commented 5 days ago

Is there an option to output the .dot files you demonstrated today? I can't find that anywhere, and when I attempted to manually add that functionality, none of the nodes in the .dot files I got it to output had any contents beyond a number.

Rather than using .dot graphs though, it would be more useful for debugging if it could print the mappings in plain text, in an order that made sense - relating back to the order of statements in the IR?

sadrabt commented 5 days ago

Is there an option to output the .dot files you demonstrated today? I can't find that anywhere, and when I attempted to manually add that functionality, none of the nodes in the .dot files I got it to output had any contents beyond a number.

I pushed my most recent changes on, now you should be able to produce dot graphs from a DSG using writeToFile(dsg.toDot, "test.dot")

Rather than using .dot graphs though, it would be more useful for debugging if it could print the mappings in plain text, in an order that made sense - relating back to the order of statements in the IR?

Yeah this makes sense, I'll work on outputting text format

l-kent commented 5 days ago

That's pretty much what I added in, but the DOT graph it produced didn't have anything in the nodes except their number, it didn't contain all the information that was in the graph you demonstrated today.

l-kent commented 5 days ago

mainTopDown.txt This is one of the outputs I got, for src\test\correct\jumptable\clang\jumptable.adt

l-kent commented 5 days ago

Thanks, that works.

The DSA seems to run into problems with overlapping accesses. The following is from src\test\correct\jumptable\clang\jumptable.bir with comments added:

000003fe: R8 := 0x10000
// 0x10DC0 contains a pointer to the procedure add_two
// 0x10DC8 contains a pointer to the procedure add_six
00000404: R8 := R8 + 0xDC0
// loading 128 bits from 0x10DC0 loads both the 64-bit pointer at address 0x10DC0
// and the 64-bit pointer at address 0x10DC8 to V0, concatenated together
0000040b: V0 := mem[R8, el]:u128
// storing V0 to the stack stores the pointer to add_two at R31 + 0x10 and the pointer to add_six at R31 + 0x18
00000413: mem := mem with [R31 + 0x10, el]:u128 <- V0
0000041a: R8 := mem[R8 + 0x10, el]:u64
00000422: mem := mem with [R31 + 0x20, el]:u64 <- R8
00000429: R8 := mem[R31 + 0x10, el]:u64
0000042e: R30 := 0x7D0
00000431: call R8 with return %00000433

00000433:
// the DSA says that R8 at this assignment points to node 434 which is empty, but it should point to add_six
// or alternatively some node that represents that the pointers to add_two and add_six were loaded together and stored on the stack together
00000438: R8 := mem[R31 + 0x18, el]:u64
0000043d: R30 := 0x7D8
00000440: call R8 with return %00000442
l-kent commented 5 days ago

Flags like CF, VF, etc. are inherently 1-bit values and can't point to anything, I don't think there is a reason to include them in this?

l-kent commented 4 days ago

In general it would be preferable if you do not use the examples folder for any tests - the existing contents of the examples folder are very out of date and we really should delete most of them. Any new test files should be put in their own folder in the tests folder - move the /unsafe_pointer_arithmetic and /interproc_pointer_arithmetic folders from /examples to /src/test/dsa.