GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-04 06:36:29 +03:00
Code Issues Projects Releases Wiki Activity
342 Commits 51 Branches 0 Tags 13 MiB
81aeca9e0b
Commit Graph

342 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Iavor Diatchki
81aeca9e0b Generate a fresh value for a register. 2018-03-20 19:04:00 -07:00
Iavor Diatchki
20135c91ae Generate fresh symbolic values. 2018-03-20 19:03:50 -07:00
Iavor Diatchki
4988297429 Change semantics for pointers! 
When computing pointers we don't always check that the results are valid.
Instead, we do the check whenever we use the pointers.

The reason is to support code where pointers are temporarily "bad"
but are never used that way.  For example:


   subq $10, %aex   # aex contains a pointer
Loop:
   addq $10, %aex
   ...
 2018-03-16 16:14:25 -07:00
Iavor Diatchki
1ea6792f28 Add special treatment for "aligning" pointers. 
We don't really do anything with alignment, but sometime asm code
ands pointers to align them.  For example `andq $(-64), %rsp`
aligns the pointer to a multiple of 64.

To support code like this we treat "and"-ing a pointer with a special
constant of the form 0xFFFF...FF000  (i.e., and alignment) as a subtracting
`0x0000...00XXX`  where the `XXX` is symbolic.

This looses some information (i.e., we don't know that the result is aligned).
However, it is good enough for checking memory safety, as it covers
all possible results of the alignment.
 2018-03-16 13:35:58 -07:00
Iavor Diatchki
084f6a4d2b Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-15 09:49:16 -07:00
Iavor Diatchki
6875f84971 Add implementation for vpsllq 2018-03-15 09:49:03 -07:00
Jason Dagit
e1ea0c8def Discovery: pretty instance for DiscoveryFunInfo now prints function address 2018-03-14 17:32:29 -07:00
Iavor Diatchki
f8dfc368c6 Allow reading from raw global addresses. 2018-03-14 17:20:22 -07:00
Iavor Diatchki
e967573eb0 Set false to False, not True :) 2018-03-14 15:22:19 -07:00
Iavor Diatchki
9c7070f8e6 Haddock comments fixes, thanks to Brian 2018-03-09 09:51:55 -08:00
Iavor Diatchki
53dca44cc0 Add a function to update a register assignment. 2018-03-08 17:17:14 -08:00
Iavor Diatchki
07e52b16ce Revert back to the previous order of indexing. 
This matches the Intel spec, and seems to match manual tests.
 2018-03-08 15:06:10 -08:00
Iavor Diatchki
82e1dc0ebc Add shift right for vectors. 2018-03-08 11:20:41 -08:00
Iavor Diatchki
ae54d2e078 Bit 4 seems to be for the 1st argument, and bit 0 for the snd. 2018-03-07 17:07:00 -08:00
Iavor Diatchki
89529ed7e3 Be more lenient when interpreting bogus expressions. 
Previously we were asserting that some bogus-y things don't happen.
Unfortunately, these expressions can occur in code that was not
directly written by the user (e.g., comparisons for setting various
machine flags).   To allow for that, we allow the expressions, but
give them undefined values.  So the proof will succeed only if it
does not depend on the values of these bogus comparisons.
 2018-03-07 10:22:46 -08:00
Iavor Diatchki
417c34429d Add some support for function calls. 
We basically punt, by passing-in a function to use as the implementation of
all functions.  This function is supposed to look at the IP, and
decide what to do.
 2018-03-05 16:29:15 -08:00
Iavor Diatchki
32710829f6 Use pointer addition, only when the value is not a bit-vector. 
The other version was getting confusing by the NULL pointer.
 2018-03-05 13:47:55 -08:00
