Memory Encoding

flake.nix

@@ -0,0 +1,77 @@
+{
+  inputs = {
+    flake-utils.url = "github:numtide/flake-utils";
+    nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+    nixpkgs-mill.url = "github:NixOS/nixpkgs/914a3a6a1024f495af1f5a35c420b170d8b946dd";
+    pac-nix.url = "github:katrinafyi/pac-nix";
+  };
+
+  outputs =
+    {
+      self,
+      nixpkgs,
+      nixpkgs-mill,
+      flake-utils,
+      pac-nix,
+    }:
+    flake-utils.lib.eachSystem [ "x86_64-linux" ] (
+      system:
+      let
+        pkgs = import nixpkgs {
+          inherit system;
+        };
+
+        millPkgs = import nixpkgs-mill {
+          inherit system;
+        };
+      in
+      {
+        devShell = pkgs.mkShell {
+          LD_LIBRARY_PATH = "${pkgs.gmp}/lib:";
+
+          buildInputs =
+            (with pkgs; [
+              scala
+              scala-cli
+              ctags
+              metals
+              jdk
+              boogie
+              coursier
+              gmp
+              # z3
+              cvc5
+              antlr
+              haskellPackages.BNFC
+
+              pkgsCross.aarch64-multiplatform.pkgsBuildHost.gcc
+              pkgsCross.aarch64-multiplatform.pkgsBuildHost.clang
+              pkgsCross.aarch64-multiplatform.pkgsBuildHost.llvmPackages.clang
+
+              pkgsCross.aarch64-multiplatform-musl.pkgsBuildHost.gcc
+              pkgsCross.aarch64-multiplatform-musl.pkgsBuildHost.clang
+              pkgsCross.aarch64-multiplatform-musl.pkgsBuildHost.llvmPackages.clang
+              sbt
+
+              just
+
+              # bincaml stuff:
+              ocaml
+              ocamlPackages.ocaml-lsp
+              opam
+              # gnumake
+            ])
+            ++ (with millPkgs; [
+              # mill
+            ])
+            ++ [
+              pac-nix.packages.${system}.ddisasm
+              pac-nix.packages.${system}.gtirb-semantics
+              pac-nix.packages.${system}.gtirb-pprinter
+              pac-nix.packages.${system}.basil
+              pac-nix.packages.${system}.asli
+            ];
+        };
+      }
+    );
+}

src/main/scala/Main.scala

@@ -10,6 +10,7 @@ import util.{
   BoogieGeneratorConfig,
   BoogieMemoryAccessMode,
   DSAPhase,
+  MemoryEncodingRepresentation,
   DSConfig,
   DebugDumpIRLogger,
   ILLoadingConfig,
@@ -264,7 +265,14 @@ object Main {
     @arg(name = "noif", doc = "Disable information flow security transform in Boogie output")
     noif: Flag,
     @arg(name = "nodebug", doc = "Disable runtime debug assertions")
-    noDebug: Flag
+    noDebug: Flag,
+    @arg(
+      name = "memory-encoding",
+      doc = """Enable memory encoding. options: flat | split(,reverseOrder)(,splitMem).
+      | flat: maps pointers to abstract metadata leveraging quantifiers + triggers for regions.
+      | split: embeds base + offset into pointers, reducing maximum allocations/allocation size but eliminating quantifiers and most pointer metadata. reverseOrder changes mapping to (offset -> base) and splitMem splits heap load/stores."""
+    )
+    memoryEncoding: Option[String]
   )
 
   def main(args: Array[String]): Unit = {
@@ -380,13 +388,33 @@ object Main {
         throw new IllegalArgumentException("Illegal argument for --assert-callee-saved. allowed: (auto|always|never)")
     }
 
+    val memoryEncodingRepresentation = conf.memoryEncoding match
+      case None => None
+      case Some("flat") | Some("") => Some(MemoryEncodingRepresentation.Flat)
+      case Some(s) if s.slice(0, 5) == "split" => {
+        val parts = s.split(',')
+        Some(MemoryEncodingRepresentation.Split(
+          splitMem = parts.contains("splitMem"),
+          baseFirst = !parts.contains("reverseOrder")
+        ))
+      }
+      case Some(_) =>
+        throw new IllegalArgumentException("Illegal option to memory-encoding, allowed are: flat | split(,reverseOrder)(,splitMem)")
+
     val boogieMemoryAccessMode = if (conf.lambdaStores.value) {
       BoogieMemoryAccessMode.LambdaStoreSelect
     } else {
       BoogieMemoryAccessMode.SuccessiveStoreSelect
     }
     val boogieGeneratorConfig =
-      BoogieGeneratorConfig(boogieMemoryAccessMode, true, rely, conf.threadSplit.value, conf.noif.value)
+      BoogieGeneratorConfig(
+        boogieMemoryAccessMode,
+        true,
+        rely,
+        conf.threadSplit.value,
+        conf.noif.value,
+        memoryEncoding = memoryEncodingRepresentation
+      )
 
     var loadingInputs = if (conf.bapInputDirName.isDefined) then {
       loadDirectory(ChooseInput.Bap, conf.bapInputDirName.get)
@@ -488,7 +516,8 @@ object Main {
       outputPrefix = conf.outFileName,
       dsaConfig = dsa,
       memoryTransform = conf.memoryTransform.value,
-      assertCalleeSaved = calleeSaved
+      assertCalleeSaved = calleeSaved,
+      memoryEncoding = memoryEncodingRepresentation
     )
 
     Logger.info(programNameVersionHeader)

src/main/scala/analysis/procedure_summaries/SummaryGenerator.scala

@@ -221,8 +221,8 @@ def getGenerateProcedureSummariesTransform(simplified: Boolean): Transform =
 
       val summaryGenerator = SummaryGenerator(prog, simplified)
       for procedure <- prog.procedures if procedure != prog.mainProcedure do
-        procedure.requires = summaryGenerator.generateRequires(procedure)
-        procedure.ensures = summaryGenerator.generateEnsures(procedure)
+        procedure.requires ++= summaryGenerator.generateRequires(procedure)
+        procedure.ensures ++= summaryGenerator.generateEnsures(procedure)
 
       man.ClobberAll
     },