Skip to content

Type Inference & SVA#58

Draft
JTrenerry wants to merge 90 commits intomainfrom
type-inference
Draft

Type Inference & SVA#58
JTrenerry wants to merge 90 commits intomainfrom
type-inference

Conversation

@JTrenerry
Copy link
Copy Markdown
Collaborator

@JTrenerry JTrenerry commented Feb 23, 2026 •
edited
Loading

  • SVA
    • Intra pass
    • IDE pass
  • Type inferencing
    • Constraint generation (Relies on SVA)
    • Type coalescing
    • Type Automata
    • Type lowering
      • Remove Ep
      • Merge Nodes (old code in git so should be simple)
      • mini Unsure if this does anything of value
    • Transform
      • Add in new expressions
      • Type transform
        • type decls
        • Exprs
        • stmts
        • function in / out
          attrib
(run-transforms "ssa")
(run-transforms "cf-expressions")
(run-transforms "type-check")
(run-transforms "type-inference")

Note: SVA does not net very good results in most cases

@JTrenerry JTrenerry self-assigned this Feb 23, 2026
@JTrenerry JTrenerry added the enhancement New feature or request label Feb 23, 2026
@JTrenerry JTrenerry force-pushed the type-inference branch 4 times, most recently from 8489b31 to 6bab69a Compare March 2, 2026 03:42
@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 2, 2026

Is testing analysis just by doing the value soundness enough? The lattices I am using should be tested already I believe as it is just wrapped and map lattice from Hayden and bpal.

@JTrenerry JTrenerry marked this pull request as ready for review March 2, 2026 07:15
@JTrenerry JTrenerry requested a review from agle March 2, 2026 07:15
@agle agle changed the title Type Inferencing & SVA Type Inference & SVA Mar 4, 2026
@JTrenerry JTrenerry mentioned this pull request Mar 5, 2026
Merged
@JTrenerry JTrenerry marked this pull request as draft March 5, 2026 01:02
@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 5, 2026

I think it would be best if this is merged once fully complete as it would allow for more complete testing.

If SVA is needed elsewhere I can cherry pick those commits, but I also would need some better testing for SVA as well.

@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 9, 2026

Globals are not done in SVA, will probably have to confirm with Nick but he did not want me to just say things are globals and then the offsets goes out of that global area and now I have to widen.

I believe what he wanted (although I do not remember), after I get all the offsets I can then check to see if it lines up maybe, but even that seems iffy, I remember him saying, keep it is a constant unless I need it to be a global, but like when would I ever need it to be global?

@JTrenerry JTrenerry force-pushed the type-inference branch 3 times, most recently from 4e2f24d to deb3282 Compare March 13, 2026 04:22
@JTrenerry JTrenerry force-pushed the type-inference branch 2 times, most recently from 3dd9fb4 to 7552bba Compare March 17, 2026 05:15
@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 18, 2026 •
edited
Loading

