Skip to content

Support for raw pointers #532

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion kmir/pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kmir"
version = "0.3.121"
version = "0.3.122"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kmir/src/kmir/__init__.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
from typing import Final

VERSION: Final = '0.3.121'
VERSION: Final = '0.3.122'
144 changes: 143 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/rt/data.md
Original file line number Diff line number Diff line change
Expand Up @@ -581,6 +581,58 @@ The solution is to use rewrite operations in a downward pass through the project
andBool (FORCE orBool MUT ==K mutabilityMut)
[preserves-definedness]

rule <k> #projectedUpdate(
_DEST,
typedValue(Ptr(OFFSET, place(LOCAL, PLACEPROJ), MUT, _ADDRESS, _OFFSET2), _, _),
projectionElemDeref PROJS,
Comment on lines +584 to +587
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is also #readProjection earlier in this module, which will require the same kind of extension to Deref a pointer.

rule <k> #readProjection(
typedValue(Reference(FRAME, place(LOCAL:Local, PLACEPROJS), _), _, _),
projectionElemDeref PROJS
)
=>
#readProjection(
{#localFromFrame({STACK[FRAME -Int 1]}:>StackFrame, LOCAL, FRAME)}:>TypedValue,
appendP(PLACEPROJS, PROJS)
)

UPDATE,
_CTXTS,
FORCE
)
=>
#projectedUpdate(
toStack(OFFSET, LOCAL),
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET),
appendP(PLACEPROJ, PROJS), // apply ptr (reference) projections first, then rest
UPDATE,
.Contexts, // previous contexts obsolete
FORCE
)
...
</k>
<stack> STACK </stack>
requires 0 <Int OFFSET
andBool OFFSET <=Int size(STACK)
andBool isStackFrame(STACK[OFFSET -Int 1])
andBool (FORCE orBool MUT ==K mutabilityMut)
[preserves-definedness]

rule <k> #projectedUpdate(
_DEST,
typedValue(Ptr(OFFSET, place(local(I), PLACEPROJ), MUT, _ADDRESS, _OFFSET2), _, _),
projectionElemDeref PROJS,
UPDATE,
_CTXTS,
FORCE
)
=>
#projectedUpdate(
toLocal(I),
{LOCALS[I]}:>TypedLocal,
appendP(PLACEPROJ, PROJS), // apply ptr (reference) projections first, then rest
UPDATE,
.Contexts, // previous contexts obsolete
FORCE
)
...
</k>
<locals> LOCALS </locals>
requires OFFSET ==Int 0
andBool 0 <=Int I
andBool I <Int size(LOCALS)
andBool (FORCE orBool MUT ==K mutabilityMut)
[preserves-definedness]

rule <k> #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false)
=>
#setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS))
Expand Down Expand Up @@ -831,7 +883,19 @@ A `CopyForDeref` `RValue` has the semantics of a simple `Use(operandCopy(...))`,
```k
rule <k> rvalueCopyForDeref(PLACE) => rvalueUse(operandCopy(PLACE)) ... </k>

// AddressOf: not implemented yet
```

### Raw Pointers
TODO

```k
// FIXME: Address is currently hardcoded to 0 so that the alignment check passes everytime
rule <k> rvalueAddressOf( MUTABILITY, PLACE)
=>
typedValue( Ptr( 0, PLACE, MUTABILITY, 0, 0), TyUnknown, MUTABILITY ) // TyUnknown and MUTABILITY will be overwritten to the Local's type
...
</k>

```

## Type casts
Expand Down Expand Up @@ -890,6 +954,25 @@ Error cases for `castKindIntToInt`
[owise]
```

### Pointer Casts

Casting between two raw pointers. FIXME: No validity checks are currently performed

```k
// FIXME: Address and Offset are blindly transferred through
rule <k> #cast( typedValue(Ptr(DEPTH, PLACE, PTR_MUT, ADDRESS, OFFSET), _TY_FROM, LOCAL_MUT), castKindPtrToPtr, TY_TO)
=>
typedValue(Ptr(DEPTH, PLACE, PTR_MUT, ADDRESS, OFFSET), TY_TO, LOCAL_MUT)
...
</k>
// <types> TYPEMAP </types>
// requires TY_TO #in TYPEMAP
// requires #is_valid_cast(TY_FROM.layout(), TY_TO.layout())

rule <k> #cast( typedValue(VALUE, _TY_FROM, LOCAL_MUT), castKindTransmute, TY_TO) => typedValue(VALUE, TY_TO, LOCAL_MUT) ... </k>
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well... this rule is certainly too generic.
Right now we only want to cast raw pointers and return their "Address" (IIUC, or something that is derived from it?), as a usize value that will suit the example program...


```

### Other type casts

Other type casts are not implemented yet.
Expand Down Expand Up @@ -1315,6 +1398,57 @@ The `unOpNot` operation works on boolean and integral values, with the usual sem
`binOpShr`
`binOpShrUnchecked`

```k
syntax Bool ::= isBitwise ( BinOp ) [function, total]
// --------------------------------------------------
rule isBitwise(binOpBitXor) => true
rule isBitwise(binOpBitAnd) => true
rule isBitwise(binOpBitOr) => true
rule isBitwise(_) => false [owise]

syntax Bool ::= isShift ( BinOp ) [function, total]
// ------------------------------------------------
rule isShift(binOpShl) => true
rule isShift(binOpShlUnchecked) => true
rule isShift(binOpShr) => true
rule isShift(binOpShrUnchecked) => true
rule isShift(_) => false [owise]

