[prev in list] [next in list] [prev in thread] [next in thread] 

List:       klee-commits
Subject:    [klee-commits] [klee/klee] 279be1: Test case for externally concretized variables and...
From:       MartinNowack <noreply () github ! com>
Date:       2024-02-29 19:57:20
Message-ID: klee/klee/push/refs/heads/master/7b8ede-76a2ad () github ! com
[Download RAW message or body]


*******************
This email originates from outside Imperial. Do not click on links and attachments \
unless you recognise the sender.  If you trust the sender, add them to your safe \
senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping \
                for this address.
*******************
  Branch: refs/heads/master
  Home:   https://github.com/klee/klee
  Commit: 279be1d2748f9694c27423cc650deb46638736ad
      https://github.com/klee/klee/commit/279be1d2748f9694c27423cc650deb46638736ad
  Author: Martin Nowack <m.nowack@imperial.ac.uk>
  Date:   2024-02-29 (Thu, 29 Feb 2024)

  Changed paths:
    A test/Feature/ConcretizeSymbolicExternals.c

  Log Message:
  -----------
  Test case for externally concretized variables and constraint fully symbolic \
variables

The test case is based on the example provided by Mingyi Liu from the KLEE
mailing list.


  Commit: a4d9762a31402c5e5298ef22870a7e25124a7af2
      https://github.com/klee/klee/commit/a4d9762a31402c5e5298ef22870a7e25124a7af2
  Author: Martin Nowack <m.nowack@imperial.ac.uk>
  Date:   2024-02-29 (Thu, 29 Feb 2024)

  Changed paths:
    M lib/Core/AddressSpace.cpp

  Log Message:
  -----------
  Correctly update symbolic variables that have been changed externally

Before, external changes to symbolic variables have not been propagated
back to their internal representation.

Do a byte-by-byte comparison and update object state if required.


  Commit: 8750da62ccb9772a121126d5fffd393690c95758
      https://github.com/klee/klee/commit/8750da62ccb9772a121126d5fffd393690c95758
  Author: Martin Nowack <m.nowack@imperial.ac.uk>
  Date:   2024-02-29 (Thu, 29 Feb 2024)

  Changed paths:
    M lib/Core/Memory.cpp

  Log Message:
  -----------
  Use correctly constrained constants if the memory object is fully symbolic

Before, only partially symbolic variables have been concretized.
Now, every object that is not fully concrete is concretized correctly
this includes fully symbolic objects.


  Commit: 46b4c4885c0162893835081e2d9d731ca7a8341c
      https://github.com/klee/klee/commit/46b4c4885c0162893835081e2d9d731ca7a8341c
  Author: Martin Nowack <m.nowack@imperial.ac.uk>
  Date:   2024-02-29 (Thu, 29 Feb 2024)

  Changed paths:
    M lib/Core/Executor.h
    M lib/Core/Memory.cpp
    M lib/Core/Memory.h

  Log Message:
  -----------
  Refactor `ObjectState::flushToConcreteStore` to use `toConstant`

Use existing `Executor::toConstant()` function to transform a symbolic
byte of an `ObjectState` to its concrete representation.

This will also add constraints if required.


  Commit: 2cae55383a11fbcb3fcc1a8bac67949e2245d451
      https://github.com/klee/klee/commit/2cae55383a11fbcb3fcc1a8bac67949e2245d451
  Author: Martin Nowack <m.nowack@imperial.ac.uk>
  Date:   2024-02-29 (Thu, 29 Feb 2024)

  Changed paths:
    M lib/Core/Executor.cpp

  Log Message:
  -----------
  Support external call concretisation policies for referenced objects

Provide an additional argument to select the concretisation policy.

Fix a bug where the concretisation of a shared memory object was visible
across different states by retrieving a writable object state first.


  Commit: 76a2adef91dc987083e8e30f40c4143742e4e726
      https://github.com/klee/klee/commit/76a2adef91dc987083e8e30f40c4143742e4e726
  Author: Martin Nowack <m.nowack@imperial.ac.uk>
  Date:   2024-02-29 (Thu, 29 Feb 2024)

  Changed paths:
    M lib/Core/AddressSpace.cpp
    M lib/Core/AddressSpace.h
    M lib/Core/Executor.cpp

  Log Message:
  -----------
  Add support to fully concretise objects if modified externally

Propagate ExternalCallPolicy to allow user-based selection.


Compare: https://github.com/klee/klee/compare/7b8edeb2a7cc...76a2adef91dc

To unsubscribe from these emails, change your notification settings at \
https://github.com/klee/klee/settings/notifications

_______________________________________________
klee-commits mailing list
klee-commits@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-commits


[prev in list] [next in list] [prev in thread] [next in thread]