Skip to content
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

Update InverseBranchFold strategy to not emit if #13

Closed
ngsankha opened this issue Jan 28, 2020 · 2 comments
Closed

Update InverseBranchFold strategy to not emit if #13

ngsankha opened this issue Jan 28, 2020 · 2 comments

Comments

@ngsankha
Copy link
Owner

We can fall back on the prog cond tuples to do the if statement generation at a later time. Will lead to better branch folding opportunities.

@ngsankha
Copy link
Owner Author

ngsankha commented Feb 10, 2020

This caused a big issue when writing the synthetic example for Overview section. The original spec was:

define :update_post, "(String, String, {created_by: ?String, title: ?String, slug: ?String}) -> Post", [Post, DemoUser], prog_size: 30 do
  spec "author can only change titles" do
    pre {
      @dummy = DemoUser.create(name: 'Dummy', username: 'dummy', admin: false)
      @admin = DemoUser.create(name: 'Admin', username: 'admin', admin: true)
      @author = DemoUser.create(name: 'Author', username: 'author', admin: false)
      @fake_post = Post.create(created_by: 'dummy', slug:'fake-post', title: 'Fake Post')
      @post = Post.create(created_by: 'author', slug:'hello-world', title: 'Hello World')
    }

    updated = update_post('author', 'hello-world', created_by: 'dummy', title: 'Foo Bar', slug: 'foo-bar')

    post { |updated|
      assert { updated.id == @post.id }
      assert { updated.created_by == "author" }
      assert { updated.title == "Foo Bar" }
      assert { updated.slug == 'hello-world' }
    }
  end

  spec "unrelated users cannot change anything" do
    pre {
      @dummy = DemoUser.create(name: 'Dummy', username: 'dummy', admin: false)
      @admin = DemoUser.create(name: 'Admin', username: 'admin', admin: true)
      @author = DemoUser.create(name: 'Author', username: 'author', admin: false)
      @fake_post = Post.create(created_by: 'dummy', slug:'fake-post', title: 'Fake Post')
      @post = Post.create(created_by: 'author', slug:'hello-world', title: 'Hello World')
    }

    updated = update_post('dummy', 'hello-world', created_by: 'dummy', title: 'Foo Bar', slug: 'foo-bar')

    post { |updated|
      assert { updated.id == @post.id }
      assert { updated.created_by == "author" }
      assert { updated.title == "Hello World" }
      assert { updated.slug == 'hello-world' }
    }
  end

  spec "admin can takeover any post" do
    pre {
      @dummy = DemoUser.create(name: 'Dummy', username: 'dummy', admin: false)
      @admin = DemoUser.create(name: 'Admin', username: 'admin', admin: true)
      @author = DemoUser.create(name: 'Author', username: 'author', admin: false)
      @fake_post = Post.create(created_by: 'dummy', slug:'fake-post', title: 'Fake Post')
      @post = Post.create(created_by: 'author', slug:'hello-world', title: 'Hello World')
    }

    updated = update_post('admin', 'hello-world', created_by: 'dummy', title: 'Foo Bar', slug: 'foo-bar')

    post { |updated|
      assert { updated.id == @post.id }
      assert { updated.created_by == "dummy" }
      assert { updated.title == "Foo Bar" }
      assert { updated.slug == 'foo-bar' }
    }
  end

  puts generate_program
end

This fails to synthesize because the branch predicates are lost in this fold. If the first spec is made last, then the synthesis completes with the following output:

def update_post(arg0, arg1, arg2)
  if DemoUser.exists?(username: arg0, admin: false)
    if Post.exists?(created_by: arg0, slug: arg1)
      t2 = Post.where(slug: arg1).first
      t2.title=arg2.[](:title)
      t2
    else
      Post.where(slug: arg1).first
    end
  else
    t4 = Post.where(slug: arg1).first
    t4.created_by=arg2.[](:created_by)
    t4.title=arg2.[](:title)
    t4.slug=arg2.[](:slug)
    t4
  end
end

@ngsankha
Copy link
Owner Author

ngsankha commented Mar 6, 2020

Fixed!

@ngsankha ngsankha closed this as completed Mar 6, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant