95 Commits (851fb3267bb42b760bb8051c2bad2b0c56609ccb)

Author SHA1 Message Date
Josh Berdine 4920cce2f3 [sledge] Interpret negative bounds as unbounded
4 years ago
Josh Berdine f52f9a09ca [sledge] Rename Dom to Domain
4 years ago
Josh Berdine 716c207095 [sledge] Move analysis config options from Domain_intf to Control_intf
4 years ago
Josh Berdine 45156d5901 [sledge] Parameterize Control.Make over the scheduler queue
4 years ago
Josh Berdine 20a6eda491 [sledge] Revise type of Domain join operation, it is not partial
4 years ago
Josh Berdine 7817a87e32 [sledge] Support stopping on first report in release mode
4 years ago
Josh Berdine 631eacd71f [sledge] Add explicit type for Alarms
4 years ago
Josh Berdine d5cc42a7fd [sledge] Do not disable backtrace reporting in non-debug builds
4 years ago
Josh Berdine 3e5b4c8183 [sledge] Make tracing more explicit by including module names
4 years ago
Josh Berdine f322d92cba [sledge] Add nonsupport for preallocated operand bundles
4 years ago
Josh Berdine 94395d9bec [sledge] Add support for ScalableVector type
4 years ago
Josh Berdine 55813164dc [sledge] Add support for Freeze instruction
4 years ago
Josh Berdine 6095771e57 [sledge] Add support for BFloat type
4 years ago
Josh Berdine 5316e64230 [sledge] Add nonsupport for CallBr instruction
4 years ago
Josh Berdine de0b4e764c [sledge] Add support for FNeg instruction
4 years ago
Josh Berdine aeca13145a [sledge] Update operand index of Invoke callee
4 years ago
Josh Berdine 38eb6aa8d0 [sledge] Add memtrace support
4 years ago
Josh Berdine 8d1743bf27 [sledge] Make reading config file more robust
4 years ago
Josh Berdine 585237aec1 [sledge] Remove functionality depending on Llvm_linker.link_in
4 years ago
Josh Berdine 6b9b16b077 [sledge] Drop calls to llvm.dbg.label
4 years ago
Josh Berdine 018c738499 [sledge] Make type arg of Exp.conditional non-optional
4 years ago
Josh Berdine eb4a01ce8d [sledge] Change args of Loc.mk from optional to explicit options
4 years ago
Josh Berdine 9ee705bb88 [sledge] Resolve match-on-mutable-state-prevent-uncurry warnings
4 years ago
Josh Berdine 65f8b48aac [sledge] Check type of arg of Resume the same as param of LandingPad
4 years ago
Josh Berdine 40fe8a8bc3 [sledge] Avoid calling Llvm.is_declaration on formal parameters
4 years ago
Josh Berdine 5a81118e14 [sledge] Fix bug in translation of ExtractElement InsertElement instructions
4 years ago
Josh Berdine 37d68c654e [sledge] Add script to link bitcode using gllvm
4 years ago
Josh Berdine 86298e078f [sledge] Print only function name when warning of ignored variadic arguments
4 years ago
Josh Berdine 96b8558b08 [sledge] Simplify Var by combining `program` and `identified` variables
4 years ago
Josh Berdine 3af760ee40 [sledge] Minor improvement to Frontend.cleanup
4 years ago
Josh Berdine 0534623a63 [sledge] Add unique int ids to Llair registers
4 years ago
Josh Berdine 6010ec45b2 [sledge] Do not consume names for non-call void instructions
4 years ago
Josh Berdine 19a237c730 [sledge] Name trampoline blocks using source block instead of instr
4 years ago
Josh Berdine aaf0921d86 [sledge] Do not regenerate symbol name when updating loc in Frontend
4 years ago
Josh Berdine 5c5a1cc581 [sledge] Add support for dumping and replaying solver queries
4 years ago
Josh Berdine 11c8ba21be [sledge] Allow more flexibility in Trace.trace breaking
4 years ago
Josh Berdine 1e4e650dec [sledge] Change execution options from a record to a module
4 years ago
Josh Berdine 453068fa53 [sledge] Revise Control flow exploration algorithm
4 years ago
Josh Berdine 481774c115 [sledge] Model operator new[](unsigned long)
4 years ago
Josh Berdine 16a9b9f7d2 [sledge] Fix translation of alloca
4 years ago
Josh Berdine 2726079a63 [sledge] Handle whether to follow exceptional control flow at model compilation
4 years ago
Josh Berdine c9185ae607 [sledge] Add __llair_unreachable intrinsic for use in model code
4 years ago
Josh Berdine 4605f505ce [sledge] Strengthen dynamic resolution of indirect calls
4 years ago
Josh Berdine 5c5126474e [sledge] Statically resolve known function calls
4 years ago
Josh Berdine 9e3ca541e8 [sledge] Revise name generation for return blocks of void-returning functions
4 years ago
Josh Berdine c346c5ec7f [sledge] Convert memset, memcpy, and memmov to intrinsics
4 years ago
Josh Berdine 6e5e127380 [sledge] Enable translation of intrinsic instructions for llvm intrinsics
4 years ago
Josh Berdine 31744dcfbf [sledge] Remove support for intrinsic functions
4 years ago
Josh Berdine 87ee0df07d [sledge] Convert intrinsic functions to instructions
4 years ago
Josh Berdine 9a07d6a778 [sledge] Reuse the translation of instruction intrinsics for Invoke
4 years ago