Record & Pointer Types

flake.nix

@@ -5,30 +5,41 @@
     infuse-src.flake = false;
   };
   outputs =
-    { self
-    , nixpkgs
-    , infuse-src
+    {
+      self,
+      nixpkgs,
+      infuse-src,
     }@args:
     let
       inherit (nixpkgs) lib;
 
-      inherit (import ./nix/infuse-lib.nix {
-        lib = lib;
-        infuse-src = infuse-src;
-      }) infuse infuse-with;
+      inherit
+        (import ./nix/infuse-lib.nix {
+          lib = lib;
+          infuse-src = infuse-src;
+        })
+        infuse
+        infuse-with
+        ;
 
       inherit (import ./nix/flake-for-all-systems.nix { lib = lib; })
-        flake-for-all-systems;
+        flake-for-all-systems
+        ;
 
-    in flake-for-all-systems args {
-      systems = ["x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin"];
-      outputs = { self, nixpkgs, ... }:
+    in
+    flake-for-all-systems args {
+      systems = [
+        "x86_64-linux"
+        "aarch64-linux"
+        "aarch64-darwin"
+        "x86_64-darwin"
+      ];
+      outputs =
+        { self, nixpkgs, ... }:
         let
           pkgs = nixpkgs.legacyPackages;
-          selfOcamlPackages =
-            pkgs.ocamlPackages.overrideScope self.overlays.addBincamlPackages;
-          fpOcamlPackages =
-            selfOcamlPackages.overrideScope self.overlays.enableOcamlFramePointer;
+          selfOcamlPackages = pkgs.ocamlPackages.overrideScope self.overlays.addBincamlPackages;
+          fpOcamlPackages = selfOcamlPackages.overrideScope self.overlays.enableOcamlFramePointer;
         in
         {
           defaultPackage = selfOcamlPackages.bincaml;
@@ -40,17 +51,19 @@
               intPQueue = ofinal.callPackage ./nix/intpqueue.nix { };
             };
 
-            enableOcamlFramePointer = ofinal: infuse-with {
-              # https://github.com/NixOS/nixpkgs/blob/aca4d95fce4914b3892661bcb80b8087293536c6/pkgs/development/compilers/ocaml/generic.nix#L30
-              ocaml.__input.flambdaSupport.__assign = true;
-              ocaml.__input.framePointerSupport.__assign = true;
-              ocaml.__attrs.patches.__append = [
-                (pkgs.fetchpatch {
-                  url = "https://github.com/ocaml/ocaml/commit/c2eec4dd1de7d0da2d2f76e5e7f2b567901f4e2c.patch";
-                  hash = "sha256-qDx8saOLhFMYaK4PLsSvHnDBYKvRSMmPtdVa/IqkQSI=";
-                })
-              ];
-            };
+            enableOcamlFramePointer =
+              ofinal:
+              infuse-with {
+                # https://github.com/NixOS/nixpkgs/blob/aca4d95fce4914b3892661bcb80b8087293536c6/pkgs/development/compilers/ocaml/generic.nix#L30
+                ocaml.__input.flambdaSupport.__assign = true;
+                ocaml.__input.framePointerSupport.__assign = true;
+                ocaml.__attrs.patches.__append = [
+                  (pkgs.fetchpatch {
+                    url = "https://github.com/ocaml/ocaml/commit/c2eec4dd1de7d0da2d2f76e5e7f2b567901f4e2c.patch";
+                    hash = "sha256-qDx8saOLhFMYaK4PLsSvHnDBYKvRSMmPtdVa/IqkQSI=";
+                  })
+                ];
+              };
           };
 
           legacyPackages = {
@@ -68,8 +81,6 @@
             fp = fpOcamlPackages.callPackage ./nix/shell.nix { };
             no-fp = selfOcamlPackages.callPackage ./nix/shell.nix { };
           };
-        }
-      ;
-    }
-  ;
+        };
+    };
 }

lib/analysis/defuse_bool.ml

@@ -40,10 +40,17 @@ module IsZeroValueAbstraction = struct
     | `Bool true -> NonZero
     | `Bool false -> Zero
     | `Integer i -> if Z.equal Z.zero i then Zero else NonZero
-    | `Bitvector i ->
+    | `Bitvector i | `Pointer (i, _) ->
         if Bitvec.size i = 0 then Top
         else if Z.equal Z.zero (Bitvec.value i) then Zero
         else NonZero