Iavor Diatchki
4fa262a14c Implement MacawFresh for booleans. 2018-03-05 13:47:21 -08:00
Iavor Diatchki
357a526589 Export symbol names, so can add interpretations to them. 2018-03-02 15:35:22 -08:00
Iavor Diatchki
df32ca44aa Add a function for convenient lookup of Macaw registers in a Crucible asgn. 2018-03-02 11:35:47 -08:00
Iavor Diatchki
9071365e6d Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-01 14:36:32 -08:00
Iavor Diatchki
9094d1bd91 Improve failure message. 2018-03-01 14:36:24 -08:00
Kevin Quick
601b9def8c Merge branch 'master' of https://github.com/GaloisInc/macaw 2018-03-01 11:00:14 -08:00
Kevin Quick
e35acdcb19
Minor comment fixup. 2018-03-01 10:59:11 -08:00
Kevin Quick
84eb0a0a80 Revert "Add BVUrem App support." 
This reverts commit 6a0a59e298.

Do not want to add BVUrem because divide by zero can cause an
exception and this will greatly increase the complexity for analysis.
 2018-03-01 10:57:28 -08:00
Iavor Diatchki
da2a29b595 :Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-01 10:00:41 -08:00
Iavor Diatchki
c69349e957 Add support for global memory regions. 2018-03-01 10:00:32 -08:00
Joe Hendrix
14ab6352f5
Export elfAddrWidth 2018-02-28 09:26:10 -08:00
Joe Hendrix
a167997fc2
Merge branch 'master' of github.com:GaloisInc/macaw 2018-02-27 17:09:57 -08:00
Iavor Diatchki
2e21856afe Merge remote-tracking branch 'origin/master' into mem-model 
# Conflicts:
#	base/src/Data/Macaw/Memory/ElfLoader.hs
 2018-02-27 16:36:08 -08:00
Joe Hendrix
cf3949b170
Fix Elf X86 tests. 2018-02-27 07:37:06 -08:00
Joe Hendrix
83fa71b210
Update elf submodule 2018-02-26 14:53:08 -08:00
Joe Hendrix
9c8d7921f8
Merge branch 'master' of github.com:GaloisInc/macaw 2018-02-26 13:18:15 -08:00
Joe Hendrix
027c355001
Remove reloc hack 2018-02-26 13:04:01 -08:00
Joe Hendrix
54038b5f20
Merge branch 'mem-model' of github.com:GaloisInc/macaw into mem-model 2018-02-26 12:44:07 -08:00
Joe Hendrix
fa6f74b583
Remove unused freshVarsForRegs 2018-02-26 12:42:08 -08:00
Kevin Quick
6a0a59e298
Add BVUrem App support. 2018-02-21 20:39:57 -08:00
Iavor Diatchki
aac5a3e00f Commit the bug fix. 2018-02-21 15:24:25 -08:00
Iavor Diatchki
e3f4e0875b Bugfix and show more info when failing. 2018-02-21 15:06:18 -08:00
Iavor Diatchki
8bf523f8b1 Fill in imitted lemma 2018-02-21 09:47:53 -08:00
Joe Hendrix
cc2d09a07d
Use type synonym to clarify argument for including BSS. 2018-02-20 16:37:26 -08:00
Joe Hendrix
d8cc235368
Fix bug in loading Elf sections with no data. 2018-02-20 16:28:54 -08:00
Iavor Diatchki
6cafcdf254 More verbose failures. 2018-02-20 11:53:18 -08:00
Joe Hendrix
3e8e01f582
Merge remote-tracking branch 'public/mem-model' into mem-model 2018-02-19 16:11:47 -08:00
Joe Hendrix
0f6d030c86
Initialize variable for storing registers before use. 2018-02-19 12:48:59 -08:00
Iavor Diatchki
22fbaf9d4f Change the types of the patterns, so that matching allows us to learn the type 2018-02-15 17:03:30 -08:00
Iavor Diatchki
7c1992d991 There are only 12 FP status registers; 3 of the bits are for TOP, which is separate 2018-02-15 13:58:02 -08:00
Joe Hendrix
b20ab6664c
Provide additional control options for discovery. 2018-02-14 23:16:21 -08:00
Iavor Diatchki
b8aa67918b Assocaite global memory varaible name with its value. 2018-02-13 16:44:35 -08:00
Iavor Diatchki
470182dccb Only pass around the memory var during execution, not CFG generation. 2018-02-13 10:14:22 -08:00