Current example output:

   block %main_entry [
     var #4_1:pointer_667510074 := bvadd(R31_1:bv64, 0xffffffffffffffe0:bv64);
     $stack:1_load/store := store le $stack:1_load/store #4_1:pointer_667510074 R29_1:bv64 64;
     $stack:1_load/store := store le $stack:1_load/store bvadd(#4_1:pointer_667510074,
      0x8:bv64) R30_1:bv64 64;
     var R31_2:bv64 := #4_1:pointer_667510074;
     var R29_2:bv64 := R31_2:bv64;
     $stack:1_load/store := store le $stack:1_load/store bvadd(R31_2:bv64,
      0x1c:bv64) extract(32,0, R0_1:bv64) 32;
     $stack:1_load/store := store le $stack:1_load/store bvadd(R31_2:bv64,
      0x10:bv64) R1_1:bv64 64;
     var R0_2:bv64 := 0x20000:bv64;
     var R0_3:pointer_361240275 := bvadd(R0_2:bv64, 0x3c:bv64);
     $mem:7_load/store := store le $mem:7_load/store R0_3:pointer_361240275 0x0:bv32 32;
     var R0_4:bv64 := 0x20000:bv64;
     var R0_5:pointer_468552588 := bvadd(R0_4:bv64, 0x40:bv64);
     var load18_1:record_641486071 := load le $mem:7_load/store R0_5:pointer_468552588 32;
     var R0_6:bv64 := zero_extend(32, load18_1:record_641486071);
     var R0_7:record_171251786 := zero_extend(32,
     bvconcat(0x0:bv31, extract(1,0, R0_6:bv64)));
     var #5_1:bv32 := bvadd(extract(32,0, R0_7:record_171251786), 0xffffffff:bv32);
     var VF_2:bv1 := bvnot(booltobv1(eq(sign_extend(1, bvadd(#5_1:bv32, 0x1:bv32)),
        sign_extend(1, extract(32,0, R0_7:record_171251786)))));
     var CF_2:bv1 := bvnot(booltobv1(eq(zero_extend(1, bvadd(#5_1:bv32, 0x1:bv32)),
        bvadd(zero_extend(1, extract(32,0, R0_7:record_171251786)),
         0x100000000:bv33))));
     var ZF_2:bv1 := booltobv1(eq(bvadd(#5_1:bv32, 0x1:bv32), 0x0:bv32));
     var NF_2:bv1 := extract(32,31, bvadd(#5_1:bv32, 0x1:bv32));
     goto (%main_27,%main_23);
   ];

Todo

- Attrib sets aren't type casted, this seems terrible to do though (Might make maps on them, but im unsure about use cases outside of this) Ali said no
- Function params / rets

Improvements

  • Some lack of competency around Extends.
  • Singleton records lowkey aren't records

Issues

Weird assignments not working properly.

     var R31_2:bv64 := #4_1:pointer_667510074;
     var R29_2:bv64 := R31_2:bv64;

This doesn't cascade the pointer type somehow.

     $stack:1_load/store := store le $stack:1_load/store bvadd(R31_2:bv64,
      0x1c:bv64) extract(32,0, R0_1:bv64) 32;
     $stack:1_load/store := store le $stack:1_load/store bvadd(R31_2:bv64,
      0x10:bv64) R1_1:bv64 64;

This also doesn't cascade the pointer type, but this is known and due to lack of constrain calls on load / stores, changing this should fix it.

Edit: Implemented the above and it fixed those two issues, the first may still be lurking and only fixed in this case due to the pointers being better, but doubt it

@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 18, 2026 •
edited
Loading

Idea for recursives:

make inferred_to_real return something like this

Recursive name,ty -> (name, inferred_to_real ty rec), Variable name

and then that first element can be turned into extra decls

Edit: Done but not tested

@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 20, 2026

type ptr_pointer_207517760(record_349067438{("131132": (record_270654248{("131132": (7_store, 131132))}, 131132))}, 7_store);

This looks like an error, will need to investigate

@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 20, 2026

records will be present within the IR and be converted when needed to sorts.

@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 20, 2026

store constraint seems wrong, stmt number is not good enough for store names.

@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 20, 2026

tests are currently wrong as names were added to recs / ptrs

JTrenerry
JTrenerry commented Mar 20, 2026
View reviewed changes
lib/transforms/type_inference.ml
let rec iter f (ty : t) =
f ty;
match ty with
| Top | Bottom | BinCamlType _ | TypeVar _ | Recursive _ -> ()
Copy link
Copy Markdown
Collaborator Author

@JTrenerry JTrenerry Mar 20, 2026

Choose a reason for hiding this comment

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

recursive needs to go deeper

lib/transforms/type_inference.ml
| Variable a -> TypeVar (VarId.make_id a)
| Pointer { lower; upper } ->
Pointer (type_to_inferred lower, type_to_inferred upper)
| Record (name, fields) -> failwith "TODO"
Copy link
Copy Markdown
Collaborator Author

@JTrenerry JTrenerry Mar 20, 2026

Choose a reason for hiding this comment

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

finish this

lib/transforms/type_inference.ml
let rec type_to_state_list p (ty : InferredType.t) ((ls, tbl) as acc) =
let open Sigma in
match ty with
| Top | BinCamlType _ | TypeVar _ | Bottom | Field _ ->
Copy link
Copy Markdown
Collaborator Author

@JTrenerry JTrenerry Mar 20, 2026

Choose a reason for hiding this comment

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

what if field isnt just a single type

lib/transforms/type_inference.ml
let st = constrain_arg proc st l t in
constrain_arg proc st r t

let rec constrain_expr proc (st : ConstraintState.t)
Copy link
Copy Markdown
Collaborator Author

@JTrenerry JTrenerry Mar 20, 2026

Choose a reason for hiding this comment

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

i should seperate this into each type of expr.

lib/transforms/type_inference.ml
let st = constrain st (Pointer (lb, ub)) addr in
let st = constrain st ub lb in
constrain st ty (TypeVar lhs)
| Stmt.Instr_Store { lhs; addr = Addr { addr; size } } ->
Copy link
Copy Markdown
Collaborator Author

@JTrenerry JTrenerry Mar 20, 2026

Choose a reason for hiding this comment

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

i want this and load to be more function

@JTrenerry
Copy link
Copy Markdown
Collaborator Author

JTrenerry commented Mar 26, 2026

extract has errors where the coalescing is wrong, i forget if i fixed this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@agle agle Awaiting requested review from agle

Assignees

@JTrenerry JTrenerry

Labels

enhancement New feature or request

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@JTrenerry