+    | `Record fields ->
+        StringMap.fold
+          (fun _ ({ value = i; _ } : Lang.Ops.Record.field) acc ->
+            if Bitvec.size i = 0 then Top
+            else if Z.equal Z.zero (Bitvec.value i) then join acc Zero
+            else join acc NonZero)
+          fields Zero
 
   let eval_unop (op : Lang.Ops.AllOps.unary) a =
     match op with
@@ -58,13 +65,17 @@ module IsZeroValueAbstraction = struct
     | `Old -> Top
     | `Exists -> Top
     | `Forall | `Lambda | `Gamma | `Classification -> Top
+    (* NOTE: More effort would be needed to be able to say is this one field zero or not *)
+    | `FACCESS offset -> ( match a with Zero -> Zero | _ -> Top)
 
   let eval_binop (op : Lang.Ops.AllOps.binary) a b =
     match (op, a, b) with
     | `BVSREM, _, _ -> Top
     | `BVSDIV, _, _ -> Top
     | `BVADD, Zero, Zero -> Zero
+    | `PTRADD, Zero, Zero -> Zero
     | `BVADD, _, _ -> Top
+    | `PTRADD, _, _ -> Top
     | `NEQ, Zero, Zero -> Zero
     | `NEQ, _, _ -> Top
     | `BVASHR, _, _ -> Top
@@ -101,6 +112,10 @@ module IsZeroValueAbstraction = struct
     | `INTSUB, _, _ -> Top
     | `BVSLT, Zero, Zero -> Zero
     | `BVSLT, _, _ -> Top
+    | `FSET _, Zero, Zero -> Zero
+    | `FSET _, _, NonZero -> NonZero
+    (* Larger refactor would be needed to reason about individual fields *)
+    | `FSET _, _, _ -> Top
     | #Lang.Ops.Spec.binary, _, _ -> Top
 
   let eval_intrin (op : Lang.Ops.AllOps.intrin) (args : t list) =

lib/analysis/wrapped_intervals.ml

@@ -697,7 +697,10 @@ module WrappedIntervalsValueAbstraction = struct
     match op with
     | `Bool _ -> top
     | `Integer _ -> top
-    | `Bitvector bv -> if size bv = 0 then top else interval bv bv
+    | `Bitvector bv | `Pointer (bv, _) ->
+        if size bv = 0 then top else interval bv bv
+    (* NOTE: This kind of thing happens frequently, should I go through all of the fields and make a intervals out of those bvs?*)
+    | `Record fields -> top
 
   let eval_unop (op : Lang.Ops.AllOps.unary) (a, t) rt =
     match t with
@@ -715,7 +718,7 @@ module WrappedIntervalsValueAbstraction = struct
     match (ta, ta) with
     | Types.Bitvector width, Types.Bitvector w2 when width = w2 -> (
         match op with
-        | `BVADD -> add ~width a b
+        | `BVADD | `PTRADD -> add ~width a b
         | `BVSUB -> sub ~width a b
         | `BVMUL -> mul ~width a b
         | `BVUDIV -> udiv ~width a b

lib/fe/BasilIR.cf

@@ -7,6 +7,7 @@ terminator Decl ";";
 position token BVTYPE ('b' 'v' digit+) ;
 position token INTTYPE {"int"} ;
 position token BOOLTYPE {"bool"} ;
+position token POINTERTYPE {"ptr"} ;
 
 {- position token UserIdent '`' ((upper | letter | '_' | '#')(upper | letter | digit | ["_.$#"])*) '`'; -}
 position token BIdent '.'((upper | letter | '_')(upper | letter | digit | ["_.$#~"])*) ;
@@ -71,8 +72,13 @@ Decl_Type . Decl ::= "type" LocalIdent ;
 ProcDef_Empty . ProcDef ::= ;
 ProcDef_Some  . ProcDef ::= BeginList [Block] EndList ;
 
+separator Field "," ;
+Field1 . Field ::= OpenParen Str ":" Type CloseParen ;
+
 IntType1 . IntType ::= INTTYPE ;
 BoolType1. BoolType ::= BOOLTYPE ;
