Permalink
Browse files

[bonsai][Analysis] The pre operator can only be applied to single_spa…

…ce and world_line variable and in a READ context.
  • Loading branch information...
ptal committed May 12, 2017
1 parent ce96630 commit b4604dcc3505763cf2416ae8726b94b37688e0e7
View
@@ -50,7 +50,7 @@ rm ~/.m2/repository/bonsai
# Example
The following command will compile and execute the NQueens problem as described in the file [NQueens.bonsai.java](examples/bonsai/NQueens/src/main/java/bonsai/example/NQueens.bonsai.java):
The following command will compile and execute the NQueens problem as described in the file [NQueens.bonsai.java](examples/bonsai/NQueens/src/main/java/bonsai/examples/NQueens.bonsai.java):
```sh
cd examples/bonsai/NQueens
@@ -0,0 +1,38 @@
// Copyright 2017 Pierre Talbot (IRCAM)
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
// http://www.apache.org/licenses/LICENSE-2.0
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#[error(E0016, 33, 4)]
#[error(E0016, 34, 4)]
#[error(E0016, 36, 15)]
#[error(E0016, 36, 22)]
package test;
public class ForbiddenWriteOnPre
{
ref single_space T a;
single_space T ok;
public ForbiddenWriteOnPre(T a) {
this.a = a;
}
proc test() {
world_line N b;
pre a <- 1;
pre b <- 2;
ok <- pre a;
J.external(pre b, pre a, ok);
}
}
@@ -0,0 +1,40 @@
// Copyright 2017 Pierre Talbot (IRCAM)
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
// http://www.apache.org/licenses/LICENSE-2.0
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#[error(E0017, 35, 10)]
#[error(E0017, 36, 10)]
#[error(E0017, 37, 10)]
#[error(E0017, 38, 9)]
#[error(E0017, 38, 18)]
package test;
public class PreOnlyOnStream
{
JavaHost h = new JavaHost();
module Module m;
single_space transient T ok;
public PreOnlyOnStream(T a) {
this.a = a;
}
proc test() {
single_time N b;
ok <- pre b;
ok <- pre m;
ok <- pre h;
when pre b |= pre m { nothing; }
}
}
@@ -27,31 +27,80 @@ pub fn approximate_permission<'a>(context: Context<'a>) -> Partial<Context<'a>>
struct ApproximatePermission<'a> {
context: Context<'a>,
perm_context: Permission
perm_context: Permission,
context_span: Span
}
impl<'a> ApproximatePermission<'a> {
pub fn new(context: Context<'a>) -> Self {
ApproximatePermission {
context: context,
perm_context: Permission::ReadWrite,
context_span: DUMMY_SP
}
}
fn session(&'a self) -> &'a Session {
self.context.session
}
fn compute(mut self) -> Partial<Context<'a>> {
let mut bcrate_clone = self.context.clone_ast();
self.visit_crate(&mut bcrate_clone);
self.context.replace_ast(bcrate_clone);
Partial::Value(self.context)
if self.session().has_errors() {
Partial::Fake(self.context)
} else {
Partial::Value(self.context)
}
}
fn pre_on_variable(&self, var: &Variable) {
if var.past > 0 {
let uid = var.last_uid();
match self.context.var_by_uid(uid).kind {
Kind::Product => self.err_forbid_pre_on(var, "module"),
Kind::Host => self.err_forbid_pre_on(var, "host"),
Kind::Spacetime(Spacetime::SingleTime) => self.err_forbid_pre_on(var, "single_time"),
_ => {
if self.perm_context != Permission::Read {
self.err_forbid_write_on_pre(var);
}
}
}
}
}
fn err_forbid_write_on_pre(&self, var: &Variable) {
self.session().struct_span_err_with_code(var.span,
&format!("forbidden write on `pre` variable."),
"E0016")
.span_label(var.span, &format!("write here"))
.help(&"`pre` variables can only be read. External function call's parameters are considered as read/write variables.")
.emit();
}
fn err_forbid_pre_on(&self, var: &Variable, kind: &str) {
self.session().struct_span_err_with_code(var.span,
&format!("forbidden `pre` on {} variable.", kind),
"E0017")
.help(&"Only `single_space` and `world_line` variables can be used under the `pre` operator.")
.emit();
}
}
impl<'a> VisitorMut<JClass> for ApproximatePermission<'a>
{
fn visit_var(&mut self, var: &mut Variable) {
self.pre_on_variable(var);
var.permission = self.perm_context;
}
fn visit_stmt(&mut self, child: &mut Stmt) {
self.context_span = child.span;
walk_stmt_mut(self, child)
}
fn visit_tell(&mut self, var: &mut Variable, expr: &mut Expr) {
let old = self.perm_context;
self.perm_context = Permission::Write;
@@ -13,7 +13,7 @@
// limitations under the License.
/// `RefInitialization` checks:
/// (a) Each module containing referenced fields (keyword `ref`) must has a single constructor initializing these variables. It must simply appears in the constructor argument list with the same type and same name. An assert checking that the argument and the field are the same is added in the generation stage (TODO).
/// (a) Each module containing referenced fields (keyword `ref`) must have a single constructor initializing these variables. It must simply appears in the constructor argument list with the same type and same name. An assert checking that the argument and the field are the same is added in the generation stage.
/// (b) Ref fields must not be initialized with right handed expression when declared.
use context::*;

0 comments on commit b4604dc

Please sign in to comment.