Plans on SMG fixes

  • enable CI (#3 (closed))
  • fix easy problems detected by CI
  • merge trunk into smg-master
    • !13 (merged) update CI after merge
    • check aligned/packed attributes
  • merge fixes into smg-master
  • refactor:
    • SMG consistency runtime checks, see #32 for details, see also upstream #712.
    • unsupported features in input
      • unsupported features (atexit, pthread_create, ...) -- fail with error?
      • recursion -- two modes: strict fails (for competitions), default keeps searching for bugs and reports unknown instead of true
      • cannot evaluate size / offset -- same as above?
    • get rid of HV-edge filter !29
      • was necessary when HVEs was a flat collection
      • introduce methods #getHVEs(object), #getHVE(object, offset), #hasHVE(object, offset, bitsize)
      • other, more rare variants of filtering
      • depends on how we treat value sizes
      • maybe add backwards map value->HVEs with this value
    • get rid of PT-edge filter too?
      • add backwards collection for PTEs so we can use same scheme as for HVEs
    • objects
      • fix: stack allocations are not variables, move to separate collection in frame, forbid abstracting
      • fix: invalid heap should still be in heap collection
      • see which collections we need
      • refactor collections into the small ones, return big ones as chained iterators over small
      • isHeap, isStack, isGlobal, isExternal should be object's method, without lookup in an SMG collections
        • isExternal is spreading in SMGState#pruneUnreachable, so it is not an object's method. Split into isExternal and isReachableFromExternal?
      • refactor SMGObject's hierarchy:
        • make SMGAbstractObject an abstract class under SMGObject !34 (merged)
        • introduce children for SMGRegion: variable, allocation, return object, string literal, function. This way we can be sure if something is an allocation and can add specifics inside.
          • make use of SMGRegion's hierarchy: store and retrieve specific information via methods
    • evaluators, see !9
      • remove address value class
      • might fix #1, #7, #12, #17
Edited by Олег Максимович Петров