Propagate unsafety to definitions that depend on unsafe definitions #379

edusporto · 2024-06-07T19:17:59Z

Related to #362.

This PR kind of fixes the issue, but not really. While this new version does return an error in the previously thought "correct" version of the program, which is expected since it actually performed unsafe operations, it doesn't error in the second version, which does the same. Returning an error in this version is much harder, since it's not cloning an unsafe definition, but an unsafe expression. According to Nicolas, that could be solved with an affine type system.

TODO: - Document how the algorithm works along with complexities - From the original bug that led to this, `ok.hvm` now works as expectes but `bad.hvm` still doesn't... - Investigate

edusporto · 2024-06-07T19:22:28Z

src/ast.rs

+  pub fn direct_dependencies<'name>(&'name self) -> BTreeSet<&'name str> {
+    match self {
+      Tree::Ref { nam } => BTreeSet::from([nam.as_str()]),
+      Tree::Con { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Dup { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Opr { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Swi { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Num { val } => BTreeSet::new(),
+      Tree::Var { nam } => BTreeSet::new(),
+      Tree::Era => BTreeSet::new(),
+    }
+  }


Writing a recursive function like this may not be the best idea since we still don't have a way to increase stack size as needed like in the hvm-64 repo. I think it's fine for now to add this function like this, since pretty much all the other functions related to trees are also recursive and if this one fails, they do too.

if it becomes a problem we can just write this imperatively

This function is quadratic, due to repeatedly cloning these btreesets; (@a (@b (@c (@d (@e ...))))) will take triangular time (which is asymptotically quadratic).

This function is quadratic, due to repeatedly cloning these btreesets; (@a (@b (@c (@d (@e ...))))) will take triangular time (which is asymptotically quadratic).

Thanks! I thought it would be similar to merging in merge sort, but I tested it and it really is slow. It should be better now.

edusporto · 2024-06-07T19:23:48Z

tests/run.rs

+    println!("only testing rust implementation for {path:?}");
+    return;
+  }
+


I added the possibility to only run tests in the Rust implementation, since the C one doesn't throw an error in this same case. This is something to discuss - should the C and CUDA implementations also "panic" printing this error and stopping the program?

I think this is fine as is, and is in line with the other test-io pattern.

enricozb

So if I understand correctly, this doesn't account for user-introduced unsafety? It only accounts for when users reference an unsafe function?

enricozb · 2024-06-10T09:00:20Z

src/ast.rs

+  pub fn direct_dependencies<'name>(&'name self) -> BTreeSet<&'name str> {
+    match self {
+      Tree::Ref { nam } => BTreeSet::from([nam.as_str()]),
+      Tree::Con { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Dup { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Opr { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Swi { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Num { val } => BTreeSet::new(),
+      Tree::Var { nam } => BTreeSet::new(),
+      Tree::Era => BTreeSet::new(),
+    }
+  }


if it becomes a problem we can just write this imperatively

enricozb · 2024-06-10T09:02:40Z

tests/run.rs

+    println!("only testing rust implementation for {path:?}");
+    return;
+  }
+


I think this is fine as is, and is in line with the other test-io pattern.

edusporto · 2024-06-10T13:20:52Z

So if I understand correctly, this doesn't account for user-introduced unsafety? It only accounts for when users reference an unsafe function?

Depends on what you mean by "user-introduced", since users also introduce definitions. It will only catch unsafe operations if the unsafe operation is contained in a definition, and a reference to that definition is directly duplicated.

For example, exponentiation of church naturals (which I think should behave poorly in IC?)

unsf = @f @x (f (f x))
main = (unsf unsf)

This currently gets compiled to

@main = a
  & @unsf ~ (@unsf a)

@unsf = ({(b c) (a b)} (a c))

which is correctly marked as unsafe. We could also do

@main = a
  & ({(b c) (d b)} (d c)) ~ (({(b c) (d b)} (d c)) a)

which is not marked as unsafe, and does not terminate (loops forever)

edusporto · 2024-06-10T13:31:31Z

@developedby this PR breaks (surprisingly only) one of the tests in Bend, guide_shader_dummy.bend:

# given a shader, returns a square image
def render(depth, shader):
  bend d = 0, i = 0:
    when d < depth:
      color = (fork(d+1, i*2+0), fork(d+1, i*2+1))
    else:
      width = depth / 2
      color = shader(i % width, i / width)
  return color

# given a position, returns a color
# for this demo, it just busy loops
def demo_shader(x, y):
  bend i = 0:
    when i < 10:
      color = fork(i + 1)
    else:
      color = 0x000001
  return color

# renders a 256x256 image using demo_shader
def main:
  return render(5, demo_shader)

demo_shader is marked as unsafe since it duplicates i, and the program fails with the "ERROR: attempt to clone a non-affine global reference." error when render duplicates that function.

This is a very natural program to write, and the safety check this PR introduces will probably break many more programs created by users of Bend. I'm not sure how to deal with this... Should we really add this check in the way it's done by this PR, or should we do something else?

developedby · 2024-06-10T15:15:17Z

@developedby this PR breaks (surprisingly only) one of the tests in Bend, guide_shader_dummy.bend:
# given a shader, returns a square image
def render(depth, shader):
  bend d = 0, i = 0:
    when d < depth:
      color = (fork(d+1, i*2+0), fork(d+1, i*2+1))
    else:
      width = depth / 2
      color = shader(i % width, i / width)
  return color

# given a position, returns a color
# for this demo, it just busy loops
def demo_shader(x, y):
  bend i = 0:
    when i < 10:
      color = fork(i + 1)
    else:
      color = 0x000001
  return color

# renders a 256x256 image using demo_shader
def main:
  return render(5, demo_shader)
demo_shader is marked as unsafe since it duplicates i, and the program fails with the "ERROR: attempt to clone a non-affine global reference." error when render duplicates that function.

This is a very natural program to write, and the safety check this PR introduces will probably break many more programs created by users of Bend. I'm not sure how to deal with this... Should we really add this check in the way it's done by this PR, or should we do something else?

Yes, this is the intended behaviour and a big limitation of hvm32

developedby · 2024-06-10T15:18:26Z

If we plan on continuing with hvm32 for a lot longer, I should probably add some monomorphization system to Bend to avoid hitting this limitation so often

tjjfvi · 2024-06-10T16:37:59Z

src/ast.rs

+  pub fn direct_dependencies<'name>(&'name self) -> BTreeSet<&'name str> {
+    match self {
+      Tree::Ref { nam } => BTreeSet::from([nam.as_str()]),
+      Tree::Con { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Dup { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Opr { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Swi { fst, snd } => &fst.direct_dependencies() | &snd.direct_dependencies(),
+      Tree::Num { val } => BTreeSet::new(),
+      Tree::Var { nam } => BTreeSet::new(),
+      Tree::Era => BTreeSet::new(),
+    }
+  }


This function is quadratic, due to repeatedly cloning these btreesets; (@a (@b (@c (@d (@e ...))))) will take triangular time (which is asymptotically quadratic).

src/ast.rs

edusporto · 2024-06-10T18:15:30Z

All suggestions were resolved
Any other details or should we merge it? @enricozb @developedby @tjjfvi

tjjfvi · 2024-06-10T18:26:37Z

fine by me, although slight nit: direct_dependencies_reversed could instead be named direct_dependents (with similar naming changes made elsewhere)

Change "dependency reversed" to "dependent"

src/ast.rs

Co-authored-by: T6 <[email protected]>

edusporto added 8 commits June 6, 2024 00:24

Add first version of safety propagation

e6c8123

TODO: - Document how the algorithm works along with complexities - From the original bug that led to this, `ok.hvm` now works as expectes but `bad.hvm` still doesn't... - Investigate

Clean up and better comments

bc870fc

Merge branch 'main' into fix-safety-checking

3fd3412

Remove unnecessary lookup table return from Book::build

55b6b4c

Tidy up before pull request

77f8b73

Bump version

2bfbd99

Add @test-rust-only option

607426d

Add test for safety checking

0f44d07

edusporto commented Jun 7, 2024

View reviewed changes

edusporto requested review from enricozb and developedby June 7, 2024 19:25

edusporto mentioned this pull request Jun 7, 2024

Eraser nodes being placed where they shouldn't #362

Open

enricozb reviewed Jun 10, 2024

View reviewed changes

tjjfvi reviewed Jun 10, 2024

View reviewed changes

edusporto added 2 commits June 10, 2024 15:03

Resolve suggestions

0f675a8

Slightly better visited definition

92773fb

Function name change

e016d7c

Change "dependency reversed" to "dependent"

tjjfvi reviewed Jun 10, 2024

View reviewed changes

src/ast.rs Outdated Show resolved Hide resolved

enricozb self-requested a review June 10, 2024 19:20

enricozb approved these changes Jun 10, 2024

View reviewed changes

edusporto force-pushed the fix-safety-checking branch from 9ade570 to 9465666 Compare June 10, 2024 20:23

Fix function name change

23ad6dc

Co-authored-by: T6 <[email protected]>

edusporto force-pushed the fix-safety-checking branch from 9465666 to 23ad6dc Compare June 10, 2024 20:24

edusporto merged commit d153497 into main Jun 10, 2024
3 of 4 checks passed

edusporto deleted the fix-safety-checking branch June 10, 2024 20:28

edusporto mentioned this pull request Jun 10, 2024

Broken shader example in the guide HigherOrderCO/Bend#576

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Propagate unsafety to definitions that depend on unsafe definitions #379

Propagate unsafety to definitions that depend on unsafe definitions #379

edusporto commented Jun 7, 2024

edusporto Jun 7, 2024

enricozb Jun 10, 2024

tjjfvi Jun 10, 2024

edusporto Jun 10, 2024

edusporto Jun 7, 2024

enricozb Jun 10, 2024

enricozb left a comment

enricozb Jun 10, 2024

enricozb Jun 10, 2024

edusporto commented Jun 10, 2024

edusporto commented Jun 10, 2024

developedby commented Jun 10, 2024

developedby commented Jun 10, 2024

tjjfvi Jun 10, 2024

edusporto commented Jun 10, 2024

tjjfvi commented Jun 10, 2024

Propagate unsafety to definitions that depend on unsafe definitions #379

Propagate unsafety to definitions that depend on unsafe definitions #379

Conversation

edusporto commented Jun 7, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

enricozb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

edusporto commented Jun 10, 2024

edusporto commented Jun 10, 2024

developedby commented Jun 10, 2024

developedby commented Jun 10, 2024

Choose a reason for hiding this comment

edusporto commented Jun 10, 2024

tjjfvi commented Jun 10, 2024