Skip to content
Merged
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
24 changes: 24 additions & 0 deletions majit/charon-corpus/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,30 @@ out in issue #97:
| `parse_one` | `match` with guards, internal helper for #4 | 9 |
| `desugar_mix` | `?` + `for` + `match` + `break` | 22 |

The corpus also includes a header-first object model. These functions pin
lowering decisions that otherwise fail by leaving a residual call or an
untyped field access rather than raising an error:

| Function | Premise it pins |
|-----------------------|-------------------------------------------------------|
| `w_object_type` | `(*w).ob_type` narrows to a *typed* `FieldRead` |
| `w_new_int` | the boxing cluster fuses to one `NewWithVtable` |
| `w_new_type_only_int` | so does a cluster whose header declares no class word |
| `w_number_add` | a narrowing-chain arm lowers to a direct `FunctionPath` call |

`ObjectHeader` has both `ob_type` and a per-instance `w_class`.
`TypeOnlyHeader` has only `ob_type`, matching RPython's root `OBJECT`, whose
only data field is `typeptr`. The two-word allocation can fuse when its
`w_class` is derived from the same class object as `ob_type`; the one-word
allocation can fuse from its declared layout because no class word exists to
disagree with the type pointer.

The fixture spells `pyre_object::pyobject::get_instantiate` literally because
`model.rs` currently recognises that path suffix. The one-word header does not
use this helper. `_immutable_fields_W_IntObject` preserves the marker shape
harvested by `front::llbc_hints`.


## Findings

### 1. `.llbc` top-level shape
Expand Down
2 changes: 1 addition & 1 deletion majit/charon-corpus/corpus.ullbc

Large diffs are not rendered by default.

149 changes: 149 additions & 0 deletions majit/charon-corpus/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,155 @@ pub fn option_question_mark(keep: bool, value: i64, addend: i64) -> Option<i64>
Some(v + addend)
}

// 8. Header-first object model
//
// 1. `(*w).ob_type` off a `*mut ObjectHeader` — a `FieldRead` preceded by
// a `__pyre_cast_instance/<Root>` narrow, not a classdef-less read.
// 2. `lltype::malloc_typed(Leaf { ob_header: .., payload })` — one
// by-value argument, header written before the call, so
// `fuse_boxing_alloc` mints `NewWithVtable` with a real vtable.
// 3. `if ta == &CLS { concrete(..) }` — the arm body a `FunctionPath`
// call, i.e. inlinable, rather than an indirect one.
// 4. an `_immutable_fields_<Struct>` marker const, so the payload read
// can fold to a pure getfield.
//
// `TypeOnlyHeader` matches RPython's root `OBJECT`, whose only data field is
// `typeptr`. `ObjectHeader` additionally represents an object model with a
// per-instance class word. Both allocation shapes must fuse.

#[repr(C)]
pub struct ClassObject {
pub name: &'static str,
pub kind: u8,
}

#[repr(C)]
pub struct ObjectHeader {
pub ob_type: *const ClassObject,
pub w_class: *const ClassObject,
}

/// The one-word header: `ob_type` and nothing else.
///
/// `fuse_boxing_alloc`'s substitution asks whether the per-instance class
/// word agrees with `ob_type`; where the header declares no such word the
/// question has no subject, and `model.rs`'s `header_declares_no_class_word`
/// arm admits the cluster on the layout alone. That arm is unreachable from
/// any fixture whose header declares the field, so it gets its own.
#[repr(C)]
pub struct TypeOnlyHeader {
pub ob_type: *const ClassObject,
}

#[repr(C)]
#[allow(non_camel_case_types)]
pub struct W_IntObject {
pub ob_header: ObjectHeader,
pub intval: i64,
}

#[repr(C)]
#[allow(non_camel_case_types)]
pub struct W_TypeOnlyIntObject {
pub ob_header: TypeOnlyHeader,
pub intval: i64,
}

pub static INT_CLASS: ClassObject = ClassObject {
name: "int",
kind: 1,
};
pub static DOUBLE_CLASS: ClassObject = ClassObject {
name: "double",
kind: 2,
};