+RecordType1 . RecordType ::= BeginRec [Field] EndRec ;
+PointerType1 . PointerType ::= "ptr" OpenParen Type "," Type CloseParen ;
 BVType1 . BVType ::= BVTYPE ;
 -- map types are right associative. left of -> cannot be another MapType.
 MapType1 . MapType ::=  Type1 "->" Type ; 
@@ -86,20 +92,24 @@ VariantCase . SumCase    ::= LocalIdent "of" BeginRec [RecordField] EndRec;
 separator nonempty SumCase "|";
 
 
-TypeIntType  . Type1 ::= IntType ;
-TypeBoolType . Type1 ::= BoolType ;
-TypeBVType   . Type1 ::= BVType ;
-TypeParen    . Type1 ::= OpenParen Type CloseParen; 
-TypeSort . Type1 ::= LocalIdent;
-
-TypeMapType . Type ::= MapType;
+TypeIntType     . Type1 ::= IntType ;
+TypeBoolType    . Type1 ::= BoolType ;
+TypeBVType      . Type1 ::= BVType ;
+TypePointerType . Type1 ::= PointerType ;
+TypeRecordType  . Type1 ::= RecordType ;
+TypeVarType     . Type1 ::= LocalIdent ;
+TypeParen       . Type1 ::= OpenParen Type CloseParen; 
+TypeMapType     . Type ::= MapType;
 _ . Type ::= Type1;
 
 IntVal_Hex . IntVal ::= IntegerHex ;
 IntVal_Dec . IntVal ::=  IntegerDec ;
 
 rules BVVal ::=  IntVal ":" BVType ;
 
+separator FieldVal "," ;
+rules FieldVal ::= OpenParen Str ":" BVVal "," Type CloseParen;
+
 Endian_Little . Endian ::= "le" ;
 Endian_Big . Endian ::= "be" ;
 
@@ -215,6 +225,8 @@ separator Params "," ;
 
 Value_BV . Value ::=  BVVal;
 Value_Int . Value ::= IntVal;
+Value_Record . Value ::= OpenParen [FieldVal] CloseParen;
+Value_Pointer . Value ::= "ptr" OpenParen BVVal "," PointerType CloseParen;
 Value_True . Value ::= "true" ;
 Value_False . Value ::= "false" ;
 
@@ -246,7 +258,7 @@ Expr_FunctionOp . Expr1       ::= Expr1 OpenParen [Expr] CloseParen;
 
 -- binary expr
 
-rules BinOp ::= BVBinOp | BVLogicalBinOp | IntLogicalBinOp | IntBinOp | EqOp ;
+rules BinOp ::= BVBinOp | BVLogicalBinOp | IntLogicalBinOp | IntBinOp | EqOp | PointerBinOp ;
 Expr_Binary . Expr2      ::= BinOp OpenParen Expr "," Expr CloseParen ;
 Expr_Assoc  . Expr2      ::= BoolBinOp OpenParen [Expr] CloseParen ;
 
@@ -260,6 +272,8 @@ Expr_ZeroExtend . Expr2 ::= "zero_extend" OpenParen IntVal "," Expr CloseParen ;
 Expr_SignExtend . Expr2 ::= "sign_extend" OpenParen IntVal "," Expr CloseParen ;
 Expr_Extract    . Expr2 ::= "extract" OpenParen IntVal "," IntVal "," Expr CloseParen ;
 Expr_Concat     . Expr2 ::= "bvconcat"  OpenParen [Expr]  CloseParen ;
+Expr_FSet       . Expr2 ::= "fset" OpenParen Str "," Expr "," Expr CloseParen ;
+Expr_FAccess    . Expr2 ::= "faccess" OpenParen Str "," Expr CloseParen ;
 
 CaseCase . Case ::= Expr "->" Expr  ;
 CaseDefault . Case ::=  "_" "->" Expr ;
@@ -280,7 +294,7 @@ rules BVLogicalBinOp ::= "bvule" |  "bvugt" |  "bvuge" | "bvult" | "bvslt" |  "b
 rules IntBinOp ::= "intadd" | "intmul" | "intsub" | "intdiv" | "intmod"  ;
 rules IntLogicalBinOp ::=  "intlt" | "intle" | "intgt" | "intge" ;
 rules BoolBinOp ::=  "booland" | "boolor" | "boolimplies" ;
-
+rules PointerBinOp ::= "ptradd" ;
 
 {- SPECIFICATION -}