pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
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.
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '0c3e568fa4'
${ noResults }
infer_clone/sledge/semantics/llvm_to_llair_propScript.sml

1556 lines
59 KiB
Raw Normal View History Unescape

[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
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
(* Proofs about llvm to llair translation *)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
open HolKernel boolLib bossLib Parse lcsymtacs;
[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
open listTheory arithmeticTheory pred_setTheory finite_mapTheory wordsTheory integer_wordTheory;
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
open optionTheory rich_listTheory pathTheory;
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
open settingsTheory miscTheory memory_modelTheory;
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
open llvmTheory llvm_propTheory llvm_ssaTheory llairTheory llair_propTheory llvm_to_llairTheory;
[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
new_theory "llvm_to_llair_prop";
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
set_grammar_ancestry ["llvm", "llair", "llair_prop", "llvm_to_llair", "llvm_ssa"];
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
[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
numLib.prefer_num ();
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
Definition translate_trace_def:
(translate_trace gmap Tau = Tau) ∧
(translate_trace gmap Error = Error) ∧
(translate_trace gmap (Exit i) = (Exit i)) ∧
(translate_trace gmap (W gv bytes) = W (translate_glob_var gmap gv) bytes)
End
[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
Inductive v_rel:
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
(∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) llair$pointer_size))) ∧
[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
(∀w. v_rel (FlatV (W1V w)) (FlatV (IntV (w2i w) 1))) ∧
(∀w. v_rel (FlatV (W8V w)) (FlatV (IntV (w2i w) 8))) ∧
(∀w. v_rel (FlatV (W32V w)) (FlatV (IntV (w2i w) 32))) ∧
(∀w. v_rel (FlatV (W64V w)) (FlatV (IntV (w2i w) 64))) ∧
(∀vs1 vs2.
list_rel v_rel vs1 vs2
⇒
v_rel (AggV vs1) (AggV vs2))
End
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Definition take_to_call_def:
(take_to_call [] = []) ∧
(take_to_call (i::is) =
if terminator i ∨ is_call i then [i] else i :: take_to_call is)
End
Definition dest_llair_lab_def:
dest_llair_lab (Lab_name f b) = (f, b)
End
Inductive pc_rel:
(* LLVM side points to a normal instruction *)
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
(∀prog emap ip bp d b idx b' prev_i fname gmap.
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
(* Both are valid pointers to blocks in the same function *)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
dest_fn ip.f = fst (dest_llair_lab bp) ∧
alookup prog ip.f = Some d ∧
alookup d.blocks ip.b = Some b ∧
ip.i = Offset idx ∧
idx < length b.body ∧
get_block (translate_prog prog) bp b' ∧
(* The LLVM side is at the start of a block, or immediately following a
* call, which will also start a new block in llair *)
(ip.i ≠ Offset 0 ⇒ get_instr prog (ip with i := Offset (idx - 1)) (Inl prev_i) ∧ is_call prev_i) ∧
ip.f = Fn fname ∧
(∃regs_to_keep.
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
b' = fst (translate_instrs fname gmap emap regs_to_keep (take_to_call (drop idx b.body))))
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
pc_rel prog gmap emap ip bp) ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(* If the LLVM side points to phi instructions, the llair side
* should point to a block generated from them *)
(∀prog emap ip bp b from_l phis.
get_instr prog ip (Inr (from_l, phis)) ∧
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
(* We should have just jumped here from block from_l *)
(∃d b. alookup prog ip.f = Some d ∧
alookup d.blocks from_l = Some b ∧
ip.b ∈ set (map Some (instr_to_labs (last b.body)))) ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(* TODO: constrain b to be generated from the phis *)
get_block (translate_prog prog) bp b
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
pc_rel prog gmap emap ip bp)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
End
Definition untranslate_reg_def:
untranslate_reg (Var_name x t) = Reg x
End
(* Define when an LLVM state is related to a llair one.
* Parameterised on a map for locals relating LLVM registers to llair
[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
* expressions that compute the value in that register. This corresponds to part
* of the translation's state.
*)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Definition mem_state_rel_def:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap (s:llvm$state) (s':llair$state) ⇔
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
(* Live LLVM registers are mapped and have a related value in the emap
* (after evaluating) *)
(∀r. r ∈ live prog s.ip ⇒
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(∃v v' e.
[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
v_rel v.value v' ∧
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
flookup s.locals r = Some v ∧
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
flookup emap r = Some e ∧ eval_exp s' e v' ∧
(* Each register used in e is dominated by an assignment to that
* register for the entire live range of r. *)
(∀ip1 r'. ip1.f = s.ip.f ∧ r ∈ live prog ip1 ∧ r' ∈ exp_uses e ⇒
∃ip2. untranslate_reg r' ∈ assigns prog ip2 ∧ dominates prog ip2 ip1))) ∧
reachable prog s.ip ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
fmap_rel (\(_,n) n'. w2n n = n')
s.globals
(s'.glob_addrs f_o translate_glob_var gmap) ∧
heap_ok s.heap ∧
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
erase_tags s.heap = s'.heap ∧
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
s.status = s'.status
[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
End
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(* Define when an LLVM state is related to a llair one
* Parameterised on a map for locals relating LLVM registers to llair
* expressions that compute the value in that register. This corresponds to part
* of the translation's state.
*)
Definition state_rel_def:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap (s:llvm$state) (s':llair$state) ⇔
(s.status = Partial ⇒ pc_rel prog gmap emap s.ip s'.bp) ∧
mem_state_rel prog gmap emap s s'
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
End
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
Theorem mem_state_ignore_bp[simp]:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s s' b.
mem_state_rel prog gmap emap s (s' with bp := b) ⇔
mem_state_rel prog gmap emap s s'
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Proof
rw [mem_state_rel_def] >> eq_tac >> rw [] >>
first_x_assum drule >> rw [] >>
`eval_exp (s' with bp := b) e v' ⇔ eval_exp s' e v'`
by (irule eval_exp_ignores >> rw []) >>
metis_tac []
QED
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
Triviality lemma:
((s:llair$state) with status := Complete code).locals = s.locals
Proof
rw []
QED
Theorem mem_state_rel_exited:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s s' code.
mem_state_rel prog gmap emap s s'
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap (s with status := Complete code) (s' with status := Complete code)
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
Proof
rw [mem_state_rel_def] >>
metis_tac [eval_exp_ignores, lemma]
QED
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Theorem mem_state_rel_no_update:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s1 s1' v res_v r i i'.
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
assigns prog s1.ip = {} ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap s1 s1' ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
i ∈ next_ips prog s1.ip
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap (s1 with ip := i) s1'
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Proof
rw [mem_state_rel_def]
>- (
first_x_assum (qspec_then `r` mp_tac) >> simp [Once live_gen_kill, PULL_EXISTS] >>
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
metis_tac [next_ips_same_func])
>- metis_tac [next_ips_reachable]
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
QED
Theorem mem_state_rel_update:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s1 s1' v res_v r e i.
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
is_ssa prog ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
assigns prog s1.ip = {r} ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap s1 s1' ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
eval_exp s1' e res_v ∧
v_rel v.value res_v ∧
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
i ∈ next_ips prog s1.ip ∧
(∀r_use. r_use ∈ exp_uses e ⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∃r_tmp. r_use ∈ exp_uses (translate_arg gmap emap (Variable r_tmp)) ∧ r_tmp ∈ live prog s1.ip)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap (emap |+ (r, e))
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(s1 with <|ip := i; locals := s1.locals |+ (r, v) |>)
s1'
Proof
rw [mem_state_rel_def]
>- (
rw [FLOOKUP_UPDATE]
>- (
HINT_EXISTS_TAC >> rw [] >>
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
first_x_assum drule >> rw [] >>
first_x_assum drule >> rw [] >>
fs [exp_uses_def, translate_arg_def] >>
pop_assum (qspec_then `s1.ip` mp_tac) >> simp [] >>
disch_then drule >> rw [] >>
`dominates prog s1.ip ip1`
by (
irule ssa_dominates_live_range_lem >> rw [] >>
metis_tac [next_ips_same_func]) >>
metis_tac [dominates_trans]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
`i.f = s1.ip.f` by metis_tac [next_ips_same_func] >> simp [] >>
first_x_assum irule >>
simp [Once live_gen_kill, PULL_EXISTS, METIS_PROVE [] ``x ∨ y ⇔ (~y ⇒ x)``] >>
metis_tac [])
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
>- metis_tac [next_ips_reachable]
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
QED
Theorem mem_state_rel_update_keep:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s1 s1' v res_v r i ty.
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
is_ssa prog ∧
assigns prog s1.ip = {r} ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap s1 s1' ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
v_rel v.value res_v ∧
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
reachable prog s1.ip ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
i ∈ next_ips prog s1.ip
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap (emap |+ (r, Var (translate_reg r ty)))
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(s1 with <|ip := i; locals := s1.locals |+ (r, v)|>)
(s1' with locals := s1'.locals |+ (translate_reg r ty, res_v))
Proof
rw [mem_state_rel_def]
>- (
rw [FLOOKUP_UPDATE]
>- (
simp [Once eval_exp_cases] >>
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
qexists_tac `res_v` >> rw [exp_uses_def] >>
rw [FLOOKUP_UPDATE] >>
Cases_on `r` >> simp [translate_reg_def, untranslate_reg_def] >>
`∃ip. ip.f = ip1.f ∧ Reg s ∈ uses prog ip`
by (
qabbrev_tac `x = (ip1.f = i.f)` >>
fs [live_def] >> qexists_tac `last (ip1::path')` >> rw [] >>
irule good_path_same_func >>
qexists_tac `ip1::path'` >> rw [MEM_LAST] >>
metis_tac []) >>
metis_tac [ssa_dominates_live_range]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
first_x_assum (qspec_then `r'` mp_tac) >>
simp [Once live_gen_kill, PULL_EXISTS] >>
impl_tac >> rw []
>- metis_tac [] >>
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
ntac 3 HINT_EXISTS_TAC >> rw []
>- (
`DRESTRICT (s1' with locals := s1'.locals |+ (translate_reg r ty,res_v)).locals (exp_uses e) =
DRESTRICT s1'.locals (exp_uses e)`
suffices_by metis_tac [eval_exp_ignores_unused] >>
rw [] >>
first_x_assum (qspecl_then [`s1.ip`, `translate_reg r ty`] mp_tac) >> simp [Once live_gen_kill] >>
impl_tac >- metis_tac [] >> rw [] >>
`ip2 = s1.ip`
by (
fs [is_ssa_def, EXTENSION, IN_DEF] >>
Cases_on `r` >> fs [translate_reg_def, untranslate_reg_def] >>
metis_tac [reachable_dominates_same_func]) >>
metis_tac [dominates_irrefl])
>- (
first_x_assum irule >> rw [] >>
metis_tac [next_ips_same_func]))
>- metis_tac [next_ips_reachable]
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
QED
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
Triviality lemma:
((s:llair$state) with heap := h).locals = s.locals
Proof
rw []
QED
Theorem mem_state_rel_heap_update:
∀prog gmap emap s s' h h'.
mem_state_rel prog gmap emap s s' ∧
heap_ok h ∧
erase_tags h = erase_tags h'
⇒
mem_state_rel prog gmap emap (s with heap := h) (s' with heap := h')
Proof
rw [mem_state_rel_def, erase_tags_def]
>- metis_tac [eval_exp_ignores, lemma] >>
rw [heap_component_equality] >>
fs [fmap_eq_flookup, FLOOKUP_o_f] >> rw [] >>
first_x_assum (qspec_then `x` mp_tac) >>
BasicProvers.EVERY_CASE_TAC >> rw [] >>
Cases_on `x'` >> Cases_on `x''` >> fs []
QED
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Theorem v_rel_bytes:
∀v v'. v_rel v v' ⇒ llvm_value_to_bytes v = llair_value_to_bytes v'
[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
Proof
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
ho_match_mp_tac v_rel_ind >>
rw [v_rel_cases, llvm_value_to_bytes_def, llair_value_to_bytes_def] >>
rw [value_to_bytes_def, llvmTheory.unconvert_value_def, w2n_i2n,
llairTheory.unconvert_value_def, llairTheory.pointer_size_def,
llvmTheory.pointer_size_def] >>
pop_assum mp_tac >>
qid_spec_tac `vs1` >>
Induct_on `vs2` >> rw [] >> rw []
[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
QED
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
Theorem bytes_v_rel_lem:
(∀f s bs t.
f = (λn t w. convert_value t w) ∧
s = type_to_shape t ∧
first_class_type t
⇒
(quotient_pair$### v_rel $=)
(bytes_to_value f s bs)
(bytes_to_value (λn t w. convert_value t w) (type_to_shape (translate_ty t)) bs)) ∧
(∀f n s bs t.
f = (λn t w. convert_value t w) ∧
s = type_to_shape t ∧
first_class_type t
⇒
(quotient_pair$### (list_rel v_rel) $=)
(read_array f n s bs)
(read_array (λn t w. convert_value t w) n (type_to_shape (translate_ty t)) bs)) ∧
(∀f ss bs ts.
f = (λn t w. convert_value t w) ∧
ss = map type_to_shape ts ∧
every first_class_type ts
⇒
(quotient_pair$### (list_rel v_rel) $=)
(read_str f ss bs)
(read_str (λn t w. convert_value t w) (map (type_to_shape o translate_ty) ts) bs))
Proof
ho_match_mp_tac bytes_to_value_ind >>
rw [llvmTheory.type_to_shape_def, translate_ty_def, type_to_shape_def,
sizeof_def, llvmTheory.sizeof_def, bytes_to_value_def, pointer_size_def,
convert_value_def, llvmTheory.convert_value_def, quotient_pairTheory.PAIR_REL]
>- (
Cases_on `t'` >>
fs [llvmTheory.type_to_shape_def, llvmTheory.sizeof_def, llvmTheory.first_class_type_def] >>
TRY (Cases_on `s`) >>
rw [llvmTheory.sizeof_def, le_read_num_def, translate_size_def,
convert_value_def, llvmTheory.convert_value_def, translate_ty_def,
type_to_shape_def, bytes_to_value_def, sizeof_def, llvmTheory.sizeof_def] >>
simp [v_rel_cases] >> rw [word_0_w2i, w2i_1] >>
fs [pointer_size_def, llvmTheory.pointer_size_def] >>
qmatch_goalsub_abbrev_tac `l2n 256 l` >>
qmatch_goalsub_abbrev_tac `n2i n dim` >>
`n < 2 ** dim`
by (
qspecl_then [`l`, `256`] mp_tac numposrepTheory.l2n_lt >>
rw [] >>
`256 ** length l ≤ 2 ** dim` suffices_by decide_tac >>
`256 = 2 ** 8` by rw [] >>
full_simp_tac bool_ss [] >>
REWRITE_TAC [GSYM EXP_EXP_MULT] >>
rw [EXP_BASE_LE_MONO] >>
unabbrev_all_tac >> rw []) >>
metis_tac [w2i_n2w, dimword_def, dimindex_8, dimindex_32, dimindex_64])
>- (
Cases_on `t` >>
fs [llvmTheory.type_to_shape_def, llvmTheory.sizeof_def, llvmTheory.first_class_type_def] >>
rw [pairTheory.PAIR_MAP] >>
pairarg_tac >> fs [type_to_shape_def, translate_ty_def, bytes_to_value_def] >>
first_x_assum (qspec_then `t'` mp_tac) >> simp [] >>
simp [v_rel_cases] >>
pairarg_tac >> fs [] >>
pairarg_tac >> fs [] >> rw [])
>- (
Cases_on `t` >>
fs [llvmTheory.type_to_shape_def, llvmTheory.sizeof_def, llvmTheory.first_class_type_def] >>
rw [pairTheory.PAIR_MAP] >>
fs [type_to_shape_def, translate_ty_def, bytes_to_value_def] >>
pairarg_tac >> fs [pairTheory.PAIR_MAP] >>
first_x_assum (qspec_then `l` mp_tac) >> simp [] >>
simp [v_rel_cases] >>
pairarg_tac >> fs [] >>
pairarg_tac >> fs [MAP_MAP_o] >> rw [] >> fs [ETA_THM])
>- (
rpt (pairarg_tac >> fs []) >>
first_x_assum (qspec_then `t` mp_tac) >> rw [] >>
first_x_assum (qspec_then `t` mp_tac) >> rw [])
>- (
Cases_on `ts` >> fs [bytes_to_value_def] >>
rpt (pairarg_tac >> fs []) >>
first_x_assum (qspec_then `h` mp_tac) >> simp [] >> strip_tac >>
fs [] >> rfs [] >> fs [] >>
first_x_assum (qspec_then `t` mp_tac) >> simp [] >> strip_tac >>
fs [MAP_MAP_o] >> rw [])
QED
Theorem bytes_v_rel:
∀t bs.
first_class_type t ⇒
v_rel (fst (bytes_to_llvm_value t bs))
(fst (bytes_to_llair_value (translate_ty t) bs))
Proof
rw [bytes_to_llvm_value_def, bytes_to_llair_value_def] >>
qspecl_then [`bs`, `t`] mp_tac (CONJUNCT1 (SIMP_RULE (srw_ss()) [] bytes_v_rel_lem)) >>
rw [quotient_pairTheory.PAIR_REL] >>
pairarg_tac >> fs [] >>
pairarg_tac >> fs []
QED
[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
Theorem translate_constant_correct_lem:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
(∀c s prog gmap emap s'.
mem_state_rel prog gmap emap s s'
[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
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel (eval_const s.globals c) v') ∧
(∀(cs : (ty # const) list) s prog gmap emap s'.
mem_state_rel prog gmap emap s s'
[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
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∃v'. list_rel (eval_exp s') (map (translate_const gmap o snd) cs) v' ∧ list_rel v_rel (map (eval_const s.globals o snd) cs) v') ∧
(∀(tc : ty # const) s prog gmap emap s'.
mem_state_rel prog gmap emap s s'
[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
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∃v'. eval_exp s' (translate_const gmap (snd tc)) v' ∧ v_rel (eval_const s.globals (snd tc)) v')
[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
Proof
ho_match_mp_tac const_induction >> rw [translate_const_def] >>
simp [Once eval_exp_cases, eval_const_def]
>- (
Cases_on `s` >> simp [eval_const_def, translate_size_def, v_rel_cases] >>
metis_tac [truncate_2comp_i2w_w2i, dimindex_1, dimindex_8, dimindex_32, dimindex_64])
>- (
simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
metis_tac [])
>- (
simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
metis_tac [])
[sledge sem] Improve and unify treatment of Exit Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago
(* TODO: unimplemented stuff *)
[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
>- cheat
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
>- (
fs [mem_state_rel_def, fmap_rel_OPTREL_FLOOKUP] >>
CASE_TAC >> fs [] >> first_x_assum (qspec_then `g` mp_tac) >> rw [] >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
rename1 `option_rel _ _ opt` >> Cases_on `opt` >> fs [OPTREL_def] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
(* TODO: false at the moment, need to work out the llair story on globals *)
cheat)
(* TODO: unimplemented stuff *)
[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
>- cheat
>- cheat
QED
Theorem translate_constant_correct:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀c s prog gmap emap s' g.
mem_state_rel prog gmap emap s s'
[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
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel (eval_const s.globals c) v'
[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
Proof
metis_tac [translate_constant_correct_lem]
QED
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
(* TODO: This isn't true, since the translation turns LLVM globals into llair
* locals *)
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
Theorem translate_const_no_reg[simp]:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀gmap c. r ∉ exp_uses (translate_const gmap c)
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
Proof
ho_match_mp_tac translate_const_ind >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
rw [translate_const_def, exp_uses_def, MEM_MAP, METIS_PROVE [] ``x ∨ y ⇔ (~x ⇒ y)``]
>- (pairarg_tac >> fs [] >> metis_tac [])
>- (pairarg_tac >> fs [] >> metis_tac [])
>- cheat
>- cheat
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
QED
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Theorem translate_arg_correct:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀s a v prog gmap emap s'.
mem_state_rel prog gmap emap s s' ∧
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
eval s a = Some v ∧
arg_to_regs a ⊆ live prog s.ip
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∃v'. eval_exp s' (translate_arg gmap emap a) v' ∧ v_rel v.value v'
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Proof
Cases_on `a` >> rw [eval_def, translate_arg_def] >> rw []
>- metis_tac [translate_constant_correct] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
CASE_TAC >> fs [PULL_EXISTS, mem_state_rel_def, arg_to_regs_def] >>
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
res_tac >> rfs [] >> metis_tac []
QED
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Theorem is_allocated_mem_state_rel:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s1 s1'.
mem_state_rel prog gmap emap s1 s1'
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
⇒
(∀i. is_allocated i s1.heap ⇔ is_allocated i s1'.heap)
Proof
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
rw [mem_state_rel_def, is_allocated_def, erase_tags_def] >>
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
pop_assum mp_tac >> pop_assum (mp_tac o GSYM) >> rw []
QED
[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
Theorem restricted_i2w_11:
∀i (w:'a word). INT_MIN (:'a) ≤ i ∧ i ≤ INT_MAX (:'a) ⇒ (i2w i : 'a word) = i2w (w2i w) ⇒ i = w2i w
Proof
rw [i2w_def]
>- (
Cases_on `n2w (Num (-i)) = INT_MINw` >>
rw [w2i_neg, w2i_INT_MINw] >>
fs [word_L_def] >>
`?j. 0 ≤ j ∧ i = -j` by intLib.COOPER_TAC >>
rw [] >>
fs [] >>
`INT_MIN (:'a) < dimword (:'a)` by metis_tac [INT_MIN_LT_DIMWORD] >>
`Num j MOD dimword (:'a) = Num j`
by (irule LESS_MOD >> intLib.COOPER_TAC) >>
fs []
>- intLib.COOPER_TAC
>- (
`Num j < INT_MIN (:'a)` by intLib.COOPER_TAC >>
fs [w2i_n2w_pos, integerTheory.INT_OF_NUM]))
>- (
fs [GSYM INT_MAX, INT_MAX_def] >>
`Num i < INT_MIN (:'a)` by intLib.COOPER_TAC >>
rw [w2i_n2w_pos, integerTheory.INT_OF_NUM] >>
intLib.COOPER_TAC)
QED
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Theorem translate_sub_correct:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s1 s1' nsw nuw ty v1 v1' v2 v2' e2' e1' result.
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
do_sub nuw nsw v1 v2 ty = Some result ∧
eval_exp s1' e1' v1' ∧
v_rel v1.value v1' ∧
eval_exp s1' e2' v2' ∧
v_rel v2.value v2'
⇒
∃v3'.
eval_exp s1' (Sub (translate_ty ty) e1' e2') v3' ∧
v_rel result.value v3'
Proof
rw [] >>
simp [Once eval_exp_cases] >>
fs [do_sub_def] >> rw [] >>
rfs [v_rel_cases] >> rw [] >> fs [] >>
BasicProvers.EVERY_CASE_TAC >> fs [PULL_EXISTS, translate_ty_def, translate_size_def] >>
pairarg_tac >> fs [] >>
fs [pairTheory.PAIR_MAP, wordsTheory.FST_ADD_WITH_CARRY] >>
rw [] >>
qmatch_goalsub_abbrev_tac `w2i (-1w * w1 + w2)` >>
qexists_tac `w2i w2` >> qexists_tac `w2i w1` >> simp [] >>
unabbrev_all_tac >> rw []
>- (
irule restricted_i2w_11 >> simp [word_sub_i2w] >>
`dimindex (:1) = 1` by rw [] >>
drule truncate_2comp_i2w_w2i >>
rw [word_sub_i2w] >>
metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:1)``,
SIMP_CONV (srw_ss()) [] ``INT_MAX (:1)``])
>- (
irule restricted_i2w_11 >> simp [word_sub_i2w] >>
`dimindex (:8) = 8` by rw [] >>
drule truncate_2comp_i2w_w2i >>
rw [word_sub_i2w] >>
metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:8)``,
SIMP_CONV (srw_ss()) [] ``INT_MAX (:8)``])
>- (
irule restricted_i2w_11 >> simp [word_sub_i2w] >>
`dimindex (:32) = 32` by rw [] >>
drule truncate_2comp_i2w_w2i >>
rw [word_sub_i2w] >>
metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:32)``,
SIMP_CONV (srw_ss()) [] ``INT_MAX (:32)``])
>- (
irule restricted_i2w_11 >> simp [word_sub_i2w] >>
`dimindex (:64) = 64` by rw [] >>
drule truncate_2comp_i2w_w2i >>
rw [word_sub_i2w] >>
metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:64)``,
SIMP_CONV (srw_ss()) [] ``INT_MAX (:64)``])
QED
[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
Theorem translate_extract_correct:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s1 s1' a v v1' e1' cs ns result.
mem_state_rel prog gmap emap s1 s1' ∧
[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
map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
extract_value v ns = Some result ∧
eval_exp s1' e1' v1' ∧
v_rel v v1'
⇒
∃v2'.
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
eval_exp s1' (foldl (λe c. Select e (translate_const gmap c)) e1' cs) v2' ∧
[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
v_rel result v2'
Proof
Induct_on `cs` >> rw [] >> fs [extract_value_def]
>- metis_tac [] >>
first_x_assum irule >>
Cases_on `ns` >> fs [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
qmatch_goalsub_rename_tac `translate_const gmap c` >>
`?v2'. eval_exp s1' (translate_const gmap c) v2' ∧ v_rel (eval_const s1.globals c) v2'`
[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
by metis_tac [translate_constant_correct] >>
Cases_on `v` >> fs [extract_value_def] >>
qpat_x_assum `v_rel (AggV _) _` mp_tac >>
simp [Once v_rel_cases] >> rw [] >>
simp [Once eval_exp_cases, PULL_EXISTS] >>
fs [LIST_REL_EL_EQN] >>
qmatch_assum_rename_tac `_ = map Some is` >>
Cases_on `eval_const s1.globals c` >> fs [signed_v_to_num_def, signed_v_to_int_def] >> rw [] >>
`?i. v2' = FlatV i` by fs [v_rel_cases] >> fs [] >>
qmatch_assum_rename_tac `option_join _ = Some x` >>
`?size. i = IntV (&x) size` suffices_by metis_tac [] >> rw [] >>
qpat_x_assum `v_rel _ _` mp_tac >>
simp [v_rel_cases] >> rw [] >> fs [signed_v_to_int_def] >> rw [] >>
intLib.COOPER_TAC
QED
Theorem translate_update_correct:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀prog gmap emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
mem_state_rel prog gmap emap s1 s1' ∧
[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
map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
insert_value v1 v2 ns = Some result ∧
eval_exp s1' e1' v1' ∧
v_rel v1 v1' ∧
eval_exp s1' e2' v2' ∧
v_rel v2 v2'
⇒
∃v3'.
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
eval_exp s1' (translate_updatevalue gmap e1' e2' cs) v3' ∧
[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
v_rel result v3'
Proof
Induct_on `cs` >> rw [] >> fs [insert_value_def, translate_updatevalue_def]
>- metis_tac [] >>
simp [Once eval_exp_cases, PULL_EXISTS] >>
Cases_on `ns` >> fs [] >>
Cases_on `v1` >> fs [insert_value_def] >>
rename [`insert_value (el x _) _ ns`] >>
Cases_on `insert_value (el x l) v2 ns` >> fs [] >> rw [] >>
qpat_x_assum `v_rel (AggV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
simp [v_rel_cases] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
qmatch_goalsub_rename_tac `translate_const gmap c` >>
[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
qexists_tac `vs2` >> simp [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
`?v4'. eval_exp s1' (translate_const gmap c) v4' ∧ v_rel (eval_const s1.globals c) v4'`
[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
by metis_tac [translate_constant_correct] >>
`?idx_size. v4' = FlatV (IntV (&x) idx_size)`
by (
pop_assum mp_tac >> simp [Once v_rel_cases] >>
rw [] >> fs [signed_v_to_num_def, signed_v_to_int_def] >>
intLib.COOPER_TAC) >>
first_x_assum drule >>
disch_then drule >>
disch_then drule >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
disch_then (qspecl_then [`el x vs2`, `v2'`, `e2'`, `Select e1' (translate_const gmap c)`] mp_tac) >>
[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
simp [Once eval_exp_cases] >>
metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
QED
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
val trunc_thms =
LIST_CONJ (map (fn x => SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a`` |-> x] truncate_2comp_i2w_w2i))
[``:1``, ``:8``, ``:32``, ``:64``]);
val i2n_thms =
LIST_CONJ (map (fn x => SIMP_RULE (srw_ss()) [] (INST_TYPE [``:'a`` |-> x] (GSYM w2n_i2n)))
[``:1``, ``:8``, ``:32``, ``:64``]);
Theorem translate_cast_correct:
∀prog gmap emap s1' cop ty v1 v1' e1' result t2.
do_cast cop v1.value ty = Some result ∧
eval_exp s1' e1' v1' ∧
v_rel v1.value v1' ∧
(cop = Inttoptr ⇒ ∃t. ty = PtrT t)
⇒
∃v3'.
[sledge sem] Add proof of bit cast implementation Summary: Add some theorems establishing the correspondence between the implementation of the Convert operation in OCaml and the definition of Convert in the semantics. Essentially, the OCaml version is in terms of extracting certain ranges of bits, whereas the semantics is in terms of integer arithmetic (addition, modulus, and exponentiation) Reviewed By: jberdine Differential Revision: D18113878 fbshipit-source-id: c318596d0
5 years ago
eval_exp s1' (Convert (cop ≠ Sext) (translate_ty ty) t2 e1') v3' ∧
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
v_rel result v3'
Proof
rw [] >> simp [Once eval_exp_cases, PULL_EXISTS, Once v_rel_cases] >>
Cases_on `cop ≠ Sext`
>- (
Cases_on `cop` >> fs [do_cast_def] >> rw [] >>
BasicProvers.EVERY_CASE_TAC >> fs [] >>
fs [OPTION_JOIN_EQ_SOME, w64_cast_some, signed_v_to_int_some,
unsigned_v_to_num_some, mk_ptr_some] >>
rw [sizeof_bits_def, translate_ty_def, translate_size_def] >>
rfs [] >> fs [v_rel_cases] >>
HINT_EXISTS_TAC >>
rw [w2w_n2w, trunc_thms, i2n_thms, w2w_def, pointer_size_def]) >>
fs [do_cast_def, OPTION_JOIN_EQ_SOME, PULL_EXISTS, w64_cast_some,
translate_ty_def, sizeof_bits_def, signed_v_to_int_some,
translate_size_def] >>
rfs [v_rel_cases, w2w_i2w] >> rw [trunc_thms] >>
qmatch_assum_abbrev_tac `eval_exp _ _ (FlatV (IntV i s))` >>
qexists_tac `s` >> qexists_tac `i` >> rw [] >>
unabbrev_all_tac >> rw [] >>
rw [i2w_w2i_extend, WORD_w2w_OVER_MUL, WORD_ALL_BITS] >>
Cases_on `w2w w : word1` >> rw [] >> fs [dimword_1] >>
Cases_on `n` >> rw [] >> fs [] >>
Cases_on `n'` >> rw [] >> fs []
QED
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
Theorem prog_ok_nonterm:
∀prog i ip.
prog_ok prog ∧ get_instr prog ip (Inl i) ∧ ¬terminator i ⇒ inc_pc ip ∈ next_ips prog ip
Proof
rw [next_ips_cases, IN_DEF, get_instr_cases, PULL_EXISTS] >>
`terminator (last b.body) ∧ b.body ≠ []` by metis_tac [prog_ok_def] >>
Cases_on `length b.body = idx + 1`
>- (
drule LAST_EL >>
rw [] >> fs [DECIDE ``PRE (x + 1) = x``]) >>
Cases_on `el idx b.body` >>
fs [instr_next_ips_def, terminator_def] >>
rw [EXISTS_OR_THM, inc_pc_def, inc_bip_def]
QED
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
Theorem const_idx_uses[simp]:
∀cs gmap e.
exp_uses (foldl (λe c. Select e (translate_const gmap c)) e cs) = exp_uses e
Proof
Induct_on `cs` >> rw [exp_uses_def] >>
rw [translate_const_no_reg, EXTENSION]
QED
Theorem exp_uses_trans_upd_val[simp]:
∀cs gmap e1 e2. exp_uses (translate_updatevalue gmap e1 e2 cs) =
(if cs = [] then {} else exp_uses e1) ∪ exp_uses e2
Proof
Induct_on `cs` >> rw [exp_uses_def, translate_updatevalue_def] >>
rw [translate_const_no_reg, EXTENSION] >>
metis_tac []
QED
(* TODO: identify some lemmas to cut down on the duplicated proof in the very
* similar cases *)
[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
Theorem translate_instr_to_exp_correct:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀gmap emap instr r t s1 s1' s2 prog l.
[sledge sem] Improve and unify treatment of Exit Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago
is_ssa prog ∧ prog_ok prog ∧
[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
classify_instr instr = Exp r t ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap s1 s1' ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
get_instr prog s1.ip (Inl instr) ∧
step_instr prog s1 instr l s2 ⇒
∃pv emap' s2'.
l = Tau ∧
s2.ip = inc_pc s1.ip ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap' s2 s2' ∧
(r ∉ regs_to_keep ⇒ s1' = s2' ∧ emap' = emap |+ (r, translate_instr_to_exp gmap emap instr)) ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(r ∈ regs_to_keep ⇒
emap' = emap |+ (r,Var (translate_reg r t)) ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
step_inst s1' (Move [(translate_reg r t, translate_instr_to_exp gmap emap instr)]) Tau s2')
[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
Proof
recInduct translate_instr_to_exp_ind >>
simp [translate_instr_to_exp_def, classify_instr_def] >>
conj_tac
>- ( (* Sub *)
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
rw [step_instr_cases, get_instr_cases, update_result_def] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
qpat_x_assum `Sub _ _ _ _ _ _ = el _ _` (assume_tac o GSYM) >>
`bigunion (image arg_to_regs {a1; a2}) ⊆ live prog s1.ip`
by (
simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
instr_uses_def] >>
metis_tac []) >>
fs [] >>
[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
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
disch_then drule >> disch_then drule >>
[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
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
disch_then drule >> disch_then drule >> rw [] >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
drule translate_sub_correct >>
simp [] >>
disch_then (qspecl_then [`s1'`, `v'`, `v''`] mp_tac) >> simp [] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
disch_then drule >> disch_then drule >> rw [] >>
rename1 `eval_exp _ (Sub _ _ _) res_v` >>
rename1 `r ∈ _` >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
simp [inc_pc_def, llvmTheory.inc_pc_def] >>
`assigns prog s1.ip = {r}`
by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
`reachable prog s1.ip` by fs [mem_state_rel_def] >>
`s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
by (
drule prog_ok_nonterm >>
simp [get_instr_cases, PULL_EXISTS] >>
ntac 3 (disch_then drule) >>
simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Cases_on `r ∈ regs_to_keep` >> rw []
[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
>- (
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
simp [step_inst_cases, PULL_EXISTS] >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
qexists_tac `res_v` >> rw [] >>
rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
irule mem_state_rel_update_keep >> rw [])
[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
>- (
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
irule mem_state_rel_update >> rw []
>- (
fs [exp_uses_def]
>| [Cases_on `a1`, Cases_on `a2`] >>
fs [translate_arg_def] >>
rename1 `flookup _ r_tmp` >>
qexists_tac `r_tmp` >> rw [] >>
simp [Once live_gen_kill] >> disj2_tac >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
metis_tac [])) >>
[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
conj_tac
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
>- ( (* Extractvalue *)
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
rw [step_instr_cases, get_instr_cases, update_result_def] >>
qpat_x_assum `Extractvalue _ _ _ = el _ _` (assume_tac o GSYM) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
`arg_to_regs a ⊆ live prog s1.ip`
by (
simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
instr_uses_def]) >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
drule translate_extract_correct >> rpt (disch_then drule) >>
drule translate_arg_correct >> disch_then drule >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
simp [] >> strip_tac >>
disch_then drule >> simp [] >> rw [] >>
rename1 `eval_exp _ (foldl _ _ _) res_v` >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
rw [inc_pc_def, llvmTheory.inc_pc_def] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
rename1 `r ∈ _` >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
`assigns prog s1.ip = {r}`
by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
`reachable prog s1.ip` by fs [mem_state_rel_def] >>
`s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
by (
drule prog_ok_nonterm >>
simp [get_instr_cases, PULL_EXISTS] >>
ntac 3 (disch_then drule) >>
simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Cases_on `r ∈ regs_to_keep` >> rw []
>- (
simp [step_inst_cases, PULL_EXISTS] >>
qexists_tac `res_v` >> rw [] >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
irule mem_state_rel_update_keep >> rw [])
>- (
irule mem_state_rel_update >> rw []
>- (
Cases_on `a` >>
fs [translate_arg_def] >>
rename1 `flookup _ r_tmp` >>
qexists_tac `r_tmp` >> rw [] >>
simp [Once live_gen_kill] >> disj2_tac >>
simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
metis_tac [])) >>
[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
conj_tac
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
>- ( (* Updatevalue *)
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
rw [step_instr_cases, get_instr_cases, update_result_def] >>
qpat_x_assum `Insertvalue _ _ _ _ = el _ _` (assume_tac o GSYM) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
`arg_to_regs a1 ⊆ live prog s1.ip ∧
arg_to_regs a2 ⊆ live prog s1.ip`
by (
ONCE_REWRITE_TAC [live_gen_kill] >>
simp [SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
instr_uses_def]) >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
drule translate_update_correct >> rpt (disch_then drule) >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >>
simp [] >> strip_tac >> strip_tac >>
disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >>
disch_then drule >> disch_then drule >>
rw [] >>
rename1 `eval_exp _ (translate_updatevalue _ _ _ _) res_v` >>
rw [inc_pc_def, llvmTheory.inc_pc_def] >>
rename1 `r ∈ _` >>
`assigns prog s1.ip = {r}`
by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
`reachable prog s1.ip` by fs [mem_state_rel_def] >>
`s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
by (
drule prog_ok_nonterm >>
simp [get_instr_cases, PULL_EXISTS] >>
ntac 3 (disch_then drule) >>
simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
Cases_on `r ∈ regs_to_keep` >> rw []
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
>- (
simp [step_inst_cases, PULL_EXISTS] >>
qexists_tac `res_v` >> rw [] >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
irule mem_state_rel_update_keep >> rw [])
>- (
irule mem_state_rel_update >> strip_tac
>- (
Cases_on `a1` >> Cases_on `a2` >>
rw [translate_arg_def] >>
rename1 `flookup _ r_tmp` >>
qexists_tac `r_tmp` >> rw [] >>
simp [Once live_gen_kill] >> disj2_tac >>
simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
rw [] >> metis_tac [] ))>>
conj_tac
>- ( (* Cast *)
rw [step_instr_cases, get_instr_cases, update_result_def] >>
qpat_x_assum `Cast _ _ _ _ = el _ _` (assume_tac o GSYM) >>
`arg_to_regs a1 ⊆ live prog s1.ip`
by (
simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
instr_uses_def] >>
metis_tac []) >>
fs [] >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >> disch_then drule >> rw [] >>
drule translate_cast_correct >> ntac 2 (disch_then drule) >>
simp [] >>
disch_then (qspec_then `translate_ty t1` mp_tac) >>
impl_tac
(* TODO: prog_ok should enforce that the type is consistent *)
>- cheat >>
rw [] >>
rename1 `eval_exp _ (Convert _ _ _ _) res_v` >>
rw [inc_pc_def, llvmTheory.inc_pc_def] >>
rename1 `r ∈ _` >>
`assigns prog s1.ip = {r}`
by rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def] >>
`reachable prog s1.ip` by fs [mem_state_rel_def] >>
`s1.ip with i := inc_bip (Offset idx) ∈ next_ips prog s1.ip`
by (
drule prog_ok_nonterm >>
simp [get_instr_cases, PULL_EXISTS] >>
ntac 3 (disch_then drule) >>
simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def]) >>
Cases_on `r ∈ regs_to_keep` >> rw []
>- (
simp [step_inst_cases, PULL_EXISTS] >>
qexists_tac `res_v` >> rw [] >>
rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
irule mem_state_rel_update_keep >> rw [])
>- (
irule mem_state_rel_update >> rw []
>- (
fs [exp_uses_def] >> Cases_on `a1` >> fs [translate_arg_def] >>
rename1 `flookup _ r_tmp` >>
qexists_tac `r_tmp` >> rw [] >>
simp [Once live_gen_kill] >> disj2_tac >>
simp [uses_cases, IN_DEF, get_instr_cases, instr_uses_def, arg_to_regs_def]) >>
metis_tac [])) >>
(* TODO: unimplemented instruction translations *)
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
cheat
QED
Triviality eval_exp_help:
(s1 with heap := h).locals = s1.locals
Proof
rw []
QED
Theorem translate_instr_to_inst_correct:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀gmap emap instr r t s1 s1' s2 prog l.
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
classify_instr instr = Non_exp ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
prog_ok prog ∧ is_ssa prog ∧
mem_state_rel prog gmap emap s1 s1' ∧
get_instr prog s1.ip (Inl instr) ∧
step_instr prog s1 instr l s2
⇒
∃pv s2'.
s2.ip = inc_pc s1.ip ∧
mem_state_rel prog gmap (extend_emap_non_exp emap instr) s2 s2' ∧
step_inst s1' (translate_instr_to_inst gmap emap instr) (translate_trace gmap l) s2'
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Proof
rw [step_instr_cases] >>
fs [classify_instr_def, translate_instr_to_inst_def]
>- ( (* Load *)
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
fs [step_inst_cases, get_instr_cases, PULL_EXISTS] >>
qpat_x_assum `Load _ _ _ = el _ _` (assume_tac o GSYM) >>
`arg_to_regs a1 ⊆ live prog s1.ip`
by (
simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
instr_uses_def] >>
metis_tac []) >>
fs [] >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >> disch_then drule >> rw [] >>
qpat_x_assum `v_rel (FlatV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
`∃n. r = Reg n` by (Cases_on `r` >> metis_tac []) >>
qexists_tac `n` >> qexists_tac `translate_ty t` >>
HINT_EXISTS_TAC >> rw [] >>
qexists_tac `freeable` >> rw [translate_trace_def]
>- rw [inc_pc_def, llvmTheory.inc_pc_def, update_result_def]
>- (
simp [GSYM translate_reg_def, llvmTheory.inc_pc_def, update_result_def,
update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST,
extend_emap_non_exp_def] >>
irule mem_state_rel_update_keep >>
rw []
>- rw [assigns_cases, IN_DEF, EXTENSION, get_instr_cases, instr_assigns_def]
>- (
`s1.ip with i := inc_bip (Offset idx) = inc_pc s1.ip` by rw [inc_pc_def] >>
simp [] >> irule prog_ok_nonterm >>
simp [get_instr_cases, terminator_def])
>- metis_tac [next_ips_reachable, mem_state_rel_def]
>- (
fs [w2n_i2n, pointer_size_def, mem_state_rel_def] >>
metis_tac [bytes_v_rel, get_bytes_erase_tags]))
>- rw [translate_reg_def]
>- (
fs [w2n_i2n, pointer_size_def, mem_state_rel_def] >>
metis_tac [is_allocated_erase_tags]))
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
>- ( (* Store *)
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
fs [step_inst_cases, get_instr_cases, PULL_EXISTS] >>
qpat_x_assum `Store _ _ = el _ _` (assume_tac o GSYM) >>
`bigunion (image arg_to_regs {a1; a2}) ⊆ live prog s1.ip`
by (
simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
instr_uses_def] >>
metis_tac []) >>
fs [] >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >> disch_then drule >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >> disch_then drule >> rw [] >>
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
qpat_x_assum `v_rel (FlatV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
drule v_rel_bytes >> rw [] >>
fs [w2n_i2n, pointer_size_def] >>
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
HINT_EXISTS_TAC >> rw [] >>
qexists_tac `freeable` >> rw [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
qexists_tac `v'` >> rw []
>- rw [llvmTheory.inc_pc_def, inc_pc_def]
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
>- (
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
simp [llvmTheory.inc_pc_def] >>
irule mem_state_rel_no_update >> rw []
>- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
>- (
`s1.ip with i := inc_bip (Offset idx) = inc_pc s1.ip` by rw [inc_pc_def] >>
simp [] >> irule prog_ok_nonterm >>
simp [get_instr_cases, terminator_def]) >>
irule mem_state_rel_heap_update >>
rw [set_bytes_unchanged, erase_tags_set_bytes] >>
fs [mem_state_rel_def, extend_emap_non_exp_def] >>
metis_tac [set_bytes_heap_ok])
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
>- (
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
fs [mem_state_rel_def] >>
fs [is_allocated_def, heap_component_equality, erase_tags_def] >>
metis_tac [])
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
>- (
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
(* TODO: mem_state_rel needs to relate the globals *)
fs [get_obs_cases, llvmTheory.get_obs_cases] >> rw [translate_trace_def] >>
fs [mem_state_rel_def, fmap_rel_OPTREL_FLOOKUP]
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
>- (
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
first_x_assum (qspec_then `x` mp_tac) >> rw [] >>
rename1 `option_rel _ _ opt` >> Cases_on `opt` >>
[sledge sem] Implement and verify cast expressions Summary: This commit adds truncation, sign extension and zero extension to LLVM and the Convert instruction to LLAIR. The LLVM instructions use HOL's build-in word/int and word/num conversions. Sanity-checking theorems prove that zero-extending leaves the value of the word unchanged when considered as an unsigned value, and that sign-extending leaves the value unchanged when considered as a signed value. The llair semantics for Convert uses the truncate_2comp function which converts an integer to another integer as though they were represented in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp 255 8 = -1, truncate_2comp -3 2 = 1 Reviewed By: jberdine Differential Revision: D18058833 fbshipit-source-id: df9de480c
5 years ago
fs [OPTREL_def] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
cheat) >>
cheat))
QED
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
Theorem classify_instr_term_call:
∀i. (classify_instr i = Term ⇔ terminator i) ∧
(classify_instr i = Call ⇔ is_call i)
Proof
Cases >> rw [classify_instr_def, is_call_def, terminator_def] >>
Cases_on `p` >> rw [classify_instr_def]
QED
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Definition untranslate_glob_var_def:
untranslate_glob_var (Var_name n ty) = Glob_var n
End
Definition untranslate_trace_def:
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
(untranslate_trace Tau = Tau) ∧
(untranslate_trace Error = Error) ∧
(untranslate_trace (Exit i) = (Exit i)) ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
(untranslate_trace (W gv bytes) = W (untranslate_glob_var gv) bytes)
End
Theorem un_translate_glob_inv:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀x t. untranslate_glob_var (translate_glob_var gmap x) = x
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Proof
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
Cases_on `x` >> rw [translate_glob_var_def] >>
CASE_TAC >> rw [untranslate_glob_var_def]
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
QED
Theorem un_translate_trace_inv:
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀x. untranslate_trace (translate_trace gmap x) = x
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Proof
Cases >> rw [translate_trace_def, untranslate_trace_def] >>
metis_tac [un_translate_glob_inv]
QED
[sledge sem] Improve and unify treatment of Exit Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago
Theorem take_to_call_lem:
∀i idx body.
idx < length body ∧ el idx body = i ∧ ¬terminator i ∧ ¬is_call i ⇒
take_to_call (drop idx body) = i :: take_to_call (drop (idx + 1) body)
Proof
Induct_on `idx` >> rw []
>- (Cases_on `body` >> fs [take_to_call_def] >> rw []) >>
Cases_on `body` >> fs [] >>
first_x_assum drule >> simp [ADD1]
QED
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Theorem translate_instrs_correct1:
∀prog s1 tr s2.
multi_step prog s1 tr s2 ⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀s1' b' gmap emap regs_to_keep d b idx.
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
prog_ok prog ∧ is_ssa prog ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
mem_state_rel prog gmap emap s1 s1' ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
alookup prog s1.ip.f = Some d ∧
alookup d.blocks s1.ip.b = Some b ∧
s1.ip.i = Offset idx ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
b' = fst (translate_instrs (dest_fn s1.ip.f) gmap emap regs_to_keep (take_to_call (drop idx b.body)))
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
⇒
∃emap s2' tr'.
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
step_block (translate_prog prog) s1' b'.cmnd b'.term tr' s2' ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace gmap) tr) ∧
state_rel prog gmap emap s2 s2'
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Proof
ho_match_mp_tac multi_step_ind >> rw_tac std_ss []
>- (
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
fs [last_step_cases]
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
>- ( (* Phi (not handled here) *)
fs [get_instr_cases])
>- ( (* Terminator *)
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
`(∃code. l = Exit code) ∨ l = Tau `
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
by (
fs [llvmTheory.step_cases] >>
`i' = i''` by metis_tac [get_instr_func, sumTheory.INL_11] >>
fs [step_instr_cases] >> rfs [terminator_def]) >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
fs [get_instr_cases, translate_trace_def] >> rw [] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
`el idx b.body = el 0 (drop idx b.body)` by rw [EL_DROP] >>
fs [] >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
Cases_on `drop idx b.body` >> fs [DROP_NIL] >> rw []
>- ( (* Exit *)
fs [llvmTheory.step_cases, get_instr_cases, step_instr_cases,
translate_instrs_def, take_to_call_def, classify_instr_def,
translate_instr_to_term_def, translate_instr_to_inst_def,
llvmTheory.get_obs_cases] >>
simp [Once step_block_cases, step_term_cases, PULL_EXISTS, step_inst_cases] >>
drule translate_arg_correct >>
disch_then drule >> impl_tac
>- (
`get_instr prog s1.ip (Inl (Exit a))` by rw [get_instr_cases] >>
drule get_instr_live >>
simp [uses_cases, SUBSET_DEF, IN_DEF, PULL_EXISTS] >>
rw [] >> first_x_assum irule >>
disj1_tac >>
metis_tac [instr_uses_def]) >>
rw [] >>
qexists_tac `emap` >>
qexists_tac `s1' with status := Complete code` >>
qexists_tac `[Exit code]` >>
rw []
>- (fs [v_rel_cases] >> fs [signed_v_to_int_def] >> metis_tac []) >>
rw [state_rel_def] >>
metis_tac [mem_state_rel_exited]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
simp [take_to_call_def, translate_instrs_def] >>
Cases_on `el idx b.body` >> fs [terminator_def, classify_instr_def, translate_trace_def] >> rw []
>- ( (* Ret *)
cheat)
>- ( (* Br *)
simp [translate_instr_to_term_def, Once step_block_cases] >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
simp [step_term_cases, PULL_EXISTS, RIGHT_AND_OVER_OR, EXISTS_OR_THM] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
fs [llvmTheory.step_cases] >>
drule get_instr_live >> disch_tac >>
drule translate_arg_correct >>
fs [step_instr_cases] >> fs [] >>
TRY (fs [get_instr_cases] >> NO_TAC) >>
`a = a'` by fs [get_instr_cases] >>
disch_then drule >>
impl_tac
>- (
fs [SUBSET_DEF, IN_DEF] >> rfs [uses_cases, get_instr_cases, instr_uses_def] >>
fs [IN_DEF]) >>
disch_tac >> fs [] >>
fs [v_rel_cases, GSYM PULL_EXISTS] >>
qexists_tac `emap` >> qexists_tac `w2i tf` >> simp [] >> conj_tac
>- metis_tac [] >>
Cases_on `s1'.bp` >> fs [dest_llair_lab_def] >>
rename1 `el _ _ = Br e lab1 lab2` >>
qexists_tac `dest_fn s1.ip.f` >>
qexists_tac `if 0 = w2i tf then dest_label lab2 else dest_label lab1` >> simp [] >>
qpat_abbrev_tac `target = if tf = 0w then l2 else l1` >>
qpat_abbrev_tac `target' = if 0 = w2i tf then dest_label lab2 else dest_label lab1` >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
`last b.body = Br a l1 l2 ∧
<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|> ∈ next_ips prog s1.ip`
by (
fs [prog_ok_def, get_instr_cases] >>
last_x_assum drule >> disch_then drule >>
strip_tac >> conj_asm1_tac
>- (
CCONTR_TAC >>
`Br a l1 l2 ∈ set (front (b.body))`
by (
`mem (Br a l1 l2) (front b.body ++ [last b.body])`
by metis_tac [EL_MEM, APPEND_FRONT_LAST] >>
fs [] >> metis_tac []) >>
fs [EVERY_MEM] >> first_x_assum drule >> rw [terminator_def])
>- (
rw [next_ips_cases, IN_DEF, assigns_cases] >>
disj1_tac >>
qexists_tac `Br a l1 l2` >>
rw [instr_next_ips_def, Abbr `target`] >>
fs [get_instr_cases, instr_to_labs_def] >>
metis_tac [blockHeader_nchotomy])) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
rw [] >>
`translate_label (dest_fn s1.ip.f) target = Lab_name (dest_fn s1.ip.f) target' `
by (
fs [get_instr_cases] >> rw [] >>
unabbrev_all_tac >> rw [] >> fs [word_0_w2i] >>
Cases_on `l2` >> Cases_on `l1` >> rw [translate_label_def, dest_label_def] >>
`0 = w2i (0w:word1)` by rw [word_0_w2i] >>
fs [w2i_11]) >>
rw [state_rel_def]
>- (Cases_on `lab2` >> rw [Abbr `target'`, translate_label_def, dest_label_def])
>- (Cases_on `lab1` >> rw [Abbr `target'`, translate_label_def, dest_label_def])
>- (
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
fs [get_instr_cases] >>
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
`every (λlab. ∃b phis landing. alookup d.blocks (Some lab) = Some b ∧ b.h = Head phis landing)
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
(instr_to_labs (last b.body))`
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
by (fs [prog_ok_def, EVERY_MEM] >> metis_tac []) >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
rfs [instr_to_labs_def] >>
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
rw [pc_rel_cases, get_instr_cases, get_block_cases, PULL_EXISTS] >>
fs [GSYM PULL_EXISTS, Abbr `target`] >>
rw [MEM_MAP, instr_to_labs_def] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
fs [translate_prog_def] >>
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
`∀y z. dest_fn y = dest_fn z ⇒ y = z`
by (Cases_on `y` >> Cases_on `z` >> rw [dest_fn_def]) >>
rw [alookup_map_key] >>
(* Unfinished, will get more proof obligations once pc_rel is fleshed
* out for Inr case *)
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
cheat)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
>- (
fs [mem_state_rel_def] >> rw []
>- (
qpat_x_assum `!r. r ∈ live _ _ ⇒ P r` mp_tac >>
simp [Once live_gen_kill] >> disch_then (qspec_then `r` mp_tac) >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
impl_tac >> rw [] >>
rw [PULL_EXISTS] >>
disj1_tac >>
qexists_tac `<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>` >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
rw [] >>
rw [IN_DEF, assigns_cases] >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
CCONTR_TAC >> fs [] >>
imp_res_tac get_instr_func >> fs [] >> rw [] >>
fs [instr_assigns_def])
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
>- (
fs [reachable_def] >>
qexists_tac `path ++ [<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>]` >>
rw_tac std_ss [good_path_append, GSYM APPEND] >> rw [] >>
rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >> metis_tac [])))
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
>- ( (* Invoke *)
cheat)
>- ( (* Unreachable *)
cheat)
>- ( (* Exit *)
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
fs [llvmTheory.step_cases, get_instr_cases, step_instr_cases])
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
>- ( (* Throw *)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
cheat))
>- ( (* Call *)
cheat)
>- ( (* Stuck *)
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
rw [translate_trace_def] >>
(* TODO: need to know that stuck LLVM instructions translate to stuck
* llair instructions. This will follow from knowing that when a llair
* instruction takes a step, the LLVM source can take the same step, ie,
* the backward direction of the proof. *)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
cheat))
>- ( (* Middle of the block *)
fs [llvmTheory.step_cases] >> TRY (fs [get_instr_cases] >> NO_TAC) >>
`i' = i` by metis_tac [get_instr_func, sumTheory.INL_11] >> fs [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
rename [`step_instr _ _ _ _ s2`, `state_rel _ _ _ s3 _`,
`mem_state_rel _ _ _ s1 s1'`] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Cases_on `∃r t. classify_instr i = Exp r t` >> fs []
>- ( (* instructions that compile to expressions *)
drule translate_instr_to_exp_correct >>
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
ntac 5 (disch_then drule) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
disch_then (qspec_then `regs_to_keep` mp_tac) >>
rw [] >> fs [translate_trace_def] >>
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
`reachable prog (inc_pc s1.ip)`
by metis_tac [prog_ok_nonterm, next_ips_reachable, mem_state_rel_def] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
first_x_assum drule >>
simp [inc_pc_def, inc_bip_def] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
disch_then (qspecl_then [`regs_to_keep`] mp_tac) >> rw [] >>
rename1 `state_rel prog gmap emap3 s3 s3'` >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
qexists_tac `emap3` >> qexists_tac `s3'` >> rw [] >>
`take_to_call (drop idx b.body) = i :: take_to_call (drop (idx + 1) b.body)`
[sledge sem] Improve and unify treatment of Exit Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago
by (
irule take_to_call_lem >> simp [] >>
fs [get_instr_cases]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
simp [translate_instrs_def] >>
Cases_on `r ∉ regs_to_keep` >> fs [] >> rw []
>- metis_tac [] >>
qexists_tac `Tau::tr'` >> rw [] >>
simp [Once step_block_cases] >> disj2_tac >>
pairarg_tac >> rw [] >> fs [] >>
metis_tac [])
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
>- ( (* Non-expression instructions *)
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
Cases_on `classify_instr i` >> fs [classify_instr_term_call] >>
drule translate_instr_to_inst_correct >>
ntac 5 (disch_then drule) >>
strip_tac >> fs [] >>
first_x_assum drule >> simp [inc_pc_def, inc_bip_def] >>
disch_then (qspecl_then [`regs_to_keep`] mp_tac) >> simp [] >>
strip_tac >>
rename1 `state_rel prog gmap emap3 s3 s3'` >>
qexists_tac `emap3` >> qexists_tac `s3'` >> simp [] >>
`take_to_call (drop idx b.body) = i :: take_to_call (drop (idx + 1) b.body)`
by (
irule take_to_call_lem >> simp [] >>
fs [get_instr_cases]) >>
simp [translate_instrs_def] >>
qexists_tac `translate_trace gmap l::tr'` >> rw [] >>
simp [Once step_block_cases] >> pairarg_tac >> rw [] >> fs [] >>
disj2_tac >>
qexists_tac `s2'` >> rw []))
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
QED
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Theorem multi_step_to_step_block:
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
∀prog s1 tr s2 s1'.
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
prog_ok prog ∧ is_ssa prog ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
multi_step prog s1 tr s2 ∧
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
s1.status = Partial ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap s1 s1'
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
⇒
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
∃s2' emap2 b tr'.
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
get_block (translate_prog prog) s1'.bp b ∧
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
step_block (translate_prog prog) s1' b.cmnd b.term tr' s2' ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace gmap) tr) ∧
state_rel prog gmap emap2 s2 s2'
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Proof
rw [] >> pop_assum mp_tac >> simp [Once state_rel_def] >> rw [pc_rel_cases]
>- (
[sledge sem] Improve and unify treatment of Exit Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago
(* Non-phi instruction *)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
drule translate_instrs_correct1 >> simp [] >>
disch_then drule >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
disch_then (qspecl_then [`regs_to_keep`] mp_tac) >> simp [] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
rw [] >>
qexists_tac `s2'` >> simp [] >>
ntac 3 HINT_EXISTS_TAC >>
rw [] >> fs [dest_fn_def]) >>
[sledge sem] Improve and unify treatment of Exit Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago
(* Phi instruction *)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
reverse (fs [Once multi_step_cases])
>- metis_tac [get_instr_func, sumTheory.sum_distinct] >>
qpat_x_assum `last_step _ _ _ _` mp_tac >>
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
simp [last_step_cases] >> strip_tac
>- (
fs [llvmTheory.step_cases]
>- metis_tac [get_instr_func, sumTheory.sum_distinct] >>
fs [translate_trace_def] >> rw [] >>
(* Needs the completed pc_rel for the Inr case *)
cheat)
>- metis_tac [get_instr_func, sumTheory.sum_distinct]
>- metis_tac [get_instr_func, sumTheory.sum_distinct]
>- (
fs [llvmTheory.step_cases] >> rw [translate_trace_def] >>
`!i. ¬get_instr prog s1.ip (Inl i)`
by metis_tac [get_instr_func, sumTheory.sum_distinct] >>
fs [METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
first_x_assum drule >> rw [] >>
`~every IS_SOME (map (do_phi from_l s1) phis)` by metis_tac [map_is_some] >>
fs [get_instr_cases] >>
rename [`alookup _ s1.ip.b = Some b_targ`, `alookup _ from_l = Some b_src`] >>
`every (phi_contains_label from_l) phis`
by (
fs [prog_ok_def, get_instr_cases] >>
first_x_assum (qspecl_then [`s1.ip.f`, `d`, `from_l`] mp_tac) >> rw [] >>
fs [EVERY_MEM, MEM_MAP] >>
rfs [] >> rw [] >> first_x_assum drule >> rw [] >>
first_x_assum irule >> fs [] >> rfs [] >> fs []) >>
fs [EVERY_MEM, EXISTS_MEM, MEM_MAP] >>
first_x_assum drule >> rw [] >>
rename1 `phi_contains_label _ phi` >> Cases_on `phi` >>
fs [do_phi_def, phi_contains_label_def] >>
rename1 `alookup entries from_l ≠ None` >>
Cases_on `alookup entries from_l` >> fs [] >>
(* TODO: LLVM "eval" gets stuck *)
cheat)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
QED
Theorem step_block_to_multi_step:
∀prog s1 s1' tr s2' b.
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap s1 s1' ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
get_block (translate_prog prog) s1'.bp b ∧
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
step_block (translate_prog prog) s1' b.cmnd b.term tr s2'
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
⇒
∃s2.
multi_step prog s1 (map untranslate_trace tr) s2 ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap s2 s2'
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Proof
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
(* TODO, LLVM can simulate llair direction *)
[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
cheat
QED
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Theorem trans_trace_not_tau:
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
∀types. ($≠ Tau) ∘ translate_trace types = ($≠ Tau)
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Proof
rw [FUN_EQ_THM] >> eq_tac >> rw [translate_trace_def] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
TRY (Cases_on `y`) >> fs [translate_trace_def]
QED
Theorem untrans_trace_not_tau:
∀types. ($≠ Tau) ∘ untranslate_trace = ($≠ Tau)
Proof
rw [FUN_EQ_THM] >> eq_tac >> rw [untranslate_trace_def] >>
TRY (Cases_on `y`) >> fs [untranslate_trace_def]
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
QED
Theorem translate_prog_correct_lem1:
∀path.
okpath (multi_step prog) path ∧ finite path
⇒
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
∀gmap emap s1'.
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
prog_ok prog ∧
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
is_ssa prog ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap (first path) s1'
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
⇒
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
∃path' emap.
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
finite path' ∧
okpath (step (translate_prog prog)) path' ∧
first path' = s1' ∧
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
LMAP (filter ($≠ Tau)) (labels path') =
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
LMAP (map (translate_trace gmap) o filter ($≠ Tau)) (labels path) ∧
state_rel prog gmap emap (last path) (last path')
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Proof
ho_match_mp_tac finite_okpath_ind >> rw []
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
>- (qexists_tac `stopped_at s1'` >> rw [] >> metis_tac []) >>
fs [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
rename1 `state_rel _ _ _ s1 s1'` >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
Cases_on `s1.status ≠ Partial`
>- fs [Once multi_step_cases, llvmTheory.step_cases, last_step_cases] >>
fs [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
drule multi_step_to_step_block >> ntac 4 (disch_then drule) >> rw [] >>
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
first_x_assum drule >> rw [] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
qexists_tac `pcons s1' tr' path'` >> rw [] >>
rw [FILTER_MAP, combinTheory.o_DEF, trans_trace_not_tau] >>
HINT_EXISTS_TAC >> simp [] >>
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
simp [step_cases] >> qexists_tac `b` >> simp [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
qpat_x_assum `state_rel _ _ _ _ s1'` mp_tac >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
rw [state_rel_def, mem_state_rel_def]
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
QED
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Theorem translate_prog_correct_lem2:
∀path'.
okpath (step (translate_prog prog)) path' ∧ finite path'
⇒
∀s1.
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
prog_ok prog ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap s1 (first path')
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
⇒
∃path.
finite path ∧
okpath (multi_step prog) path ∧
first path = s1 ∧
labels path = LMAP (map untranslate_trace) (labels path') ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap (last path) (last path')
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
Proof
ho_match_mp_tac finite_okpath_ind >> rw []
>- (qexists_tac `stopped_at s1` >> rw []) >>
fs [step_cases] >>
drule step_block_to_multi_step >> ntac 2 (disch_then drule) >> rw [] >>
first_x_assum drule >> rw [] >>
qexists_tac `pcons s1 (map untranslate_trace r) path` >> rw []
QED
Theorem translate_global_var_11:
∀path.
okpath (step (translate_prog prog)) path ∧ finite path
⇒
∀x t1 bytes t2 l.
labels path = fromList l ∧
MEM (W (Var_name x t1) bytes) (flat l) ∧
MEM (W (Var_name x t2) bytes) (flat l)
⇒
t1 = t2
Proof
[sledge sem] Make proof progress on phi instructions Summary: The old syntactic invariant in prog_ok was in the wrong direction, saying that all labels in a phi instruction have to exist, rather than saying that when we jump to a new block, the label of the block we came from must be in all of the phi instructions. Reviewed By: jberdine Differential Revision: D18058832 fbshipit-source-id: d2ad33b04
5 years ago
(* TODO, LLVM can simulate llair direction *)
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
cheat
QED
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
Theorem prefix_take_filter_lemma:
∀l lsub.
lsub ≼ l
⇒
filter (λy. Tau ≠ y) lsub =
take (length (filter (λy. Tau ≠ y) lsub)) (filter (λy. Tau ≠ y) l)
Proof
Induct_on `lsub` >> rw [] >>
Cases_on `l` >> fs [] >> rw []
QED
Theorem multi_step_lab_label:
∀prog s1 ls s2.
multi_step prog s1 ls s2 ⇒ s2.status ≠ Partial
⇒
∃ls'. (∃i. ls = ls' ++ [Exit i]) ∨ ls = ls' ++ [Error]
Proof
ho_match_mp_tac multi_step_ind >> rw [] >> fs [] >>
fs [last_step_cases, llvmTheory.step_cases, step_instr_cases,
update_result_def, llvmTheory.inc_pc_def] >>
rw [] >> fs []
QED
Theorem prefix_filter_len_eq:
∀l1 l2 x.
l1 ≼ l2 ++ [x] ∧
length (filter P l1) = length (filter P (l2 ++ [x])) ∧
P x
⇒
l1 = l2 ++ [x]
Proof
Induct_on `l1` >> rw [FILTER_APPEND] >>
Cases_on `l2` >> fs [] >> rw [] >> rfs [ADD1] >>
first_x_assum irule >> rw [FILTER_APPEND]
QED
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Theorem translate_prog_correct:
∀prog s1 s1'.
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
prog_ok prog ∧ is_ssa prog ∧
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
state_rel prog gmap emap s1 s1'
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
⇒
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
multi_step_sem prog s1 = image (I ## map untranslate_trace) (sem (translate_prog prog) s1')
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
Proof
rw [sem_def, multi_step_sem_def, EXTENSION] >> eq_tac >> rw []
>- (
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
drule translate_prog_correct_lem1 >> ntac 4 (disch_then drule) >> rw [pairTheory.EXISTS_PROD] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
PairCases_on `x` >> rw [] >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
qexists_tac `map (translate_trace gmap) x1` >> rw []
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
>- rw [MAP_MAP_o, combinTheory.o_DEF, un_translate_trace_inv] >>
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
qexists_tac `path'` >> rw [] >>
fs [IN_DEF, observation_prefixes_cases, toList_some] >> rw [] >>
[sledge sem] Improve and unify treatment of Exit Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago
`?labs. labels path' = fromList labs`
by (
fs [GSYM finite_labels] >>
imp_res_tac llistTheory.LFINITE_toList >>
fs [toList_some]) >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
fs [] >>
rfs [lmap_fromList, combinTheory.o_DEF, MAP_MAP_o] >>
simp [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF, FILTER_MAP]
>- fs [state_rel_def, mem_state_rel_def]
>- fs [state_rel_def, mem_state_rel_def] >>
rename [`labels path' = fromList l'`, `labels path = fromList l`,
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
`state_rel _ _ _ (last path) (last path')`, `lsub ≼ flat l`] >>
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
Cases_on `lsub = flat l` >> fs []
>- (
qexists_tac `flat l'` >>
rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF] >>
fs [state_rel_def, mem_state_rel_def]) >>
[sledge sem] Prove the Load and Store cases (mostly) Summary: This required some minor tweaks to how the semantics encode values into and out of byte lists. The remaining problems have to do with how LLVM globals are translated into llair. At the moment, llair semantic's state keeps a mapping for globals to their addresses, following the LLVM semantics. However, it is not used because the translation (following the code in frontend.ml) translates LLVM globals into llair locals, which the llair semantics isn't set up to handle. Reviewed By: jberdine Differential Revision: D17930787 fbshipit-source-id: 06c6368e0
5 years ago
`filter (λy. Tau ≠ y) (flat l') = map (translate_trace gmap) (filter (λy. Tau ≠ y) (flat l))`
[sledge sem] Update LLVM and LLAIR sem for consistent stuckness Summary: Previously, the LLVM semantics could be stuck where the LLAIR semantics was not yet stuck, but would become stuck (at the same place) after taking a step. This was due to LLVM using the traditional definition of stuck states: any state from which there are no transitions. However, LLAIR cannot do that because it might get stuck in the middle of a block that contains several visible stores. We don't want to consider the whole block stuck, nor can we finish it. Thus, the LLAIR definition of stuckness is when the state has the stuck flag set which happens when stopping in the middle of a block after encountering a stuck instruction. Now LLVM takes the same approach. Reviewed By: jberdine Differential Revision: D17855085 fbshipit-source-id: a094d25d5
5 years ago
by rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF, FILTER_MAP] >>
qexists_tac `take_prop ($≠ Tau) (length (filter ($≠ Tau) lsub)) (flat l')` >>
rw [] >> rw [GSYM MAP_TAKE]
>- metis_tac [prefix_take_filter_lemma] >>
CCONTR_TAC >> fs [] >>
`(last path).status = (last path').status` by fs [state_rel_def, mem_state_rel_def] >>
drule take_prop_eq >> strip_tac >>
`length (filter (λy. Tau ≠ y) (flat l')) = length (filter (λy. Tau ≠ y) (flat l))`
by rw [] >>
fs [] >> drule filter_is_prefix >>
disch_then (qspec_then `$≠ Tau` assume_tac) >>
drule IS_PREFIX_LENGTH >> strip_tac >> fs [] >>
`length (filter (λy. Tau ≠ y) lsub) = length (filter (λy. Tau ≠ y) (flat l))` by rw [] >>
fs [] >> rw [] >>
qspec_then `path` assume_tac finite_path_end_cases >> rfs [] >> fs [] >> rw []
>- (`l = []` by metis_tac [llistTheory.fromList_EQ_LNIL] >> fs [] >> rfs []) >>
rfs [labels_plink] >>
rename1 `LAPPEND (labels path) [|last_l'|] = _` >>
`toList (LAPPEND (labels path) [|last_l'|]) = Some l` by metis_tac [llistTheory.from_toList] >>
drule llistTheory.toList_LAPPEND_APPEND >> strip_tac >>
fs [llistTheory.toList_THM] >> rw [] >>
drule multi_step_lab_label >> strip_tac >> rfs [] >> fs [] >>
drule prefix_filter_len_eq >> rw [] >>
qexists_tac `$≠ Tau` >> rw [])
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
>- (
fs [toList_some] >>
[sledge sem] Fix trans. invariant for llair expressions Summary: If the LLVM to llair translation keeps a mapping from register r to expression e, then for each register r' mentioned in e, there must be an assignment to r' that dominates the entire live range of r. Thus, where ever r might be replaced by e, the value of r' will be the same as it was when the initial assignment to r occurred. Maintaining this invariant relies on the LLVM being in SSA form. Reviewed By: jberdine Differential Revision: D17710288 fbshipit-source-id: fd3eaa57d
5 years ago
drule translate_prog_correct_lem2 >> simp [] >>
disch_then drule >> rw [] >>
[sledge sem] Sketch out translation correctness Summary: This is work in progress; many of the cheats aren't true. In particular, the definition of stuck/complete/partial traces in LLVM and llair don't quite match up and need some modification. Also, the state relation isn't strong enough; it will need to include information about registers used in the expressions of the LLVM register to llair expression mapping. But the overall shape of the proof is ok and so it can be used to poke at various local aspects of the translation, such as individual instructions. Reviewed By: jberdine Differential Revision: D17631604 fbshipit-source-id: 743b5d64d
5 years ago
qexists_tac `path'` >> rw [] >>
fs [IN_DEF, observation_prefixes_cases, toList_some] >> rw [] >>
rfs [lmap_fromList] >>
simp [GSYM MAP_FLAT, FILTER_MAP, untrans_trace_not_tau]
>- fs [state_rel_def, mem_state_rel_def]
>- fs [state_rel_def, mem_state_rel_def] >>
qexists_tac `map untranslate_trace l2'` >>
simp [GSYM MAP_FLAT, FILTER_MAP, untrans_trace_not_tau] >>
`INJ untranslate_trace (set l2' ∪ set (flat l2)) UNIV`
by (
drule is_prefix_subset >> rw [SUBSET_DEF] >>
`set l2' ∪ set (flat l2) = set (flat l2)` by (rw [EXTENSION] >> metis_tac []) >>
simp [] >>
simp [INJ_DEF] >> rpt gen_tac >>
Cases_on `x` >> Cases_on `y` >> simp [untranslate_trace_def] >>
Cases_on `a` >> Cases_on `a'` >> simp [untranslate_glob_var_def] >>
metis_tac [translate_global_var_11]) >>
fs [INJ_MAP_EQ_IFF, inj_map_prefix_iff] >> rw [] >>
fs [state_rel_def, mem_state_rel_def])
[sledge sem] Add top-level llair semantics Summary: Give the llair semantics observable side effects (writes to global variables) and a semantic function mirroring the LLVM semantics. Start sketching out the LLVM/llair translation equivalence proof in a top-down way from the obvious statement of equality of the semantics. Reviewed By: jberdine Differential Revision: D17399654 fbshipit-source-id: 2170678a8
5 years ago
QED
[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
export_theory ();