GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-11 14:52:03 +03:00
Code Issues Projects Releases Wiki Activity
331 Commits 51 Branches 0 Tags 14 MiB
07e52b16ce
Commit Graph

331 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Iavor Diatchki
b5995421ea Port x86-symbolic to the new pointer representation 2018-02-12 13:27:57 -08:00
Iavor Diatchki
ad5f7ceddb Add write operation 2018-02-12 10:28:39 -08:00
Iavor Diatchki
b57483b1f8 Start on writeMem 2018-02-09 16:59:42 -08:00
Iavor Diatchki
1c07b88ae7 Implement conditional read. 2018-02-09 15:30:06 -08:00
Iavor Diatchki
3c2fdeafe4 Implement reading from memory. 2018-02-09 14:13:39 -08:00
Iavor Diatchki
c772eb31f4 Derive Show instance for Endianness 2018-02-09 14:12:57 -08:00
Iavor Diatchki
86c730043e Cleanup pointer manipulation operations. 2018-02-09 11:41:39 -08:00
Iavor Diatchki
c7bb8d87c4 More memory model. 2018-02-08 16:49:42 -08:00
Joe Hendrix
526f8c5e6f
Move additional functions to discovery; extend loading options. 2018-02-07 14:50:53 -08:00
Iavor Diatchki
561d211972 Get started on integrating the LLVM memory model. 2018-02-06 16:47:13 -08:00
Iavor Diatchki
9200b2bcdd Rename module, to avoid name class with module from macaw-x86 2018-01-31 14:41:45 -08:00