diff options
| author | Robert Norton | 2017-09-07 11:59:27 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-09-07 11:59:27 +0100 |
| commit | c5b352f9fb87c1d42d93df4cb39cce7a0f8e0ff0 (patch) | |
| tree | f5d57f17935dec059fdc0e818f6b46cbabe4122a | |
| parent | 5207f6f2c53c9661bb4087a65f46fe6c5a74a776 (diff) | |
add MFENCE
| -rw-r--r-- | x86/x64.sail | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/x86/x64.sail b/x86/x64.sail index 2d17cf86..2f75f540 100644 --- a/x86/x64.sail +++ b/x86/x64.sail @@ -108,6 +108,7 @@ val extern forall Nat 'n. (qword, [|'n|]) -> (bit[8 * 'n]) effect { rmem } rMEM val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval +val extern unit -> unit effect { barr } X86_MFENCE function forall Nat 'n. unit effect {eamem, wmv} wMEM ((qword) addr, ([|'n|]) len, (bit[8 * 'n]) data) = { MEMea(addr, len); @@ -582,7 +583,7 @@ function unit drop ((qword) i) = if i[7 ..0] != 0 then () else RSP := RSP + i scattered function unit execute scattered typedef ast = const union -val ast -> unit effect {escape, rmem, rreg, undef, eamem, wmv, wreg} execute +val ast -> unit effect {escape, rmem, rreg, undef, eamem, wmv, wreg, barr} execute (* ========================================================================== Binop @@ -717,6 +718,15 @@ function clause execute (LOOP (c,i)) = } (* ========================================================================== + MFENCE + ========================================================================== *) + +union ast member unit MFENCE + +function clause execute (MFENCE) = + X86_MFENCE () + +(* ========================================================================== Monop ========================================================================== *) |