Valentin Robert
4fa43a439d
Show instance for MemSymbol
2024-04-08 10:06:58 -07:00
Mike S
67f36b50a4
Update .gitmodules
...
It appears that Galois took over maintenance of this repo. the submodule is being updated to reflect that and resolve docker build errors
2024-04-04 17:17:13 -04:00
Valentin Robert
1ab280b5f8
Merge pull request #373 from GaloisInc/vr/showf-floatinforepr
...
add ShowF instance for FloatInfoRepr
2024-03-18 11:16:22 -07:00
Valentin Robert
1d3f2a3331
add ShowF instance for FloatInfoRepr
2024-03-13 15:42:07 -07:00
Ryan Scott
7e1694b0ef
macaw-symbolic: Fix interval bounds in mkGlobalPointerValidityPred
...
Fixes #279 .
2024-01-24 18:50:11 -05:00
Langston Barrett
c6c48b6f8b
x86-symbolic: Format imports
2024-01-24 11:03:37 -05:00
Langston Barrett
8b90009aec
x86-symbolic: Pretty-printing of exceptions
2024-01-24 11:03:37 -05:00
Langston Barrett
50e44e138c
x86-symbolic: Add function to extract message from exceptions
2024-01-24 11:03:37 -05:00
Langston Barrett
2df9981f49
aarch32-symbolic: Export AArch32Exception
2024-01-24 11:03:37 -05:00
Langston Barrett
a02343412d
x86-symbolic: Structured exceptions for missing primitive function semantics
2024-01-23 16:39:15 -05:00
Langston Barrett
5f8300bd57
x86-symbolic: Create an exception type for missing semantics
...
This is an exception that consumers might want to catch.
2024-01-23 16:18:16 -05:00
Valentin Robert
e1d0846be7
Merge pull request #366 from GaloisInc/vr/fix-doc
...
fix incorrect documentation
2024-01-23 09:04:12 -08:00
Valentin Robert
8569727885
fix incorrect documentation
2024-01-22 18:37:11 -08:00
Andrei Stefanescu
9d8cdcc587
Add semantics for prefetch instructions. ( #365 )
2024-01-10 11:31:36 -08:00
Valentin Robert
c8a8845983
Merge pull request #364 from GaloisInc/vr/minor-cleanups
...
minor cleanups
2024-01-05 13:27:09 -08:00
Valentin Robert
f8f406df4f
minor cleanups
2024-01-05 13:26:44 -08:00
Valentin Robert
a1fa674a5a
Merge pull request #363 from GaloisInc/vr/pp-noreturnfunstatus
...
add Pretty instance for NoReturnFunStatus
2024-01-05 13:10:56 -08:00
Valentin Robert
0f2264b7c4
add Pretty instance for NoReturnFunStatus
2024-01-05 11:46:25 -08:00
Ryan Scott
aaa5ea1234
Generalize lazy memory model using HasMacawLazySimulatorState
...
This introduces a `HasMacawLazySimulatorState` data type, which provides a
"classy lens" for accessing a `MacawLazySimulatorState` within some Crucible
personality type. It also generalizes the lazy `macaw-symbolic` memory model in
`Data.Macaw.Symbolic.Memory.Lazy` to be polymorphic over
`HasMacawLazySimulatorState` instances. The upside is that it is now possible
to use the lazy memory model at other personality types besides just
`MacawLazySimulatorState`, making it much easier to extend the memory model.
Because there is a `HasMacawLazySimulatorState` instance for
`MacawLazySimulatorState`, existing code that uses `MacawLazySimulatorState`
should continue to compile without changes.
Fixes #357 .
2023-12-12 15:29:48 -05:00
Valentin Robert
7d840065be
Merge pull request #356 from GaloisInc/vr/archaddrwidth
...
favor `ArchAddrWidth` over `RegAddrWidth (ArchReg ...)`
2023-12-11 12:48:58 -08:00
Valentin Robert
d2f7028e2d
favor ArchAddrWidth and ArchSegmentOff type synonyms
2023-12-11 09:53:53 -05:00
Langston Barrett
35b5fcd732
Bump Crucible submodule, adapt to crucible-syntax changes
2023-12-08 09:46:20 -05:00
Valentin Robert
9e09fc86e7
Merge pull request #353 from GaloisInc/vr/remove-extension
...
remove unused extension
2023-12-07 12:27:35 -08:00
Valentin Robert
822ea653c6
Merge pull request #354 from GaloisInc/vr/derive-show
...
derive `Show` for `FunctionArgAnalysisFailure`
2023-12-07 12:27:11 -08:00
Valentin Robert
e27f909867
Merge pull request #352 from GaloisInc/vr/typo
...
fix typo
2023-12-07 10:16:27 -08:00
Valentin Robert
b87da1501b
derive Show for FunArgAnalysisFailure
...
It's sometimes practical to debug the map of analysis failures by
printing them all out, but we don't seem to have any facilities for
printing them.
2023-12-07 09:09:19 -08:00
Valentin Robert
dacd1562f0
remove unused extension
2023-12-07 09:08:52 -08:00
Valentin Robert
9197aaa38f
fix typo
2023-12-06 21:21:53 -08:00
Ryan Scott
c2c2a3d6bd
macaw-symbolic: Implement MacawFreshSymbolic for all macaw Types
...
Rather than `error`ing, we now generate fresh constants for all possible
`macaw` `Type`s that are supplied to the `MacawFreshSymbolic` operation.
Fixes #301 .
2023-11-17 17:08:34 -05:00
Ryan Scott
2e49eb5351
Merge pull request #350 from GaloisInc/macaw-ppc-pic-ip-addresses
...
`macaw-ppc`: Don't assume absolute IP addresses when decoding
2023-11-14 15:02:45 -06:00
Ryan Scott
ca64b56808
macaw-{aarch32,ppc}: Remove vestigial InstructionAtUnmappedAddr error types
...
Now that `macaw-aarch32` and `macaw-ppc` properly handle position-independent
code, the `InstructionAtUnmappedAddr` error (which could only be thrown if an
IP address was found in position-independent code) is never thrown. Let's
delete it.
2023-11-14 13:03:52 -05:00
Ryan Scott
b12b049455
macaw-ppc: Don't assume absolute IP addresses when decoding
...
`macaw-ppc` was previously assuming that addresses are absolute, which is not
true for position independent executables. Extracting the offset from the
address is sufficient for our purposes here (note that taking the offset from
the `MemSegmentOffset` would not be right, as that offset is relative to the
segment start).
This is the exact same issue that was noticed in
37d8029c00
2023-11-14 12:58:01 -05:00
Ryan Scott
0c6872ad1d
Merge pull request #348 from GaloisInc/elf-edit-T35
...
`macaw-base`: Resolve PPC{32,64} relocations
2023-11-14 06:29:49 -06:00
Ryan Scott
2fb4ab4291
macaw-base: Resolve PPC{32,64} relocations
...
This builds on top of the work in
https://github.com/GaloisInc/elf-edit/pull/41 . For now, I only add support for
a select few relocation types, leaving the rest as future work.
2023-11-03 11:38:11 -04:00
Langston Barrett
7a70ce9840
Merge pull request #345 from GaloisInc/lb/syntax
...
macaw-symbolic-syntax: Concrete syntax for macaw-symbolic CFGs
2023-11-03 09:15:12 -04:00
Langston Barrett
eb68a3fa64
Bump crucible submodule
2023-11-02 17:09:03 -04:00
Langston Barrett
836298bcc6
symbolic-syntax: Remove documentation of type aliases
...
These are no longer part of the base syntax, but can be added on.
2023-11-02 17:06:06 -04:00
Langston Barrett
191c016565
symbolic-syntax: Clarify comments
2023-11-02 16:42:27 -04:00
Langston Barrett
0b9c4730d8
symbolic-syntax: Remove fresh-vec
...
It's not part of the Macaw syntax, but rather an operation that's useful
when hand-writing CFGs. This should instead be supported by parser extensions
downstream.
2023-11-02 16:39:24 -04:00
Langston Barrett
8be115c859
symbolic-syntax: Explain the utility of bv-typed-literal
2023-11-02 16:37:58 -04:00
Langston Barrett
5fc17a1c03
symbolic-syntax: make-null -> pointer-make-null
2023-11-02 16:36:08 -04:00
Langston Barrett
de4789b73b
symbolic-syntax: Reuse type alias parsers from crucible-llvm-syntax
2023-11-02 16:34:01 -04:00
Langston Barrett
7b38e4b6ce
symbolic-syntax: Fix README backticks
...
Co-authored-by: Ryan Scott <rscott@galois.com>
2023-11-02 10:56:51 -04:00
Langston Barrett
19f0a578fc
symbolic-syntax: Add a test that exercises all the operations
2023-11-02 09:11:04 -04:00
Langston Barrett
a2ac7f4300
macaw-symbolic-syntax: Concrete syntax for macaw-symbolic CFGs
...
This code was ported from ambient-verifier.
2023-11-01 17:19:13 -04:00
Valentin Robert
e05a9db243
Merge pull request #342 from GaloisInc/vr/fix-doc
...
fix incorrect documentation
2023-09-11 10:26:31 -07:00
Valentin Robert
28d3c587fc
fix incorrect documentation
2023-09-08 10:17:15 -07:00
Valentin Robert
4ad9984185
Merge pull request #341 from GaloisInc/vr/block-invariants-docstrings
...
fix BlockInvariants docstrings
2023-09-08 08:42:00 -07:00
Valentin Robert
4cfed47b7b
fix BlockInvariants docstrings
...
The alignment was all wonky, and one field was not documented.
2023-09-07 16:57:30 -07:00
Ryan Scott
299c227a77
CI: Test GHC 9.2.8, 9.4.5, 9.6.2
2023-08-21 08:16:10 -04:00
