You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Scott Owens f298d728c5 [sledge sem] Start sketching translation correctness ... Summary: This includes a few changes and corrections to the semantics, to support the translation. This initial attempt to reason about LLVM -> llair showed three things that needed repair in the semantics, in addition to various bugs. We address them as follows. Refactor llair semantics to have only a single kind of flat value: integers that fit into specified bit widths. Operations on size values (e.g., offsets, indices and the like) can just take an integer and ignore its number of bits. Pointers can just be considered integers that fit into a certain size given by the constant pointer_size. Later on we can consider making this a parameter to the model. Change the generic memory model interface to use numbers rather than words as the generic encoding of a large value. This makes it more useful for llair where words are not used. Pay more careful attention to signed/unsigned issues. Neither LLVM nor llair have a concept of signed vs unsigned value. Instead individual operations interpret bit patterns in various ways, some of which are ambiguous in the LLVM manual. For example, since getelementpointer's indices are explicitly said to be interpreted as signed 2's complement, we should probably do the same for insertvalue and extractvalue. However it is not clear how the argument to alloca is to be interpreted. For now we assume signed. Reviewed By: jberdine Differential Revision: D17164133 fbshipit-source-id: 31a8af635		5 years ago
..
bin	[sledge] Add dbg-opt build mode	6 years ago
model	[sledge] Build models without threads support	6 years ago
semantics	[sledge sem] Start sketching translation correctness	5 years ago
src	[sledge] Revise llvm to llair translation to avoid code duplication	5 years ago
test	[sledge] Update dependencies	5 years ago
tools	[sledge] Generate and commit cli help	6 years ago
.clang-format	Add initial version of LLAIR and LLVM to LLAIR translation	7 years ago
.gitignore	[sledge] Revise test scripts	6 years ago
.ocamlformat	[sledge] Update build system, etc.	6 years ago
.ocp-indent	Add initial version of LLAIR and LLVM to LLAIR translation	7 years ago
Makefile	[sledge] Add dbg-opt build mode	6 years ago
ROADMAP.org	[sledge] Update roadmap	6 years ago
TODO.org	[sledge] Add global merge pass	5 years ago
dune	[sledge] Generate and commit cli help	6 years ago
dune-common.in	[sledge] Add dbg-opt build mode	6 years ago
dune-project	[sledge] Simplify build	6 years ago
dune-workspace	[sledge] Add dbg-opt build mode	6 years ago
llair.opam	[sledge] Upgrade base to v0.12	6 years ago
sledge-help.txt	[sledge] Explicate output flag of disassemble command	5 years ago
sledge.opam	[sledge] Add dbg-opt build mode	6 years ago