rule onInt(binOpBitXor, X, Y) => X xorInt Y
rule onInt(binOpBitAnd, X, Y) => X &Int Y
rule onInt(binOpBitOr, X, Y) => X |Int Y

// Only permitting non-shift bitwise operations on same width integers, overflow check not required
rule #compute(
BOP,
typedValue(Integer(ARG1, WIDTH, _), _, _),
typedValue(Integer(ARG2, WIDTH, _), _, _),
false) // unchecked
=>
typedValue(
Integer(onInt(BOP, ARG1, ARG2), WIDTH, false),
TyUnknown,
mutabilityNot
)
Comment on lines +1422 to +1432
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Two things to correct:

  • Your result is always unsigned but we have to keep the signedness flag from the arguments.
Suggested change
rule #compute(
BOP,
typedValue(Integer(ARG1, WIDTH, _), _, _),
typedValue(Integer(ARG2, WIDTH, _), _, _),
false) // unchecked
=>
typedValue(
Integer(onInt(BOP, ARG1, ARG2), WIDTH, false),
TyUnknown,
mutabilityNot
)
rule #compute(
BOP,
typedValue(Integer(ARG1, WIDTH, SIGNED), TY, _),
typedValue(Integer(ARG2, WIDTH, SIGNED), TY, _),
false) // unchecked
=>
typedValue(
Integer(onInt(BOP, ARG1, ARG2), WIDTH, SIGNED),
TY,
mutabilityNot
)
  • We have to ensure the Ty are the same for both arguments (I added the match on TY above). There are rules that checks this, and the suitability of the operands, for arithmetic operations. Maybe we should add similar rules for bit-oriented ones, to signal TypeMismatch or OperandMismatch errors

requires isBitwise(BOP)
[preserves-definedness]

rule #compute(
BOP,
typedValue(Ptr(_, _, _, ADDRESS, _), _, _),
typedValue(Integer(VAL, WIDTH, _), _, _),
Comment on lines +1438 to +1439
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

??? Do we really need this rule? I thought the Ptr value gets cast to usize before that, or not?

EDIT after reading the related cast rule: Maybe the cast should just be different and we delete this rule.

false) // unchecked
=>
typedValue(
Integer(onInt(BOP, VAL, ADDRESS), WIDTH, false),
TyUnknown,
mutabilityNot
)
requires isBitwise(BOP)
[preserves-definedness]

```


#### Nullary operations for activating certain checks

Expand All @@ -1332,6 +1466,14 @@ One important use case of `UbChecks` is to determine overflows in unchecked arit
`nullOpAlignOf`
`nullOpOffsetOf(VariantAndFieldIndices)`

```k
rule <k> rvalueNullaryOp(nullOpAlignOf, TY) => typedValue( Integer(#alignOf({TYPEMAP[TY]}:>TypeInfo), 64, false), TyUnknown, mutabilityNot ) ... </k> // FIXME: 64 is hardcoded since usize not supported
<types> TYPEMAP </types>
requires TY in_keys(TYPEMAP)
andBool isTypeInfo(TYPEMAP[TY])

```

#### Other operations

`binOpOffset`
Expand Down
29 changes: 29 additions & 0 deletions kmir/src/kmir/kdist/mir-semantics/rt/numbers.md
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,35 @@ This truncation function is instrumental in the implementation of Integer arithm
[preserves-definedness] // positive shift, divisor non-zero
```

## Alignment of Primitives

```k
// FIXME: Alignment is platform specific
syntax Int ::= #alignOf( TypeInfo ) [function]

rule #alignOf( typeInfoPrimitiveType(primTypeBool) ) => 1
rule #alignOf( typeInfoPrimitiveType(primTypeChar) ) => 4

rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyIsize)) ) => 8 // FIXME: Hard coded since usize not implemented
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI8)) ) => 1
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI16)) ) => 2
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI32)) ) => 4
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI64)) ) => 8
rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI128)) ) => 16

rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyUsize)) ) => 8 // FIXME: Hard coded since usize not implemented
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU8)) ) => 1
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU16)) ) => 2
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU32)) ) => 4
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU64)) ) => 8
rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU128)) ) => 16

rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF16)) ) => 2
rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF32)) ) => 4
rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF64)) ) => 8
rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF128)) ) => 16
```

```k
endmodule
```
4 changes: 2 additions & 2 deletions kmir/src/kmir/kdist/mir-semantics/rt/value.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ High-level values can be
// stack depth (initially 0), place, borrow kind
| Range( List )
// homogenous values for array/slice
// | Ptr( Address, MaybeValue ) // FIXME why maybe? why value?
// address, metadata for ref/ptr
| Ptr( Int, Place, Mutability, Int, Int)
// stack depth (initially zero), place, mutablility, address, offset NOTE: First 3 fields are the same as Reference, last are needed for low level instructions
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit-pick: long line

Suggested change
// stack depth (initially zero), place, mutablility, address, offset NOTE: First 3 fields are the same as Reference, last are needed for low level instructions
// stack depth (initially zero), place, mutablility, address, offset
// NOTE: First 3 fields are the same as Reference, last are needed for low level instructions

| "Any"
// arbitrary value for transmute/invalid ptr lookup
```
Expand Down
5 changes: 5 additions & 0 deletions kmir/src/tests/integration/data/exec-smir/memory/local-raw.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
fn main() {
let mut x: u32 = 3;
let y: *mut u32 = &mut x;
unsafe { *y = 0; }
}
Loading
Loading