GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2025-01-04 04:12:02 +03:00
Code Issues Projects Releases Wiki Activity
354 Commits 52 Branches 0 Tags 14 MiB
3736ce137a
Commit Graph

354 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Iavor Diatchki
3736ce137a Remove some warnings. 2018-03-23 14:37:08 -07:00
Iavor Diatchki
f0d50049db Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-23 14:34:44 -07:00
Iavor Diatchki
2f070f99f0 Setup LLVM intrinsics, and make sure to use the config as the one for the sym. 2018-03-23 14:34:38 -07:00
Aaron Tomb
e33ecf3e84 Fix build with GHC 8.4.1 2018-03-23 14:09:28 -07:00
Iavor Diatchki
79a4cdf39e Add support for forcing allocation of fresh bits (as opposed to pointer/bits) 2018-03-22 13:11:22 -07:00
Iavor Diatchki
cf34388d41 Don't validate pointer after alignment. 
We validate only when using pointers.
 2018-03-22 13:10:58 -07:00
Iavor Diatchki
d3d5f39ebb Change YMM patterns to just use Word8 directly. 
Simpler, not clear that the additional abstraction was useful.
 2018-03-21 16:14:59 -07:00
Iavor Diatchki
21ffae1ebe Prefix fresh names with macaw 
Hopefully, this will avoid clashes with keywords.
 2018-03-21 16:14:31 -07:00
Iavor Diatchki
36e6c8f7b9 Export GlobalMap 2018-03-20 19:56:52 -07:00
Iavor Diatchki
cec6f52e0f Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-20 19:04:05 -07:00
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
Joe Hendrix
77f518a9ab
Merge pull request #3 from robdockins/master 
Minor update to track crucible API
 2018-03-20 15:03:29 -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
Rob Dockins
4a4b9d7a8a Minor update to track crucible API 2018-03-15 17:21:42 -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