Fix bugs in pragma parsing and ak_strength in model

rems-project · Aug 2, 2023 · 5365d21 · 5365d21
1 parent 7804b11
commit 5365d21
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/isla-lib/src/ir_lexer.rs b/isla-lib/src/ir_lexer.rs
@@ -264,7 +264,7 @@ lexer! {
         '#' $id_start $id_continue* $$whitespace (_ # '\n')* '\n' => |lexer| {
             let pragma_line = lexer.match_();
             let (pragma, args) = pragma_line.split_once(char::is_whitespace).unwrap();
-            lexer.return_(Tok::Pragma(pragma, args))
+            lexer.return_(Tok::Pragma(pragma, args.trim()))
         },
 
         '"' => |lexer| lexer.switch(LexerRule::String),

diff --git a/isla-lib/src/ir_parser.lalrpop b/isla-lib/src/ir_parser.lalrpop
@@ -220,15 +220,15 @@ pub Def: Def<Name, B> = {
     <p:"pragma"> => {
         let name = p.0;
         let s = p.1;
-        if name == "tuplestruct" {
+        if name == "#tuplestruct" {
             let mut iter = s.split_whitespace();
             let id = iter.next().map(|tuple| symtab.intern(tuple)).expect("malformed #tuplestruct pragma in IR");
             let mut fields = Vec::new();
             for field in iter {
                 fields.push(symtab.intern(field))
             }
             symtab.tuple_structs.insert(id, fields);
-        } else if name == "mangled" {
+        } else if name == "#mangled" {
             let (original, mangled) = s.split_once(' ').expect("malformed #mangled pragma in IR");
             let mangled = symtab.intern(mangled);
             symtab.mangled_names.insert(mangled, original);

diff --git a/web/client/dist/aarch64.cat b/web/client/dist/aarch64.cat
@@ -78,18 +78,18 @@ enum Access_variety = {
 
 enum Access_strength = {
   AS_normal,
-  AS_rel_or_acq, 
+  AS_rel_or_acq,
   AS_acq_rcpc
 }
 
 index T
 
 accessor ak_variety: Access_variety = .access_kind.match { AK_explicit => .variety, _ => default }
-accessor ak_strength: Access_strength = .access_kind.match { AK_explicit => .variety, _ => default }
+accessor ak_strength: Access_strength = .access_kind.match { AK_explicit => .strength, _ => default }
 
-define A(ev: Event): bool = R(ev) & (ak_variety(ev) == AS_rel_or_acq)
-define Q(ev: Event): bool = R(ev) & (ak_variety(ev) == AS_acq_rcpc)
-define L(ev: Event): bool = W(ev) & (ak_variety(ev) == AS_rel_or_acq)
+define A(ev: Event): bool = R(ev) & (ak_strength(ev) == AS_rel_or_acq)
+define Q(ev: Event): bool = R(ev) & (ak_strength(ev) == AS_acq_rcpc)
+define L(ev: Event): bool = W(ev) & (ak_strength(ev) == AS_rel_or_acq)
 
 define B(ev: Event): bool = false