/// The allocation entry point. `is_malloc_typed` keys on the trailing path
/// segments `lltype::malloc_typed`, and `fuse_boxing_alloc` requires the
/// single by-value argument — an alloc-then-init spelling matches nothing
/// and degrades in silence.
pub mod lltype {
#[inline(never)]
pub fn malloc_typed<T>(value: T) -> *mut T {
Box::into_raw(Box::new(value))
}
}

/// Minimal stand-in for the class-instantiation lookup whose result the
/// class word is stored from.
///
/// `model.rs`'s `get_instantiate_arg_addr` matches the three-segment path
/// suffix `["pyre_object", "pyobject", "get_instantiate"]` literally, so any
/// other spelling would not exercise that recognizer.
pub mod pyre_object {
pub mod pyobject {
use crate::ClassObject;

#[inline(never)]
pub fn get_instantiate(tp: &ClassObject) -> *const ClassObject {
tp
}
}
}

/// Premise 1: the header read.
#[inline(never)]
pub fn w_object_type(w: *mut ObjectHeader) -> *const ClassObject {
unsafe { (*w).ob_type }
}

/// Premise 2: the boxing cluster — header store, payload store, then one
/// by-value `malloc_typed`.
#[inline(never)]
pub fn w_new_int(x: i64) -> *mut W_IntObject {
lltype::malloc_typed(W_IntObject {
ob_header: ObjectHeader {
ob_type: &INT_CLASS,
w_class: pyre_object::pyobject::get_instantiate(&INT_CLASS),
},
intval: x,
})
}

/// Premise 2, second header shape: the same cluster over a header that
/// declares no class word, so the fuse has to admit it on the layout alone.
/// The `get_instantiate` call has no subject here and is absent.
#[inline(never)]
pub fn w_new_type_only_int(x: i64) -> *mut W_TypeOnlyIntObject {
lltype::malloc_typed(W_TypeOnlyIntObject {
ob_header: TypeOnlyHeader {
ob_type: &INT_CLASS,
},
intval: x,
})
}

#[inline(never)]
fn w_int_add(a: *mut W_IntObject, b: *mut W_IntObject) -> i64 {
unsafe { (*a).intval + (*b).intval }
}

/// Premise 3: the narrowing chain. `descroperation.py` `binop_impl`
/// (`type(w_obj1) is type(w_obj2)`, then the per-class shortcut)
/// transliterated — the shape that lowers each arm to a direct call.
#[inline(never)]
pub fn w_number_add(a: *mut ObjectHeader, b: *mut ObjectHeader) -> i64 {
let ta = unsafe { (*a).ob_type };
let tb = unsafe { (*b).ob_type };
if ta == tb && ta == (&INT_CLASS as *const ClassObject) {
return w_int_add(a as *mut W_IntObject, b as *mut W_IntObject);
}
0
}

/// Premise 4: the immutability marker `harvest_immutable_fields_from_llbcs`
/// reads (`front/llbc_hints.rs:148` `_immutable_fields_` prefix). Written by
/// hand rather than through `#[jit_immutable_fields]` so the corpus keeps
/// its zero-dependency manifest.
#[allow(non_upper_case_globals)]
pub const _immutable_fields_W_IntObject: &str = "intval";


// A host-registered callback table.

/// The callback a host installs at run time. A bare `fn` pointer, so the set
Expand Down
8 changes: 7 additions & 1 deletion majit/majit-charon-reader/tests/corpus.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,19 @@ fn loads_fixture_corpus() {
// + `option_source` and `option_question_mark` (the Option `?` fixture)
// + `bool_then_some` (the eager `then_some` sibling, no closure).
//
// + 10 for the header-first object model: `w_object_type`, `w_new_int`,
// `w_new_type_only_int`, `w_number_add`, `w_int_add`,
// `lltype::malloc_typed`, the fixture's `pyobject::get_instantiate`, and
// the initializer bodies for `INT_CLASS`, `DOUBLE_CLASS`, and
// `_immutable_fields_W_IntObject`.
//
// + 2 for the host-registered callback table: `host_registry_dispatch`
// and `host_registry_dispatch_optional`. `HostCallback` is a type alias,
// not an item, so it contributes no body.
//
// + 2 for the iterator element-kind pair, `slice_of_refs_sum` and
// `array_of_refs_sum`.
assert_eq!(local_count, 16, "16 local fns expected");
assert_eq!(local_count, 26, "26 local fns expected");
}

#[test]
Expand Down
Loading
Loading